arXiv subjects

Roderick Bloem

Publications and source records attributed to Roderick Bloem.

At least 19 recordsLinked to original sources

arXiv2026

Sharing The Secret: Distributed Privacy-Preserving Monitoring

In traditional runtime verification, a system is typically observed by a monolithic monitor. Enforcing privacy in such settings is computationally expensive, as it necessitates heavy cryptographic primitives. Therefore, privacy-preserving monitoring remains impractical for real-time applications. In this work, we address this scalability challenge by distributing the monitor across multiple parties -- at least one of which is honest. This architecture enables the use of efficient secret-sharing schemes instead of computationally intensive cryptography, dramatically reducing over-head while maintaining strong privacy guarantees. While existing secret-sharing approaches are typically limited to one-shot executions which do not maintain an internal state, we introduce a protocol tailored for continuous monitoring that supports repeated evaluations over an evolving internal state (kept secret from the system and the monitoring entities). We implement our approach using the MP-SPDZ framework. Our experiments demonstrate that, under these architectural assumptions, our protocol is significantly more scalable than existing alternatives.

cs.CR↗

arXiv2025

Parameterized Infinite-State Reactive Synthesis

We propose a method to synthesize a parameterized infinite-state systems that can be instantiated for different parameter values. The specification is given in a parameterized temporal logic that allows for data variables as well as parameter variables that encode properties of the environment. Our synthesis method runs in a counterexample-guided loop consisting of four main steps: First, we use existing techniques to synthesize concrete systems for some small parameter instantiations. Second, we generalize the concrete systems into a parameterized program. Third, we create a proof candidate consisting of an invariant and a ranking function. Fourth, we check the proof candidate for consistency with the program. If the proof succeeds, the parameterized program is valid. Otherwise, we identify a parameter value for which the proof fails and add a new concrete instance to step one. To generalize programs and create proof candidates, we use a combination of anti-unification and syntax-guided synthesis to express syntactic differences between programs as functions of the parameters. We evaluate our approach on examples from the literature that have been extended with parameters as well as new problems.

cs.LO↗

arXiv2023

Safety Shielding under Delayed Observation

Agents operating in physical environments need to be able to handle delays in the input and output signals since neither data transmission nor sensing or actuating the environment are instantaneous. Shields are correct-by-construction runtime enforcers that guarantee safe execution by correcting any action that may cause a violation of a formal safety specification. Besides providing safety guarantees, shields should interfere minimally with the agent. Therefore, shields should pick the safe corrective actions in such a way that future interferences are most likely minimized. Current shielding approaches do not consider possible delays in the input signals in their safety analyses. In this paper, we address this issue. We propose synthesis algorithms to compute \emph{delay-resilient shields} that guarantee safety under worst-case assumptions on the delays of the input signals. We also introduce novel heuristics for deciding between multiple corrective actions, designed to minimize future shield interferences caused by delays. As a further contribution, we present the first integration of shields in a realistic driving simulator. We implemented our delayed shields in the driving simulator \textsc{Carla}. We shield potentially unsafe autonomous driving agents in different safety-critical scenarios and show the effect of delays on the safety analysis.

cs.AI↗

arXiv2023

A Systematic Approach to Automotive Security

We propose a holistic methodology for designing automotivesystems that consider security a central concern at every design stage.During the concept design, we model the system architecture and definethe security attributes of its components. We perform threat analysis onthe system model to identify structural security issues. From that analysis,we derive attack trees that define recipes describing steps to successfullyattack the system's assets and propose threat prevention measures.The attack tree allows us to derive a verification and validation (V&V)plan, which prioritizes the testing effort. In particular, we advocate usinglearning for testing approaches for the black-box components. It consistsof inferring a finite state model of the black-box component from its executiontraces. This model can then be used to generate new relevanttests, model check it against requirements, and compare two differentimplementations of the same protocol. We illustrate the methodologywith an automotive infotainment system example. Using the advocated approach, we could also document unexpected and potentially criticalbehavior in our example systems.

cs.CR↗

arXiv2022

Automata Learning meets Shielding

