Runtime Verification

Some reflections on verification and runtime verification in general and of cyber-physical systems in particular.

This paper briefly reports on the first international summer school on Runtime Verification: Branches of practical topics rooted in theory, co-organized and sponsored by COST Action IC1402 ArVi which was held September 23–25, Madrid, Spain as part of the 16th international conference on Runtime Verification (RV 2016).

We report on the Third International Competition on Runtime Verification (CRV-2016). The competition was held as a satellite event of the 16th International Conference on Runtime Verification (RV’16). The competition consisted of two tracks: offline monitoring of traces and online monitoring of Java programs. The intention was to also include a track on online monitoring of C programs but there were too few participants to proceed with this track. This report describes the format of the competition, the participating teams, the submitted benchmarks and the results. We also describe our experiences with transforming trace formats from other tools into the standard format required by the competition and report on feedback gathered from current and past participants and use this to make suggestions for the future of the competition.

Information flow security often involves reasoning about multiple execution traces. This subtlety stems from the fact that an intruder may gain knowledge about the system through observing and comparing several executions. The monitoring of such properties of sets of traces, also known as hyperproperties, is a challenge for runtime verification, because most monitoring techniques are limited to the analysis of a single trace. In this tutorial, we discuss this challenge with respect to HyperLTL, a temporal logic for the specification of hyperproperties.

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.

This paper is an introduction to Complex Event Processing (CEP) intended for an practicioners of Runtime Verification. It first describes typical CEP problems, popular tools and their query languages. It then presents BeepBeep 3, an event stream processor that attempts to bridge the gap between RV and CEP. Thanks to BeepBeep’s generic architecture and flexible input language, queries and properties from both fields can be efficiently processed.

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, ACSL.This paper presents a three-hour tutorial on Frama-C in which 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 PathCrawler. We also emphasize different possible collaborations between these plug-ins and a few others. The presentation is illustrated on concrete examples of C programs.

Software reliability methods, such as testing and model checking, are well integrated into the software development process. They are complemented by safety enforcement mechanisms such as run time verification. However, even with a wealth of techniques and methodologies for developing reliable systems, it is still quite challenging to eliminate all the bugs from software systems. One of the reasons is the magnitude of software systems, having to handle a very large number of use cases and possible interactions with an environment or between concurrent components. Genetic algorithms and programming provide a powerful heuristic search that involves randomization based on operators that simulate natural reproduction. We show various ways where genetic algorithms and programming can be integrated with formal methods to enhance software reliability.

The LogicGuard specification language for the runtime monitoring of message/event streams specifies monitors by predicate logic formulas of a certain kind. In this paper we present an algorithm that gives upper bounds for the space requirements of monitors specified in a formally elaborated core of this language. This algorithm has been implemented in the LogicGuard software and experiments have been carried out to demonstrate the accuracy of its predictions.

We introduce Lola 2.0, a stream-based specification language for the precise description of complex security properties in network traffic. The language extends the specification language Lola with two new features: template stream expressions, which allow input data to be carried along the stream, and dynamic stream generation, where new monitors can be invoked during the monitoring process for the monitoring of new subtasks on their own time scale. Lola 2.0 is simple and expressive: it combines the ease-of-use of rule-based specification languages like Snort with the expressiveness of heavy-weight scripting languages or temporal logics previously needed for the description of complex stateful dependencies and statistical measures. Lola 2.0 specifications are monitored by incrementally constructing output streams from input streams, while maintaining a store of partially evaluated expressions. We demonstrate the flexibility and expressivity of Lola 2.0 using a prototype implementation on several practical examples.

Modern monitoring tools such as our intrusion detection tool Orchids work by firing new monitor instances dynamically. Given an Orchids signature (a.k.a. a rule, a specification), what is the complexity of checking that specification, that signature? In other words, let f(n) be the maximum number of monitor instances that can be fired on a sequence of n events: we design an algorithm that decides whether f(n) is asymptotically exponential or polynomial, and in the latter case returns an exponent d such that $$f(n) = \varTheta (n^d)$$ . Ultimately, the problem reduces to the following mathematical question, which may have other uses in other domains: given a system of recurrence equations described using the operators $$+$$ and $$\max $$ , and defining integer sequences $$u_n$$ , what is the asymptotic behavior of $$u_n$$ as n tends to infinity? We show that, under simple assumptions, $$u_n$$ is either exponential or polynomial, and that this can be decided, and the exponent computed, using a simple modification of Tarjan’s strongly connected components algorithm, in linear time.

