Structured Proofs for Adversarial Cyber-Physical Systems

TL;DR

This paper introduces Kaisar, a new language and tool that simplifies the process of formally verifying safety-critical cyber-physical systems using Constructive Differential Game Logic, enabling structured proofs and high-level reasoning.

Contribution

Kaisar is the first language and tool for CdGL proofs, making formal verification of hybrid games more accessible and structured, especially for CPS safety analysis.

Findings

Kaisar simplifies complex CPS proofs with structured, high-level reasoning.

Reproduced and extended case studies on driving scenarios.

Compared proof metrics and discussed user experiences.

Abstract

Many cyber-physical systems (CPS) are safety-critical, so it is important to formally verify them, e.g. in formal logics that show a model's correctness specification always holds. Constructive Differential Game Logic (CdGL) is such a logic for (constructive) hybrid games, including hybrid systems. To overcome undecidability, the user first writes a proof, for which we present a proof-checking tool. We introduce Kaisar, the first language and tool for CdGL proofs, which until now could only be written by hand with a low-level proof calculus. Kaisar's structured proofs simplify challenging CPS proof tasks, especially by using programming language principles and high-level stateful reasoning. Kaisar exploits CdGL's constructivity and refinement relations to build proofs around models of game strategies. The evaluation reproduces and extends existing case studies on 1D and 2D driving. Proof metrics are compared and reported experiences are discussed for the original studies and their reproductions.