ABSTRACT. We present Barrier-based Simplex (BbSimplex), a new, provably correct design for runtime assurance of continuous dynamical systems. BbSimplex is centered around the Simplex Control Architecture, which consists of a high-performance advanced controller which is not guaranteed to maintain safety of the plant, a verified-safe baseline controller, and a decision module that switches control of the plant between the two controllers to ensure safety without sacrificing performance. In BbSimplex , Barrier certificates are used to prove that the baseline controller ensures safety. Furthermore, BbSimplex features a new automated method for deriving, from the barrier certificate, the conditions for switching between the controllers. Our method is based on the Taylor expansion of the barrier certificate and yields computationally inexpensive switching conditions. We consider a significant application of BbSimplex to a microgrid featuring an advanced controller in the form of a neural network trained using reinforcement learning. The microgrid is modeled in RTDS, an industry-standard high-fidelity, real-time power systems simulator. Our results demonstrate that BbSimplex can automatically derive switching conditions for complex systems, the switching conditions are not overly conservative, and BbSimplex ensures safety even in the presence of adversarial attacks on the neural controller.

ABSTRACT. Kotlin was introduced to Android as the recommended language for development. One of the unique functionalities of Kotlin is that of coroutines, which are lightweight tasks that can run concurrently inside threads. Programming using coroutines is difficult, among other things, because they can move between threads and behave unexpectedly. We introduce runtime verification in Kotlin. We provide a language to write properties and produce runtime monitors tailored to verify Kotlin coroutines. We identify, formalise and runtime verify seven properties about common runtime errors that are not easily identifiable by static analysis. To demonstrate acceptability of the technique in real applications, we apply our framework to an in-house Android app and micro benchmarks, and measure the execution time and memory overheads.

ABSTRACT. We present a Python library for trace analysis called PyContract. PyContract is a shallow internal DSL, in contrast to many trace analysis tools that implement external or deep internal DSLs. The library has been used in a real project for analysis of logs from NASA's Europa Clipper mission. We believe that this opportunity arose largely because of the choice of Python as a host language for the DSL. We describe our design choices, including the argument for developing a Python library, and explain the implementation. The paper includes experiments comparing PyContract against other state-of-the-art tools from the research and industrial communities.

ABSTRACT. Online monitors for first-order specifications may need to store many domain values in their state, requiring significant memory. We propose an approach that compresses the monitor’s state using randomized hash functions. Unlike input sampling, our approach does not require the knowledge of distributions over traces to achieve low error probability. We develop algorithms that insert hash functions into temporal–relational algebra specifications and compute upper bounds on the resulting error probability. We employ a special hashing scheme that allows us to merge values across attributes, which further reduces memory usage. We evaluated our implementation and achieved memory reductions up to 33% when monitoring traces with large domain values, with error probability less than two in a million.

ABSTRACT. We define a fragment of metric first-order temporal logic formulas that guarantees the finiteness of their table representations. We extend our fragment's definition to cover the temporal dual operators trigger and release and show that our fragment is strictly larger than those previously used in the literature. We integrate these additions into an existing runtime verification tool and formally verify in Isabelle/HOL that the tool correctly outputs the table of constants that satisfy the monitored formula. Finally, we provide some example specifications that are now monitorable thanks to our contributions.

ABSTRACT. In the behavioural specification of imperative languages, postconditions may refer to the prestate of the function, usually with an old operator. Therefore, code performing runtime verification has to record prestate values required to evaluate the postconditions, typically by copying part of the memory state, which causes severe verification overhead, both in memory and CPU time.

In this paper, we consider the problem of efficiently capturing prestates in the context of Ortac, a runtime assertion checking tool for OCaml. Our contribution is a postcondition transformation that reduces the subset of the prestate to copy. We formalize this transformation, and we provide proof that it is sound and improves the performance of the instrumented programs. We illustrate the benefits of this approach with a maze generator. Our benchmarks show that unoptimized instrumentation is not practicable, while our transformation restores performances similar to the program without any runtime check.