We describe an approach to Statistical Model Checking (SMC) that produces not only an estimate of the probability that specified properties (a.k.a. predicates) are satisfied, but also an “input attribution” for those predicates. We use logistic regression to generate the input attribution as a set of linear and non-linear functions of the inputs that explain conditions under which a predicate is satisfied. These functions provide quantitative insight into factors that influence the predicate outcome. We have implemented our approach on a distributed SMC infrastructure, demeter, that uses Linux Docker containers to isolate simulations (a.k.a. trials) from each other. Currently, demeter is deployed on six 20-core blade servers, and can perform tens of thousands of trials in a few hours. We demonstrate our approach on examples involving robotic agents interacting in a simulated physical environment. Our approach synthesizes input attributions that are both meaningful to the investigator and have predictive value on the predicate outcomes.

In cyber-physical systems (CPS), physical behaviors are typically controlled by digital hardware. As a consequence, continuous behaviors are discretized by sampling and quantization prior to their processing. Quantifying the similarity between CPS behaviors and their specification is an important ingredient in evaluating correctness and quality of such systems. We propose a novel procedure for measuring robustness between digitized CPS signals and Signal Temporal Logic (STL) specifications. We first equip STL with quantitative semantics based on the weighted edit distance (WED), a metric that quantifies both space and time mismatches between digitized CPS behaviors. We then develop a dynamic programming algorithm for computing the robustness degree between digitized signals and STL specifications. We implemented our approach and evaluated it on an automotive case study.

Many runtime verification tools for the Java virtual machine rely on aspect-oriented programming, particularly on AspectJ, to weave the verification logic into the observed program. However, AspectJ imposes several limitations on the verification tools, such as a restricted join point model and the inability of weaving certain classes, particularly the Java and Android class libraries. In this paper, we show that our domain-specific aspect language DiSL can overcome these limitations. While offering a programming model akin to AspectJ, DiSL features an extensible join point model and ensures weaving with complete bytecode coverage for Java and Android. We present a new compiler that translates runtime-verification aspects written in AspectJ to DiSL. Hence, it is possible to use existing, unmodified runtime verification tools on top of the DiSL framework to bypass the limitations of AspectJ. As a case study, we show that the AspectJ-based runtime verification tool JavaMOP significantly benefits from the automated translation of AspectJ to DiSL code, gaining increased code coverage. Thanks to DiSL, JavaMOP analyses are able to unveil violations in the Java class library that cannot be detected when using AspectJ.

We propose a notation for specifying event stream abstractions for use in spacecraft telemetry processing. Our work is motivated by the need to quickly process streams with millions of events generated by the Curiosity rover on Mars. The approach builds a hierarchy of event abstractions for telemetry visualization and querying to aid human comprehension. Such abstractions can also be used as input to other runtime verification tools. Our notation is inspired by Allen’s Temporal Logic, and provides a rule-based declarative way to express event abstractions. The system is written in Scala, with the specification language implemented as an internal DSL. It is based on parallel executing actors communicating via a publish-subscribe model. We illustrate the solution with several examples, including a real telemetry analysis scenario.

This paper presents a novel and efficient parallel algorithm for runtime verification of an extension of Ltl that allows for nested quantifiers subject to numerical constraints. Such constraints are useful in evaluating thresholds (e.g., expected uptime of a web server). Our algorithm uses the MapReduce programming model to split a program trace into variable-based clusters at run time. Each cluster is then mapped to its respective monitor instances, verified, and reduced collectively on a multi-core CPU or the GPU. Our experiments on real-world case studies show that the algorithm imposes negligible monitoring overhead.

