ABSTRACT. The EU General Data Protection Regulation (GDPR) is in force as of May 2018. This regulation calls for widespread changes in how personal data is collected, stored, and processed by IT and related systems. I will explain some of the principles behind the GDPR and the security challenges that they entail from the perspectives of static verification, runtime monitoring, and code review. Along the way, I will describe an approach to model-based system audit, and a case study in monitoring substantial parts of the GDPR for an actual system using the MonPoly tool.

ABSTRACT. Cyber-physical systems (CPS) and the Internet-of-Things (IoT) result in a tremendous amount of generated, measured and recorded time-series data. Extracting temporal segments that encode patterns with useful information out of these huge amounts of data is an extremely difficult problem. We propose shape expressions as a declarative formalism for specifying, querying and extracting sophisticated temporal patterns from possibly noisy data. Shape expressions are regular expressions with arbitrary (linear, exponential, sinusoidal, etc.) shapes with parameters as atomic predicates and additional constraints on these parameters. We equip shape expressions with a novel noisy semantics that combines regular expression matching semantics with statistical regression. We characterize essential properties of the formalism and propose an efficient approximate shape expression matching procedure. We demonstrate the wide applicability of this technique on two case studies.

ABSTRACT. Runtime Verification (RV) consists of analyzing execution traces using formal techniques, often including monitoring executions against Linear Temporal Logic (LTL) properties. Propositional LTL is, however, limited in expressiveness, as was first shown by Wolper, where, e.g. it is not being able to express that every even state in a sequence (trace) satisfies a given proposition. Several extensions to propositional LTL, which promote the expressive power to that of regular expressions, have therefore been proposed. However, none of which was, by and large, adopted for RV. In addition, for many practical cases, there is a need in RV to monitor properties that carry data. This problem has been addressed by numerous authors, and in previous work we ourselves addressed this by providing an algorithm that uses BDD-based representation of relations over data elements for monitoring first-order LTL, implemented in the DejaVu tool. In this paper we show, however, that first-order LTL also cannot express Wolper's example, relativized to the first-order case. We suggest an extension of LTL (propositional as well as first-order) with rules to address this limitation in expressiveness. This extension has a simple incremental operational semantics that is suitable for RV. We expand the DejaVu tool to support our extension, and we perform some experiments.

ABSTRACT. Runtime verification tools must correctly establish a specification’s validity or detect violations. This task is difficult, especially when the specification is given in an expressive declarative language that demands a non-trivial monitoring algorithm. We use a proof assistant to not only solve this task, but also to gain confidence in our solution. We formally verify the correctness of a monitor for metric first-order temporal logic specifications using the Isabelle/HOL proof assistant. From our formalization, we extract an executable algorithm with correctness guarantees and use differential testing to find discrepancies in the outputs of two unverified monitors for first-order specification languages.

ABSTRACT. Runtime Verification is the process of deciding whether a run of a program satisfies some property. This work considers the more challenging problem of explaining why a run does or does not satisfy some property. We introduce a new approach to explaining violations of properties in our low-level temporal logic CFTL, motivated by results obtained by applying the related VyPR2 tool to a web service on the CMS Experiment at CERN. Our first contribution is a partial semantics for CFTL which can be used to identify the first observation in a run that causes that run to violate some property. Our second contribution is a technique that allows us to reconstruct execution paths and separate them into good and bad paths. This relies on a notion of severity of violation, allowing us to handle real-time properties sensitive to small variations in timing behaviour. These techniques are implemented as an extension to the publicly available VyPR2 tool. Initial tests show that this can produce useful explanations for realistic use cases.

ABSTRACT. AllenRV is a tool for monitoring temporal specifications, designed for ensuring good scalability in terms of size and number of formulae, and high reactivity. Its features reflect this design goal. For ensuring scalability in the number of formulae, it can simultaneously monitor a set of formulae written in past and future, next-free LTL, with some metric extensions; their efficient simultaneous monitoring is supported by a let construct allowing to share computations between formulae. For ensuring scalability in the size of formulae, it allows defining new abstractions as user-defined operators, which take discrete time boolean signals as arguments, but also constant parameters such as delays. For ensuring high reactivity, its monitoring algorithm does not require clock tick events, unlike many other tools. This is achieved by recomputing output signals both upon input signals changes and upon internally generated timeout events relative to such changes. As a consequence, monitoring remains efficient on arbitrarily fine-grained time domains.

AllenRV is implemented by extending the existing Allen language and compiler, initially targeting ubiquitous applications using binary sensors, with temporal logic operators and a comprehensive library of user-defined operators on top of them. The most complex of these operators, including a complete adaptation of Allen-logic relations as selection operators, are accompanied by formal proofs of their correctness, with respect to their defined semantics.

Thus, AllenRV offers an open platform for cooperatively developing increasingly complex libraries of high level, general or domain-specific, temporal operators and abstractions, without compromising correctness.

ABSTRACT. In this paper, we present NuRV, an extension of the nuXmv model checker to support Runtime Verification (RV). The tool provides commands for offline and online monitoring, as well as monitor code generation. As an online/offline monitor, LTL properties can be verified on finite traces incrementally from the system under scrutiny (SUS). Monitors code can be generated in various programming languages including C, C++, Common Lisp and Java. Furthermore, the monitors can be generated into SMV modules, whose characteristics can be verified by Model Checking in nuXmv. We show the architecture and use scenarios of the tool, and we compare the performance of our generated monitor code in Java with the RV-Monitor. We show that, beside the capacity of generating monitors from long LTL formulae, our Java-based monitors are about 200x faster than RV-Monitor at generation-time and 2-5x faster at runtime.

ABSTRACT. This paper presents a benchmark generator, Timescales, which can be used to evaluate the performance and scalability of runtime verification tools using Metric Temporal Logic (MTL) formulas as their specifications. We mainly target runtime verification of cyber-physical systems and generate traces similar to the qualitative behavior of sensor readings and state variables of such systems that are observed/sampled continuously. Since such systems are composed of many heterogeneous components that work over very different time scales, it is crucial to measure the performance of the MTL monitoring tool for a wide range of timing parameters in specifications. Therefore, Timescales supports the generation of benchmarks for 10 typical timed properties for any given trace length and timing parameters with several other useful features. Finally, we provide some default benchmark suites generated by Timescales and demonstrate the evaluation of an RV tool using them.

ABSTRACT. Runtime enforcement and control system synthesis are two verification techniques that automate the process of transforming an erroneous system into a valid one. As both techniques can modify the behaviour of a system to prevent erroneous executions, they are both ideal for ensuring safety. In this paper, we investigate the interplay between these two techniques and identify control system synthesis as being the static counterpart to suppression-based runtime enforcement, in the context of safety properties.

ABSTRACT. This paper presents an application of specification based runtime verification techniques to control mobile robots in a reactive manner. In our case study, we develop a layered control architecture where runtime monitors constructed from formal specifications are embedded into the navigation stack. We use temporal logic and regular expressions to describe safety requirements and mission specifications, respectively. An immediate benefit of our approach is that it leverages simple requirements and objectives of traditional control applications to more complex specifications in a non-intrusive and compositional way. Finally, we demonstrate a simulation of robots controlled by the proposed architecture and we discuss further extensions of our approach.