ABSTRACT. Blockchains are modern distributed systems that provide decentralized financial capabilities with trustable guarantees. Smart contracts are programs written in specialized programming languages running on a blockchain and govern how tokens and cryptocurrency are sent and received. Smart contracts can invoke other contracts during the execution of transactions initiated by external users. Once deployed, smart contracts cannot be modified and their pitfalls can cause malfunctions and losses, for example by attacks from malicious users. Runtime verification is a very appealing technique to improve the reliability of smart contracts. One approach consists of specifying undesired executions (never claims) and detecting violations of the specification on the fly. This can be done by extending smart contracts with additional instructions corresponding to monitor specified properties, resulting in an onchain monitoring approach. In this paper, we study transaction monitoring that consists of detecting violations of complete transaction executions and not of individual operations within transactions. Our main contributions are to show that transaction monitoring is not possible in most blockchains and propose different execution mechanisms that would enable transaction monitoring.

ABSTRACT. Smart contracts exist immutably on blockchains, making their pre-deployment correctness essential. Moreover, they exist openly on blockchains --- open for interaction with essentially any other smart contract and offchain entity. Interaction, for instance with oracles which provide information from off the blockchain, can affect the state of the smart contract, and correctness of these smart contracts may depend on the trustworthiness of the data they manipulate or events they generate which, in turn would depend on which parties or what information contributed to them.

In this paper we develop dynamic taint analysis techniques to enable data tainting in smart contracts. We propose an extension of Solidity that enables labelling inputs of interaction endpoints with dynamic data-carrying labels that capture actionable information about the sender. These labels can then be propagated dynamically across transactions to transitively dependent data. Specifications can then refer to such taints, for instance ensuring that certain data could not have been influenced through interaction by a certain party. We further allow the use of taints as part of the programming language, affecting the control flow of the smart contract. To manage the overheads of such runtime tainting we develop sound static analysis-based techniques to prune away unnecessary instrumentation. We give a case study as a proof-of-concept, and measure the overheads associated with our additions before and after optimisation.

ABSTRACT. Aspect-oriented programming tools aim to provide increased code modularity by enabling programming of cross-cutting concerns separate from the main body of code. Since the inception of runtime verification, aspect-oriented programming has regularly been touted as a perfect accompanying tool, by allowing for non-invasive monitoring instrumentation techniques. In this paper we present our tool, AspectSol, which enables aspect-oriented programming for smart contracts written in Solidity, and then discuss the design space for pointcuts and aspects in this context. We present and evaluate practical runtime verification uses and applications of the tool.

ABSTRACT. Computer Science course instructors routinely have to create comprehensive test suites to assess programming assignments. The creation of such test suites is typically not trivial as it involves selecting a limited number of tests from a set of (semi-)randomly generated ones. Manual strategies for test selection do not scale when considering large testing inputs needed, for instance, for the assessment of algorithms exercises. To facilitate this process, we present TestSelector, a new framework for automatic selection of optimal test suites for student projects. The key advantage of TestSelector over existing approaches is that it is easily extensible with arbitrarily complex code coverage measures, not requiring these measures to be encoded into the logic of an exact constraint solver. We demonstrate the flexibility of TestSelector by extending it with support for a range of classical code coverage measures and using it to select test suites for a number of real-world algorithms projects, further showing that the selected test suites outperform randomly selected ones in finding bugs in students' code.

ABSTRACT. Decent is a benchmark for evaluating decentralized enforcement. It implements two enforcement algorithms that differ in their strategy for correcting the execution: the first one explores all alternatives to perform a globally optimal correction, while the second follows an incremental strategy based on locally optimal choices. Decent allows comparing these algorithms with a centralized enforcement algorithm in terms of computational metrics and metrics for decentralized monitoring such as the number and size of messages, the required computation on each component. Our experiments show that (i) the number of messages sent and the internal memory usage is much smaller with decentralized algorithms (ii) the locally optimal algorithm performs closely to the globally optimal one.

ABSTRACT. Co-simulation allows modelling and analysis of heterogeneous systems: the simulation of a system is achieved through the joint simulation of coupled stand-alone sub-simulators for its individual parts, using a standardized interface (e.g. Functional Mock-up Interface - FMI). Runtime monitoring can be employed to follow the evolution of co-simulation runs, but it is applied only within the scope of individual simulators that may support very diverse monitoring functionalities. This work introduces a technical approach for the runtime verification of properties for the entire co-simulated system. We present the integration of the DejaVU monitor synthesis tool at the master algorithm level of FMI-based co-simulation, such that predicates and events from all constituents of a simulated system can be monitored. Communication between the master and the individual Functional Mock-Up Units (FMUs) is bidirectional, whereas the FMI master does not need to change for monitoring the property of interest. Since FMUs are synchronized by the master algorithm, runtime monitors can be used also as a means to control the co-simulation run. We provide results from co-simulation experiments to give insight into the runtime overhead.