Introduction
The modern world abounds with cyber-physical systems: Software controlling reality, from aircraft and self-driving cars to nuclear plants and smart grids. A big challenge today is how to make these systems correct and safe so that society can reap their full benefits.
VeriPhy fills in one piece of this puzzle. State-of-the-art hybrid systems proving can already rigorously verify rich safety properties of controls interacting with physics, and with a significant degree of automation. Until now, however, realizing strong safety guarantees at the implementation level has been the domain of humans: Guarantees can be automatically transported for weak modeling languages, but no prior tool for expressive models such as hybrid systems keeps correctness guarantees end-to-end. The alternative of implementing a hybrid model by hand is not only time-consuming, but prone to introducing bugs in software which absolutely needs to be correct.
VeriPhy changes that: not only can control software can be generated from safe hybrid models, allowing today's verification technology to see real-world use without the painstaking and error-prone work of implementing models by hand. That control software now comes with rock-solid correctness guarantees for each step of the generation process, crucial when the system being controlled is safety-critical. This verified control serves as sandbox around your existing control software: your controller does whatever it wishes so long as it is knowably safe. When VeriPhy detects danger, it kicks in with provably safe fallback control.
How it Works
VeriPhy is an automatic synthesis pipeline: Verified hybrid systems models enter one end and verified object files come out the other. The verified object files can then be linked with your favorite control software to form a complete system. Along the way, it transforms the model step-by-step to an executable:
- ModelPlex is used to generate monitoring conditions from the source model. These conditions tell us any time your control makes a potentially unsafe action and any time modeling assumptions are violated, so VeriPhy can activate safe fallback control.
- Monitors are translated to executable interval arithmetic.
- Code is generated for a sandbox controller which replaces potentially unsafe actions with verified-safe fallback actions. This code is compiled to machine-level with the verified CakeML compiler.
- The compiled sandbox is linked with a controller written in your favorite language.
Like all good pipelines, you don't have to see what happens inside VeriPhy unless you want to. Whether you look at them or not, VeriPhy produces formal, foundational safety proofs for every step of the process, culminating in an end-to-end safety guarantee: the real system only enters safe states according to the safety specification of the source model. The proofs include:
- Safety of a sandbox controller that monitors an external controller, providing verified fallback control
- Conservative over-approximation with interval arithmetic
- Correct generation of a concrete CakeML implementation
- Correct compilation from CakeML to machine code
These proofs exploit an array of theorem provers (KeYmaera X, Isabelle/HOL, HOL4) in order to productively verify domains ranging from hybrid dynamical systems to real analysis and from word arithmetic to register allocation. To minimize the trusted base in the process, the KeYmaera X core is cross-verified in Isabelle/HOL; the resulting verified core is highly scalable and checks 10,000's of steps per second.
