Visible to the public überSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a HypervisorConflict Detection Enabled

TitleüberSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor
Publication TypeConference Paper
Year of Publication2016
AuthorsAmit Vasudevan, Sagar Chaki, Limin Jia, Anupam Datta
Conference Name25th USENIX Security Symposium (USENIX Security 16)
Date Published01/2016
PublisherUSENIX Association
Conference LocationAustin, TX
ISBN Number978-1-931971-32-4
KeywordsCMU, Oct'16

We present uberSpark (uSpark), an innovative architecture for compositional verification of security properties of extensible hypervisors written in C and Assembly. uSpark 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 lightweight 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 uSpark 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.

Citation Keynode-30233

Other available formats:

Vasudevan_UberSpark_AD.pdfPDF document466.42 KBDownloadPreview