Borzoo Bonakdarpour and Bernd Finkbeiner.
Runtime Verification for HyperLTL
Specifying and verifying the correctness of security and privacy polices often involve reasoning about multiple execution traces. This subtlety (e.g., in information flow polices) stems from the fact that an intruder may gain knowledge about the system through observing independent (and not necessarily individual) executions. This tutorial will present in detail (1) HYPERLTL, a temporal logic for specifying such hyperproperties of traces, and (2) runtime verification techniques for monitoring HYPERLTL formulas.
Nikolai Kosmatov and Julien Signoles.
Frama-C, a Collaborative Framework for C Code Verification
Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static and dynamic analysis for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel, and their compliance to a common specification language.
In this three-hour tutorial on Frama-C, we provide a comprehensive overview of its most important plug-ins: the abstract- interpretation based plug-in Value, the deductive verification tool WP, the runtime verification tool E-ACSL and the test generation tool Path-Crawler. We also emphasize different possible collaborations between these plug-ins and a few others. The presentation is illustrated on concrete examples of C programs.
Doron Peled.
Using Genetic Programming for Software Reliability
Formal methods, e.g., testing, runtime and offline verification, can provide the means for manually or automatically enhancing the reliability of programs during the design, development, and even after the system is deployed. Classical software reliability methods are usually based on the theory of automata and logic. As such, they are susceptible to known theoretical bounds. For example, automatic verification of finite state systems (model checking) requires exponential time in the size of the system (and the the temporal specification), and is undecidable for parametric systems. Automatic synthesis of correct-by-design systems is doubly exponential in time in the size of the specification and undecidable for concurrent systems.
In this tutorial, we will present several ways in which ideas from genetic algorithms and genetic programming can be applied to alleviate some of the inherent restrictions of the classical software reliability methods. These ideas are combined with testing and formal verification methods in order to enhance existing methods and create new software reliability techniques.
Sylvain Hallé.
When RV meets CEP
Information systems generate a wealth of information in the form of event traces or logs. The analysis of these logs, either offline or in real-time, can be put to numerous uses: computation of various metrics, detection of anomalous patterns or presence of bugs. To address this general question, two lines of research have evolved in parallel.
On one side is Runtime Verification (RV): runtime monitors such as JavaMOP, LARVA, Logscope, MonPoly, Tracematches, SpoX and PoET are designed with the purpose of detecting violations of some sequential pattern of events generated by a system in realtime. Their specification languages include finite-state automata, temporal logic, μ-calculus, and multiple variations thereof.
On the other side is Complex Event Processing (CEP), which originates from the database community. A typical use case for CEP is that of a system producing a high- volume data stream, such as the record of transactions executed on the stock market. This line of research is rapidly gaining momentum, and has produced software tools like Cayuga, Borealis, TelegraphCQ, Esper, LINQ, VoltDB, and StreamBase SQL. While their input languages vary, most can be seen as database query languages, with added support for computation of aggregate functions (average, minimum, etc.) over sliding windows of events (e.g. all events of the last minute).
It was observed in earlier work [1] that these two classes of systems have complementary strengths. The handling of complex aggregate functions over events provided by CEP tools is notably lacking in most existing runtime monitors. Conversely, monitors generally allow the expression of intricate sequential relationships between events that go far beyond CEP’s traditional capabilities. To summarize, while both fields seek to analyze streams of events, RV tools put more emphasis on their sequencing, while CEP focuses on their data content.
1. S. Hallé. A declarative language interpreter for CEP. In J. Kolb, B. Weber, S. Hallé, W. Mayer, A. K. Ghose, and G. Grossmann, editors, 19th IEEE International Enterprise Distributed Object Computing Workshop, EDOC Workshops 2015, Adelaide, Australia, September 21-25, 2015, pages 156–159. IEEE Computer Society, 2015.
Philip Daian, Dwight Guth, Chris Hathhorn, Yilong Li, Edgar Pek, Manasvi Saxena, Traian Florin Serbanuta and Grigore Rosu.
Runtime Verification at Work: A Tutorial
We present a suite of runtime verification tools developed by Runtime Verification Inc.: RV-Match, RV-Predict, and RV-Monitor. RV-Match is a tool for checking C programs for undefined behavior and other common programmer mistakes. It is extracted from the most complete formal semantics of the C11 language and beats many similar tools in its ability to catch a broad range of undesirable behaviors. RV-Predict is a dynamic data race detector for Java and C/C++ programs. It is perhaps the only tool that is both sound and maximal: it only reports real races and it can find all races that can be found by any other sound data race detector analyzing the same execution trace. RV-Monitor is a runtime monitoring tool that checks and enforces safety and security properties during program execution. Our tools focus on reporting no false positives and are free for non-commercial use.