previous day
next day
all days

View: session overviewtalk overview

09:00-10:00 Session 9: Keynote: Safe and Interactive Autonomy: A Journey Starting from Formal Methods, Dorsa Sadigh, Stanford

Abstract: Today’s society is rapidly advancing towards autonomous systems that interact and collaborate with humans, e.g., semiautonomous vehicles interacting with drivers and pedestrians, medical robots used in collaboration with doctors, or service robots interacting with their users in smart homes. With the emergence of autonomous systems in our every day lives, we need to design algorithms and tools that enable safe and seamless interactions with people.

In this talk, I will start with my journey in providing safety for human-robot systems by discussing a spectrum of views on safe autonomous systems including a formal methods perspective for synthesizing provably correct controllers, a robust control approach, and more recent advances in safe learning and verification. I will then discuss one of the main challenges of safety of human-robot systems, i.e., studying how robots influence humans’ actions in one-on-one or group settings. This is usually overlooked by assuming humans act as external disturbances just like moving obstacles, or assuming that automation can always help societies without actually considering how humans can be impacted. I will talk about our recent work in building computational models of human behavior from expert demonstrations and preferences in interaction with autonomous systems and challenges it introduces for safety and robustness verification.

Bio: Dorsa Sadigh is an assistant professor in Computer Science and Electrical Engineering at Stanford University. Her research interests lie in the intersection of robotics, learning and control theory, and algorithmic human-robot interaction. Specifically, she works on developing efficient algorithms for autonomous systems that safely and reliably interact with people. Dorsa has received her doctoral degree in Electrical Engineering and Computer Sciences (EECS) at UC Berkeley in 2017, and has received her bachelor’s degree in EECS at UC Berkeley in 2012. She is awarded the Amazon Faculty Research Award, the NSF and NDSEG graduate research fellowships as well as the Leon O. Chua departmental award.

10:30-12:00 Session 10: Verification of Large Systems
Scalable Translation Validation of Unverified Legacy OS Code

ABSTRACT. Formally verifying functional and security properties of a large-scale production operating system is highly desirable. However, it is challenging as such OSes are often written in multiple source languages that have no formal semantics – a pre-requisite for formal reasoning. To avoid expensive formalization of the semantics of multiple high-level source languages, we present a lightweight and rigorous verification toolchain that verifies OS code at the binary level, targeting ARM machines. To reason about ARM instructions, we first translate the ARM Specification Language (that describes the semantics of the ARMv8 instruction set) into the PVS7 theorem prover and verify the translation. We leverage the radare2 reverse engineering tool to decode ARM binaries into PVS7 and verify the translation. Our translation verification methodology is a lightweight formal validation technique that generates large-scale instruction emulation test lemmas, whose proof obligations are automatically discharged. To demonstrate our verification methodology, we apply the technique on two OSes: Google’s Zircon and a subset of Linux. We extract a set of 370 functions from these OSes, translate them into PVS7, and verify the correctness of translation by automatically generating thousands of proof obligations and tests.

Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity

ABSTRACT. We report on the development of a blockchain system that is significantly verified and performant, detailing the design, proof, and system development based on a process of continuous refinement. We instantiate this framework to build, to the best of our knowledge, the first blockchain (Kaizen) that is performant and verified to a large degree, and a cryptocurrency protocol (KznCoin) over it. We experimentally compare its performance against the stock Bitcoin implementation.

KAIROS: Incremental Verification in High-Level Synthesis through Latency-Insensitive Design

ABSTRACT. High-level synthesis (HLS) improves design productivity by replacing cycle-accurate specifications with untimed or transaction-based specifications. Obtaining high-quality RTL implementations requires significant manual effort from designers, who must manipulate the code and evaluate different HLS-knob settings. These modifications can introduce bugs in the RTL implementations. We present KAIROS, a methodology for incremental formal verification in HLS. KAIROS verifies the equivalence of the RTL implementations the designer subsequently derives from the same specification by applying code manipulations and knobs.

