Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor

Hanno Becker, Juan Manuel Crespo, Jacek Galowicz, Ulrich Hensel, Yoichi Hirai, César Kunz, Keiko Nakata, Jorge Luis Sacchini, Hendrik Tews, Thomas Tuerk
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 19 November 2019

International Symposium on Formal Methods
Springer
Pages 69-84
2016
Note(s): Operating Systems, security, verification, Coq theorem prover, NOVA hypervisor, hypervisor

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.

NOVA hypervisor

  • QuickCheck: A lightweight tool for random testing of Haskell programs [claessen:icfp:2000]