Sagar Chaki

Amit Vasudevan, Sagar Chaki, Petros Maniatis, Limin Jia, Anupam Datta, Proceedings of the 25th USENIX Security Symposium (USENIX Security), 2016.

Abstract:We present UberSpark (USpark), an approach for compositional verification of security properties of extensible hypervisors written in C and Assembly. USpark comprises three key ideas: (i) using an architecture that endows low-level systems 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); (ii) enforcing these "secure-object" abstractions using a combination of hardware mechanisms and light-weight static analysis; and (iii) 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 USpark by building and verifying security invariants of an existing open-source x86 micro-hypervisor and several of its extensions, and demonstrating only minor performance overhead, and low verification costs.