ÜBERSPARK : Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor
Abstract
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.
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.
Research Areas
