Deductive formal methods


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:

  1. 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,
  2. Formally proving some security properties, namely isolation, confidentiality and
    integrity, on the high-level security model,
  3. Writing the actual code for the operating system,
  4. Formally proving that the code implements the high-level model.
    By composition, the security properties hold for the actual code of the operating system


Leave a Reply