Chukri Soueidi | LIG - Université Grenoble Alpes (2024)

• Print
• Share
• Share on Facebook
• Share on Twitter
• Share on LinkedIn
• Share url

Abstract:

Runtime Verification is an essential dynamic verification technique that enables formal reasoning on program executions based on specified properties. Runtime verification can be used in various stages of application development or online in production environments. Instrumentation plays a critical role in ensuring that monitors receive accurate traces that abstract needed information from the executing program. Otherwise, the integrity of the monitoring process is compromised, rendering the results unreliable. In this thesis, our primary focus is on online monitoring and concurrent programs. We identify three key challenges in applying runtime verification to these areas: capturing the correct traces, effectively guiding the instrumentation process, and assessing the validity of the collected traces. These challenges often render existing monitoring frameworks inadequate in various scenarios. To address the first two challenges mentioned above, this thesis introduces BISM, a bytecode-level instrumentation framework designed for JVM languages. BISM provides high-level abstractions suitable for different types of users within the domain of runtime verification and fulfills the following expressiveness capabilities. First, BISM allows the extraction of events at the bytecode level accommodating the monitoring of properties specified over events with various granularity levels. Second, BISM is designed to support writing static analyzers within the instrumentation specification. This enables guiding the instrumentation process to consider property and program semantics in order to optimize instrumentation. Third, BISM provides advanced users with the flexibility of unrestricted code modification. This feature is essential for deploying inline monitors or enforcing certain properties such as a sequential order of concurrent events. Building on the capabilities of the instrumentation framework, we introduce a novel method for residual runtime verification of parametric properties. This approach minimizes instrumentation points by integrating both property semantics and program behavior and applies to a broad range of safety and co-safety properties. Notably, this method is designed to be independent of external static analysis frameworks and can be performed fully within the instrumentation process, allowing for modular integration into various runtime verification workflows. For concurrent programs, we focus on the online monitoring of general behavioral properties. We highlight the shortcomings of using linear traces for capturing the behavior of concurrent programs and propose that a trace must satisfy two critical properties—soundness and faithfulness—to provide an accurate representation. To meet these criteria, we introduce a trace-collection methodology that employs a real-time vector clock algorithm to establish event causality in a non-intrusive manner. This algorithm can run off the program's critical path, minimizing the impact on the execution. Additionally, we present new criteria for assessing the validity of collected traces in concurrent programs, addressing the third challenge mentioned above. We redefine the concept of trace monitorability based on automata-based formalisms. Our refined definition integrates a causal dependence relation extracted from a given property to identify non-permutable events within a trace. This allows us to evaluate whether a trace contains sufficient order information to yield a sound monitoring verdict. We also develop and implement an opportunistic monitoring framework that leverages existing synchronization points to synchronize thread local monitors with a global monitor. This framework allows for the monitoring of global properties without the need for additional synchronization mechanisms that could disrupt program execution. Our contributions are evaluated through extensive experiments on various benchmarks, and real-world and synthetic applications from the literature. We also utilize BISM in the broader context of dynamic analysis, particularly in log analysis, testing coverage, and profiling. Collectively, these contributions enhance the reliability and efficiency of runtime monitoring for concurrent programs. We substantiate our theoretical claims with implemented solutions, providing practical tools for the advancement of the field.

• Print
• Share
• Share on Facebook
• Share on Twitter
• Share on LinkedIn
• Share url