The increasing complexity and connectivity of modern embedded systems highlight the importance of runtime monitoring to ensure correctness and security. This poses a significant challenge, since monitoring tools can break extra-functional requirements such as timing constraints. Non-intrusive program tracing through side-channel analysis techniques have recently appeared in the literature and constitute a promising approach. Existing techniques, however, exhibit important limitations.In this paper, we present a novel technique for non-intrusive program tracing from power consumption, based on a signals and system analysis approach: we view the power consumption signal as the output of a system with the power consumption of training samples as input. Using spectral analysis, we compute the impulse response to identify the system; the intuition is that for the correct training sample, the system will appear close to a system that outputs a shifted copy of the input signal, for which the impulse response is an impulse at the position corresponding to the shift. We also use the Control Flow Graph (CFG) from the source code to constrain the classifier to valid sequences only, leading to substantial performance improvements over previous works.Experimental results confirm the effectiveness of our technique and show its applicability to runtime monitoring. The experiments include tracing programs that execute randomly generated sequences of functions as well as tracing a real application developed with SCADE. The experimental evaluation also includes a case-study as evidence of the usability of our technique to detect anomalous execution through runtime monitoring.

Online Social Networks (OSNs) are ubiquitous, with more than 70 % of Internet users being active users of such networking services. This widespread use of OSNs brings with it big threats and challenges, privacy being one of them. Most OSNs today offer a limited set of (static) privacy settings and do not allow for the definition, even less enforcement, of more dynamic privacy policies. In this paper we are concerned with the specification and enforcement of dynamic (and recurrent) privacy policies that are activated or deactivated by context (events). In particular, we present a novel formalism of policy automata, transition systems where privacy policies may be defined per state. We further propose an approach based on runtime verification techniques to define and enforce such policies. We provide a proof-of-concept implementation for the distributed social network Diaspora, using the runtime verification tool Larva to synthesise enforcement monitors.

We describe an approach to control-flow integrity protection for real-time systems. We present TrackOS, a security-aware real-time operating system. TrackOS checks a task’s control stack against a statically-generated call graph, generated by an abstract interpretation-based tool that requires no source code. The monitoring is done from a dedicated task, the schedule of which is controlled by the real-time operating system scheduler. Finally, we implement a version of software-based attestation (SWATT) to ensure program-data integrity to strengthen our control-flow integrity checks. We demonstrate the feasibility of our approach by monitoring an open source autopilot in flight.

DTrace, short for “dynamic tracing”, is a powerful diagnostic tool and tracing framework. It is invaluable for performance monitoring, tuning, and for getting insights into almost any aspect of a running system. In this paper we investigate how we can leverage the DTrace operating system-level instrumentation framework [9] to conduct runtime verification. To this end, we develop graphviz2dtrace, a tool for producing monitor scripts in DTrace’s domain-specific scripting language D for specification formulas written in $$\text{ LTL }_{3}$$, a three-valued variety of the well-known Linear Temporal Logic. We evaluate the tool by analyzing a small stack-implementation and a multi-process system.

Linear temporal logic (LTL) is suitable not only for infinite-trace systems, but also for finite-trace systems. Indeed, LTL is frequently used as a trace specification formalism in runtime verification. The completeness of LTL with only infinite or with both infinite and finite traces has been extensively studied, but similar direct results for LTL with only finite traces are missing. This paper proposes a sound and complete proof system for finite-trace LTL. The axioms and proof rules are natural and expected, except for one rule of coinductive nature, reminiscent of the Gödel-Löb axiom. A direct decision procedure for finite-trace LTL satisfiability, a PSPACE-complete problem, is also obtained as a corollary.

Runtime validation of wireless protocol implementations cannot always employ direct instrumentation of the device under test (DUT). The DUT may not implement the required instrumentation, or the instrumentation may alter the DUT’s behavior when enabled. Wireless sniffers can monitor the DUT’s behavior without instrumentation, but they introduce new validation challenges. Losses caused by wireless propagation prevent sniffers from perfectly reconstructing the actual DUT packet trace. As a result, accurate validation requires distinguishing between specification deviations that represent implementation errors and those caused by sniffer uncertainty.We present a new approach enabling sniffer-based validation of wireless protocol implementations. Beginning with the original protocol monitor state machine, we automatically and completely encode sniffer uncertainty by selectively adding non-deterministic transitions. We characterize the NP-completeness of the resulting decision problem and provide an exhaustive algorithm for searching over all mutated traces. We also present practical protocol-oblivious heuristics for searching over the most likely mutated traces. We have implemented our framework and show that it can accurately identify implementation errors in the face of uncertainty.