Safety is still one of the major research challenges in reinforcement learning (RL). In this paper, we address the problem of how to avoid safety violations of RL agents during exploration in probabilistic and partially unknown environments. Our approach combines automata learning for Markov Decision Processes (MDPs) and shield synthesis in an iterative approach. Initially, the MDP representing the environment is unknown. The agent starts exploring the environment and collects traces. From the collected traces, we passively learn MDPs that abstractly represent the safety-relevant aspects of the environment. Given a learned MDP and a safety specification, we construct a shield. For each state-action pair within a learned MDP, the shield computes exact probabilities on how likely it is that executing the action results in violating the specification from the current state within the next $k$ steps. After the shield is constructed, the shield is used during runtime and blocks any actions that induce a too large risk from the agent. The shielded agent continues to explore the environment and collects new data on the environment. Iteratively, we use the collected data to learn new MDPs with higher accuracy, resulting in turn in shields able to prevent more safety violations. We implemented our approach and present a detailed case study of a Q-learning agent exploring slippery Gridworlds. In our experiments, we show that as the agent explores more and more of the environment during training, the improved learned models lead to shields that are able to prevent many safety violations.

cs.LG↗

arXiv2022

Online Shielding for Reinforcement Learning

Besides the recent impressive results on reinforcement learning (RL), safety is still one of the major research challenges in RL. RL is a machine-learning approach to determine near-optimal policies in Markov decision processes (MDPs). In this paper, we consider the setting where the safety-relevant fragment of the MDP together with a temporal logic safety specification is given and many safety violations can be avoided by planning ahead a short time into the future. We propose an approach for online safety shielding of RL agents. During runtime, the shield analyses the safety of each available action. For any action, the shield computes the maximal probability to not violate the safety specification within the next $k$ steps when executing this action. Based on this probability and a given threshold, the shield decides whether to block an action from the agent. Existing offline shielding approaches compute exhaustively the safety of all state-action combinations ahead of time, resulting in huge computation times and large memory consumption. The intuition behind online shielding is to compute at runtime the set of all states that could be reached in the near future. For each of these states, the safety of all available actions is analysed and used for shielding as soon as one of the considered states is reached. Our approach is well suited for high-level planning problems where the time between decisions can be used for safety computations and it is sustainable for the agent to wait until these computations are finished. For our evaluation, we selected a 2-player version of the classical computer game SNAKE. The game represents a high-level planning problem that requires fast decisions and the multiplayer setting induces a large state space, which is computationally expensive to analyse exhaustively.

cs.LG↗

arXiv2022

Threat Repair with Optimization Modulo Theories

We propose a model-based procedure for automatically preventing security threats using formal models. We encode system models and potential threats as satisfiability modulo theory (SMT) formulas. This model allows us to ask security questions as satisfiability queries. We formulate threat prevention as an optimization problem over the same formulas. The outcome of our threat prevention procedure is a suggestion of model attribute repair that eliminates threats. Whenever threat prevention fails, we automatically explain why the threat happens. We implement our approach using the state-of-the-art Z3 SMT solver and interface it with the threat analysis tool THREATGET. We demonstrate the value of our procedure in two case studies from automotive and smart home domains, including an industrial-strength example.

cs.CR↗

arXiv2022

Correct-by-Construction Runtime Enforcement in AI -- A Survey

Runtime enforcement refers to the theories, techniques, and tools for enforcing correct behavior with respect to a formal specification of systems at runtime. In this paper, we are interested in techniques for constructing runtime enforcers for the concrete application domain of enforcing safety in AI. We discuss how safety is traditionally handled in the field of AI and how more formal guarantees on the safety of a self-learning agent can be given by integrating a runtime enforcer. We survey a selection of work on such enforcers, where we distinguish between approaches for discrete and continuous action spaces. The purpose of this paper is to foster a better understanding of advantages and limitations of different enforcement techniques, focusing on the specific challenges that arise due to their application in AI. Finally, we present some open challenges and avenues for future work.

cs.AI↗

arXiv2022

Conformance Testing of Mealy Machines Under Input Restrictions

We introduce a grey-box conformance testing method for networks of interconnected Mealy Machines. This approach addresses the scenario where all interfaces of the component under test are observable, but its inputs are under the control of other white-box components. We prove new conditions for full fault detection that exploit repetitions across branching executions of the composite machine in a novel way.Finally, we provide experimental evaluation of our approach on cascade compositions of up to a thousand states, and show that it notably out-performs existing black-box testing techniques.

