A Formal Specification of the NOVA Microhypervisor

We present a formal specification of NOVA that captures its complex concurrent and architectural behavior. Our specification combines an operational specification for unprivileged user code with a separation logic specification of privileged state and operations. The specification precisely captures the subtle behaviors of NOVA such as address translation and user faults. Separation logic’s small footprint and open world nature makes the specification highly modular and reasonably high level, allowing us to abstract architectural details that are encapsulated by NOVA and evolve the formal specification as NOVA evolves. Using the specification, we have carried out proofs of the NOVA source code as well as of applications running on top of NOVA.