A Formal Specification of the NOVA Microhypervisor ABI

We present a formal specification for the NOVA microhypervisor that handles concurrency and architectural behaviors. Our specification combines an operational specification for unprivileged user code with a separation logic specification of privileged state and operations. We find that the small footprint and open world nature of separation logic makes the specification highly modular and reasonably high level. Furthermore, we describe several uses of the specification for verifying applications that use NOVA.