cs.FL↗

arXiv2021

Reactive Synthesis Modulo Theories Using Abstraction Refinement

Reactive synthesis builds a system from a specification given as a temporal logic formula. Traditionally, reactive synthesis is defined for systems with Boolean input and output variables. Recently, new theories and techniques have been proposed to extend reactive synthesis to data domains, which are required for more sophisticated programs. In particular, Temporal stream logic(TSL) (Finkbeiner et al. 2019) extends LTL with state variables, updates, and uninterpreted functions and was created for use in synthesis. We present a synthesis procedure for TSL(T), an extension of TSL with theories. Synthesis is performed using a counter-example guided synthesis loop and an LTL synthesis procedure. Our method translates TSL(T) specifications to LTL and extracts a system if synthesis is successful. Otherwise, it analyzes the counterstrategy for inconsistencies with the theory. If the counterstrategy is theory-consistent, it proves that the specification is unrealizable. Otherwise, we add temporal assumptions and Boolean predicates to the TSL(T) specification and start the next iteration of the the loop. We show that the synthesis problem for TSL (T) is undecidable. Nevertheless our method can successfully synthesize or show unrealizability of several non-Boolean examples.

cs.LO↗

arXiv2021

Proving SIFA Protection of Masked Redundant Circuits

Implementation attacks like side-channel and fault attacks pose a considerable threat to cryptographic devices that are physically accessible by an attacker. As a consequence, devices like smart cards implement corresponding countermeasures like redundant computation and masking. Recently, statistically ineffective fault attacks (SIFA) were shown to be able to circumvent these classical countermeasure techniques. We present a new approach for verifying the SIFA protection of arbitrary masked implementations in both hardware and software. The proposed method uses Boolean dependency analysis, factorization, and known properties of masked computations to show whether the fault detection mechanism of redundant masked circuits can leak information about the processed secret values. We implemented this new method in a tool called Danira, which can show the SIFA resistance of cryptographic implementations like AES S-Boxes within minutes.

cs.CR↗

arXiv2021

TEMPEST -- Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments

We present Tempest, a synthesis tool to automatically create correct-by-construction reactive systems and shields from qualitative or quantitative specifications in probabilistic environments. A shield is a special type of reactive system used for run-time enforcement; i.e., a shield enforces a given qualitative or quantitative specification of a running system while interfering with its operation as little as possible. Shields that enforce a qualitative or quantitative specification are called safety-shields or optimal-shields, respectively. Safety-shields can be implemented as pre-shields or as post-shields, optimal-shields are implemented as post-shields. Pre-shields are placed before the system and restrict the choices of the system. Post-shields are implemented after the system and are able to overwrite the system's output. Tempest is based on the probabilistic model checker Storm, adding model checking algorithms for stochastic games with safety and mean-payoff objectives. To the best of our knowledge, Tempest is the only synthesis tool able to solve 2-1/2-player games with mean-payoff objectives without restrictions on the state space. Furthermore, Tempest adds the functionality to synthesize safe and optimal strategies that implement reactive systems and shields

cs.LO↗

arXiv2021

Minimization and Synthesis of the Tail in Sequential Compositions of Mealy Machines

We consider a system consisting of a sequential composition of Mealy machines, called head and tail. We study two problems related to these systems. In the first problem, models of both head and tail components are available, and the aim is to obtain a replacement for the tail with the minimum number of states. We introduce a minimization method for this context which yields an exponential improvement over the state of the art. In the second problem, only the head is known, and a desired model for the whole system is given. The objective is to construct a tail that causes the system to behave according to the given model. We show that, while it is possible to decide in polynomial time whether such a tail exists, there are instances where its size is exponential in the sizes of the head and the desired system. This shows that the complexity of the synthesis procedure is at least exponential, matching the upper bound in complexity provided by the existing methods for solving unknown component equations.

cs.FL↗

arXiv2020

Online Shielding for Stochastic Systems

