Design and Provability of Statically Configurable
Microhypervisors


The creation of formal models for safety-critical system-
level software and the deduction of the equivalence proofs
that link abstract specification and concrete implementation
make up a considerable portion of the total development
process.
We present a hypervisor design based on the paradigm of
maximal staticness and analyze its suitability for the direct
derivation of formal properties.
We find that the design lends itself perfectly to exploration
through symbolic execution, and that its search space is
indeed tractable. Based on this conclusion we present a method
to automatically derive properties like guest noninterference
and kernel integrity for a given instantiation of our
hypervisor directly from its compiled image, i.e. ARMv8
assembly code.
Finally, we touch on the difficulties of adding dynamic
components back into the hypervisor, and we discuss the
obstacles of generating a full formal specification (and thus
a proof of correctness) from the results of symbolic execution.