Introduction
Using deductive formal methods for ProvenCore, a secure operating system with a high-level interface for applications and for ProvenVisor, a secure hypervisor, makes it possible to reach a higher level of security while reducing the total costs of security.
What we have done
We have developed a secure OS called ProvenCore as well as a secure hypervisor called
ProvenVisor. In both cases, the objective is to use deductive formal methods. In the case of
ProvenCore we produced proofs that can be automatically verified by a computer. Here are the
simplified steps of the development:
- Designing the high-level model of the operating system we are aiming for, simple yet
expressive enough for a human to convince himself that it is what he expects of an
operating system with the necessary features, - Formally proving some security properties, namely isolation, confidentiality and
integrity, on the high-level security model, - Writing the actual code for the operating system,
- Formally proving that the code implements the high-level model.
By composition, the security properties hold for the actual code of the operating system