In this paper, we propose a method to develop trustworthy reinforcement learning systems. To ensure safety especially during exploration, we automatically synthesize a correct-by-construction runtime enforcer, called a shield, that blocks all actions that are unsafe with respect to a temporal logic specification from the agent. Our main contribution is a new synthesis algorithm for computing the shield online. Existing offline shielding approaches compute exhaustively the safety of all states-action combinations ahead-of-time, resulting in huge offline computation times, large memory consumption, and significant delays at run-time due to the look-ups in a huge database. The intuition behind online shielding is to compute during run-time the set of all states that could be reached in the near future. For each of these states, the safety of all available actions is analysed and used for shielding as soon as one of the considered states is reached. Our proposed method is general and can be applied to a wide range of planning problems with stochastic behavior. For our evaluation, we selected a 2-player version of the classical computer game SNAKE. The game requires fast decisions and the multiplayer setting induces a large state space, computationally expensive to analyze exhaustively. The safety objective of collision avoidance is easily transferable to a variety of planning tasks.

cs.LO↗

arXiv2020

Safety Synthesis Sans Specification

We define the problem of learning a transducer ${S}$ from a target language $U$ containing possibly conflicting transducers, using membership queries and conjecture queries. The requirement is that the language of ${S}$ be a subset of $U$. We argue that this is a natural question in many situations in hardware and software verification. We devise a learning algorithm for this problem and show that its time and query complexity is polynomial with respect to the rank of the target language, its incompatibility measure, and the maximal length of a given counterexample. We report on experiments conducted with a prototype implementation.

cs.FL↗

arXiv2020

Adaptive Testing for Specification Coverage

Ensuring correctness of cyber-physical systems (CPS) is an extremely challenging task that is in practice often addressed with simulation based testing. Formal specification languages, such as Signal Temporal Logic (STL), are used to mathematically express CPS requirements and thus render the simulation activity more systematic and principled. We propose a novel method for adaptive generation of tests with specification coverage for STL. To achieve this goal, we devise cooperative reachability games that we combine with numerical optimization to create tests that explore the system in a way that exercise various parts of the specification. To the best of our knowledge our approach is the first adaptive testing approach that can be applied directly to MATLAB\texttrademark\; Simulink/Stateflow models. We implemented our approach in a prototype tool and evaluated it on several illustrating examples and a case study from the avionics domain, demonstrating the effectiveness of adaptive testing to (1) incrementally build a test case that reaches a test objective, (2) generate a test suite that increases the specification coverage, and (3) infer what part of the specification is actually implemented.

cs.SE↗

arXiv2020

Adaptive Shielding under Uncertainty

This paper targets control problems that exhibit specific safety and performance requirements. In particular, the aim is to ensure that an agent, operating under uncertainty, will at runtime strictly adhere to such requirements. Previous works create so-called shields that correct an existing controller for the agent if it is about to take unbearable safety risks. However, so far, shields do not consider that an environment may not be fully known in advance and may evolve for complex control and learning tasks. We propose a new method for the efficient computation of a shield that is adaptive to a changing environment. In particular, we base our method on problems that are sufficiently captured by potentially infinite Markov decision processes (MDP) and quantitative specifications such as mean payoff objectives. The shield is independent of the controller, which may, for instance, take the form of a high-performing reinforcement learning agent. At runtime, our method builds an internal abstract representation of the MDP and constantly adapts this abstraction and the shield based on observations from the environment. We showcase the applicability of our method via an urban traffic control problem.

cs.LO↗

arXiv2020

It's Time to Play Safe: Shield Synthesis for Timed Systems

Erroneous behaviour in safety critical real-time systems may inflict serious consequences. In this paper, we show how to synthesize timed shields from timed safety properties given as timed automata. A timed shield enforces the safety of a running system while interfering with the system as little as possible. We present timed post-shields and timed pre-shields. A timed pre-shield is placed before the system and provides a set of safe outputs. This set restricts the choices of the system. A timed post-shield is implemented after the system. It monitors the system and corrects the system's output only if necessary. We further extend the timed post-shield construction to provide a guarantee on the recovery phase, i.e., the time between a specification violation and the point at which full control can be handed back to the system. In our experimental results, we use timed post-shields to ensure the safety in a reinforcement learning setting for controlling a platoon of cars, during the learning and execution phase, and study the effect.

cs.LO↗