13:30-14:30 Session 12: Security and Safety
Verification of Authenticated Firmware Loaders

ABSTRACT. An important primitive in ensuring security of modern systems-on-chip designs are protocols for authenticated firmware load. These loaders read a firmware binary image from an untrusted input device, authenticate the image using cryptography and load the image into memory for execution if authentication succeeds. While these protocols are an essential part of the hardware root of trust in almost all modern computing devices, verification techniques for reasoning about end-to-end security of these protocols do not exist.

In this paper, we take a step toward addressing this gap by introducing a system model, adversary model and end-to-end security property that enable reasoning about the security of authenticated load protocols. We then present a decomposition of the security property into two simpler hyperproperties. This decomposition enables more scalable verification. Experiments on a protocol model demonstrate viability of the methodology.

Learning-Based Synthesis of Safety Controllers

ABSTRACT. We propose a machine learning framework to synthesize reactive controllers for systems whose interactions with their adversarial environment are modeled by infinite-duration, two-player games over (potentially) infinite graphs. Our framework targets safety games with infinitely many vertices, but it is also applicable to safety games over finite graphs whose size is too prohibitive for conventional synthesis techniques. The learning takes place in a feedback loop between a teacher component, which can reason symbolically about the safety game, and a learning algorithm, which successively learns an overapproximation of the winning set from various kinds of examples provided by the teacher. We develop a novel decision tree learning algorithm for this setting and show that our algorithm is guaranteed to converge to a reactive safety controller if a suitable overapproximation of the winning set can be expressed as a decision tree. Finally, we empirically compare the performance of a prototype implementation to existing approaches, which are based on constraint solving and automata learning, respectively.

15:00-16:30 Session 13: Synthesis for Reactive Systems
Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems

ABSTRACT. Cyber-physical systems are often safety-critical in that violations of safety properties may lead to catastrophes. We propose a method to enforce the safety of systems with real-valued signals by synthesizing a runtime enforcer called the shield. Whenever the system violates a property, the shield, composed with the system, makes correction instantaneously to ensure that no erroneous output is generated by the combined system. While techniques for synthesizing Boolean shields are well understood, they do not handle real-valued signals ubiquitous in cyber-physical systems, meaning corrections may be either unrealizable or inefficient to compute in the real domain. We solve the realizability and efficiency problems by statically analyzing the compatibility of predicates defined over real-valued signals, and using the analysis result to constrain a two-player safety game used to synthesize the shield. We have implemented the method and demonstrated its effectiveness and efficiency on a variety of applications, including an automotive powertrain control system.

Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications
PRESENTER: Philippe Heim

ABSTRACT. We present Syntroids, a case study for the automatic synthesis of hardware from a temporal logic specification. Syntroids is a space shooter acarde game realized on an FPGA, where the control flow architecture has been completely specified in Temporal Stream Logic (TSL) and implemented using reactive synthesis. TSL is a recently introduced temporal logic that separates control and data. This leads to scalable synthesis, because the cost of the synthesis process is independent of the complexity of the handled data. In this case study, we report on our experience with the TSL-based development of the Syntroids game and on the implementation quality obtained with synthesis in comparison to manual programming. We also discuss solved and open challenges with respect to currently available synthesis tools.

Synthesizing Reactive Systems Using a Robustness Specification

ABSTRACT. Past literature on synthesis identified the need to synthesize systems that are robust to failures of the system in reading the inputs from the environment, and also to failures of the environment itself to satisfy our assumptions about its behavior . In this work, we propose a simple and flexible framework for synthesizing more robust systems, where the user defines the required robustness via a temporal robustness specification. For example, the user may specify that the environment is eventually reliable, or that misreadings of the inputs cannot occur more than $k$ consecutive steps, and synthesize a system under this assumption. We show examples of robust systems that we have synthesized with this method by our synthesis tool `Party'.

18:00-21:00 Banquet

Uproar Brewing Company, 439 S 1st St, San Jose