-
Article
Open AccessOnline 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 ...
-
Chapter and Conference Paper
A Systematic Approach to Automotive Security
We propose a holistic methodology for designing automotive systems that consider security a central concern at every design stage. During the concept design, we model the system architecture and define the sec...
-
Chapter and Conference Paper
Provable Correct and Adaptive Simplex Architecture for Bounded-Liveness Properties
We propose an approach to synthesize Simplex architectures that are provably correct for a rich class of temporal specifications, and are high-performant by optimizing for the time the advanced controller is acti...
-
Chapter and Conference Paper
Attribute Repair for Threat Prevention
We propose a model-based procedure for preventing security threats using formal models. We encode system models and threats as satisfiability modulo theory (SMT) formulas. This model allows us to ask security...
-
Article
Open AccessProving 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 implemen...
-
Article
Open AccessSpecifiable robustness in reactive synthesis
When synthesizing a system from a given specification, there is room for automatically adding various requirements, hence improving the resulting system. One such requirement covered extensively in past litera...
-
Chapter and Conference Paper
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...
-
Chapter
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...
-
Article
Open AccessVacuity in synthesis
In reactive synthesis, one begins with a temporal specification \(\varphi \) φ ...
-
Article
Open AccessTwo SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional formulas with existential an...
-
Chapter and Conference Paper
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 speci...
-
Chapter and Conference Paper
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 implemen...
-
Chapter and Conference Paper
Learning Mealy Machines with One Timer
We present Mealy machines with a single timer (MM1Ts), a class of models that is both sufficiently expressive to describe the real-time behavior of many realistic applications, and can be learned efficiently. ...
-
Chapter and Conference Paper
Online Shielding for Stochastic Systems
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 shiel...
-
Article
Preface for the SYNT
-
Chapter and Conference Paper
Shield Synthesis for Reinforcement Learning
Reinforcement learning algorithms discover policies that maximize reward. However, these policies generally do not adhere to safety, leaving safety in reinforcement learning (and in artificial intelligence in ...
-
Chapter and Conference Paper
Placement of Runtime Checks to Counteract Fault Injections
Bitflips form an increasingly serious problem for the correctness and security of software and hardware, whether they occur inadvertently as soft errors or on purpose as fault injections. Error Detection Codes...
-
Article
Open AccessSynthesizing adaptive test strategies from temporal logic specifications
Constructing good test cases is difficult and time-consuming, especially if the system under test is still under development and its exact behavior is not yet fixed. We propose a new approach to compute test s...
-
Chapter and Conference Paper
Efficient Information-Flow Verification Under Speculative Execution
We study the formal verification of information-flow properties in the presence of speculative execution and side-channels. First, we present a formal model of speculative execution semantics. This model can b...
-
Chapter and Conference Paper
Run-Time Optimization for Learned Controllers Through Quantitative Games
A controller is a device that interacts with a plant. At each time point, it reads the plant’s state and issues commands with the goal that the plant operates optimally. Constructing optimal controllers is a f...