Existing dynamic determinacy race detectors for task-parallel programs are limited to programs with strict computation graphs, where a task can only wait for its descendant tasks to complete. In this paper, we present the first known determinacy race detector for non-strict computation graphs, constructed using futures. The space and time complexity of our algorithm are similar to those of the classical SP-bags algorithm, when using only structured parallel constructs such as spawn-sync and async-finish. In the presence of point-to-point synchronization using futures, the complexity of the algorithm increases by a factor determined by the number of future task creation and get operations as well as the number of non-tree edges in the computation graph. The experimental results show that the slowdown factor observed for our algorithm relative to the sequential version is in the range of 1.00$$\times $$ – 9.92$$\times $$, which is in line with slowdowns experienced for strict computation graphs in past work.

Most existing specification languages for runtime verification describe the properties of the entire system in a top-down manner, and lack constructs to describe concurrency in the specification directly. $$ CSP _E$$ is a runtime-monitoring framework based on Hoare’s Communicating Sequential Processes (CSP) that captures concurrency in the specification directly. In this paper, we define the syntax of $$ CSP _E$$ and its formal semantics. In comparison to quantified event automata (QEA), as an example, $$ CSP _E$$ describes a specification for a concurrent system in a bottom-up manner, whereas QEA lends itself to a top-down manner. We also present an implementation of $$ CSP _E$$, which supports full $$ CSP _E$$ without optimization. When comparing its performance to that of QEA, our implementation of $$ CSP _E$$ requires slightly more than twice the time required by QEA; we consider this overhead to be acceptable. Finally, we introduce a tool named stracematch, which is developed using $$ CSP _E$$. It monitors system calls in (Mac) OS X and verifies the usage of file descriptors by a monitored process.

Runtime monitoring has been proposed as an alternative to formal verification for safety critical systems. This paper introduces a decision-theoretic view of runtime monitoring. We formulate the monitoring problem as a Partially Observable Markov Decision Process (POMDP). Furthermore, we adopt a Partially Observable Monte-Carlo Planning (POMCP) to compute an approximate optimal policy of the monitoring POMDP. We show how to construct the POMCP for the monitoring problem and demonstrate experimentally that it can be effectively applied even when some of the state-space variables are continuous, the case where many other POMDP solvers fail. Experimental results on a mobile robot system show the effectiveness of the proposed POMDP-monitor.

Runtime verification focuses on analyzing the execution of a given program by a monitor to determine if it is likely to violate its specifications. There is often an impedance mismatch between the assumptions/model of the monitor and that of the underlying program. This constitutes problems especially for distributed systems, where the concept of current time and state are inherently uncertain. A monitor designed with asynchronous system model assumptions may cause false-positives for a program executing in a partially synchronous system: the monitor may flag a global predicate that does not actually occur in the underlying system. A monitor designed with a partially synchronous system model assumption may cause false negatives as well as false positives for a program executing in an environment where the bounds on partial synchrony differ (albeit temporarily) from the monitor model assumptions.In this paper we analyze the effects of the impedance mismatch between the monitor and the underlying program for the detection of conjunctive predicates. We find that there is a small interval where the monitor assumptions are hypersensitive to the underlying program environment. We provide analytical derivations for this interval, and also provide simulation support for exploring the sensitivity of predicate detection to the impedance mismatch between the monitor and the program under a partially synchronous system.

We propose a framework to solve falsification problems of conditional safety properties—specifications such that “a safety property $$\varphi _{\mathsf {safe}}$$ holds whenever an antecedent condition $$\varphi _{\mathsf {cond}}$$ holds.” In the outline, our framework follows the existing one based on robust semantics and numerical optimization. That is, we search for a counterexample input by iterating the following procedure: (1) pick up an input; (2) test how robustly the specification is satisfied under the current input; and (3) pick up a new input again hopefully with a smaller robustness. In falsification of conditional safety properties, one of the problems of the existing algorithm is the following: we sometimes iteratively pick up inputs that do not satisfy the antecedent condition $$\varphi _{\mathsf {cond}}$$, and the corresponding tests become less informative. To overcome this problem, we employ Gaussian process regression—one of the model estimation techniques—and estimate the region of the input search space in which the antecedent condition $$\varphi _{\mathsf {cond}}$$ holds with high probability.

