We present überSpark (üSpark), an innovative architecture for compositional
verification of security properties of extensible hypervisors written in C and
Assembly. üSpark comprises two key ideas: (i) endowing low-level system software
with abstractions found in higher-level languages (e.g., objects, interfaces,
function-call semantics for implementations of interfaces, access control on
interfaces, concurrency and serialization), enforced using a combination of
commodity hardware mechanisms and light-weight static analysis; and (ii)
interfacing with platform hardware by programming in Assembly using an idiomatic
style (called CASM) that is verifiable via tools aimed at C, while retaining its
performance and low-level access to hardware. After verification, the C code is
compiled using a certified compiler while the CASM code is translated into its
corresponding Assembly instructions. Collectively, these innovations enable
compositional verification of security invariants without sacrificing performance.
We validate üSpark by building and verifying security invariants of an existing
open-source commodity x86 micro-hypervisor and several of its extensions, and
demonstrating only minor performance overhead with low verification costs.