Describes formal verification in Coq of a model of the commercial NOVA micro-hypervisor. NOVA is a hypervisor in the L4 family that supports DMA access (protected by IOMMU). Very extensive testing is used to compare the model against the actual implementation using over 12 million conformance tests.
The main properties proved are security properties: authority confinement, memory confinement. To support this, they prove invariants: a consistency invariant, no dangling-pointers, semaphore consistency relating thread state to semaphore state, …
This process found around 2 dozen bugs in the hypervisor source code. Half were found during code review as part of the model construction process. Half were found while debugging the model against the implementation. In addition, they found roughly as many bugs in their model. It is not clear whether the construction of proofs found any bugs so I wonder if N-version programming would have most of the same benefit (assuming that the second version is written in an expressive high-level language).
Not mentioned in the paper is that the project was cancelled due to a change in company plans. Unusually, the affiliation on the paper says that the authors’ employers wish to remain anonymous.
Notes related to Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor
Papers related to Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor
- QuickCheck: A lightweight tool for random testing of Haskell programs [claessen:icfp:2000]