Formally verified software in the real world

Abstract

We present an approach for building highly-dependable systems that derive their assurance from a formally-verified operating-system which guarantees isolation between subsystems. We leverage those guarantees to enforce security through non-bypassable architectural constraints, and through generation of code and proofs from the architecture. We show that this approach can produce a system that is highly robust against cyber attacks, even without formal proof of its overall security. We demonstrate not only that this approach is applicable to real-world systems, such as autonomous vehicles, but also that it is possible to re-engineer an existing insecure system to achieve high robustness, and that this can be done by engineers not trained in formal methods.