This work is related to our monitoring tool called ARTiMon for the property monitoring of hybrid systems. We explain how the aggregation operator of its language derives naturally from a generalization of the eventually operator as introduced by Maler and Nickovik for $$MITL_{[a,b]}$$. We present its syntax and its semantics using an interval-based representation of piecewise-constant functions. We define an on-line algorithm for its semantics calculus coupled with an elimination of irrelevant intervals in order to keep the memory resource bounded.

Runtime verification is an approach growing in popularity to verify the correctness of complex and distributed systems by monitoring their executions. Domain Specific Modeling Languages are a technique used for specifying such systems in an abstract way, but still close to the solution domain. This paper aims at integrating runtime verification and domain specific modeling into the development process of complex systems. Such integration is achieved by linking the elements of the system model with the atomic propositions of the temporal correctness properties used to specify monitors. We provide a unified approach used for both the code generation and the simulation of the system through instance model transformations. This unification allows to check correctness properties on different abstraction levels of the modeled system.

This paper shows how runtime monitoring can be applied at different phases of electronic-product development in automotive industry. Starting with concept development, runtime monitors are generated from the product requirements and then embedded in a chip simulation to track the specification compliance at an early stage. In the later phase when a prototype or a product is available, the runtime monitors from the concept development are reused for synthesis into FPGA for monitoring the implementation correctness of the product/system during runtime tests at real-time speeds. This is advantageous for long-term test scenarios where simulation becomes impractical or where evaluation of large amounts of data is required. For example, about 480 K frames/min are exchanged between a sensor and an ECU. This is beyond the capability of an engineer to check the specification conformance of every frame even for one minute of the system run. We embed monitors in a real-world industrial case study, where we runtime-check the requirements of an automotive sensor interface both in simulation and for the test chip.

We present the implementation of an experimental tool that automatically synthesises monitors from specifications written in mHML, a monitorable subset of the branching-time logic $$\mu $$HML. The synthesis algorithm is compositional wrt the structure of the formula and follows closely a synthesis procedure that has been shown to be correct. We discuss how this compositionality facilitates a translation into concurrent Erlang monitors, where each individual (sub)monitor is an actor that autonomously analyses individual parts of the source specification formula while still guaranteeing the correctness of the overall monitoring process.

Two major approaches have emerged in runtime verification, based on synchronous and asynchronous monitoring. Each approach has its advantages and disadvantages and is applicable in different situations. In this paper, we explore a hybrid approach, where low-level properties are checked synchronously, while higher-level ones are checked asynchronously. We present a tool for constructing and deploying monitors based on an architecture specification. Monitor logic and patterns of communication between monitors are specified in a language SMEDL. The language and the tool are illustrated using a case study of a robotic simulator.

Jive is a runtime visualization system that provides (1) a visual representation of the execution of a Java program, including UML-style object and sequence diagrams as well as domain specific diagrams, (2) temporal query-based analysis over program schedules, executions, and traces, (3) finite-state automata based upon key object attributes of interest to the user, and (4) verification of the correctness of program execution with respect to design-time specifications. In this paper we describe the overall Jive tool-chain and its features.

MarQ is a runtime monitoring tool for specifications written as quantified event automata, an expressive automata-based specification language based on the notion of parametric trace slicing. MarQ has performed well in the runtime verification competition and implements advanced indexing and redundancy elimination techniques. This overview describes the basic structure and functionality provided by MarQ and gives a brief description of how to use the tool.

We present R2U2 (Realizable, Responsive, Unobtrusive Unit), a hardware-supported tool and framework for the continuous monitoring of safety-critical and embedded cyber-physical systems. With the widespread advent of autonomous systems such as Unmanned Aerial Systems (UAS), satellites, rovers, and cars, real-time, on-board decision making requires unobtrusive monitoring of properties for safety, performance, security, and system health. R2U2 models combine past-time and future-time Metric Temporal Logic, “mission time” Linear Temporal Logic, probabilistic reasoning with Bayesian Networks, and model-based prognostics.The R2U2 monitoring engine can be instantiated as a hardware solution, running on an FPGA, or as a software component. The FPGA realization enables R2U2 to monitor complex cyber-physical systems without any overhead or instrumentation of the flight software. In this tool exhibition report, we present R2U2 and demonstrate applications on system runtime monitoring, diagnostics, software health management, and security monitoring for a UAS. Our tool demonstration uses a hardware-based processor-in-the-loop “iron-bird” configuration.