Secure Composition of Systems and Policies - October 2016

Public Audience
Purpose: To highlight progress. Information is generally at a higher level which is accessible to the interested public.

PI(s): Anupam Datta, Limin Jia
Co-PI(s):
Researchers:

Hard Problems Addressed

Scalability and Composability

Our work addresses the Scalability and Composability problem. The reasoning principles we are developing will allow both sequential and parallel composition of arbitrary number of verified and unverified system program modules in varying configurations. Our program logic takes into consideration that components execute in a potentially adversarial environment (e.g., untrusted system modules), and therefore, the compositionality of components in the presence of such adversaries is built into our semantic model.

Publications

UberSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor. Amit Vasudevan, Sagar Chaki, Petros Maniatis, Limin Jia and Anupam Datta. To appear in proceedings of the 25th USENIX Security Symposium (August 10-12, 2016)

A Logic of Programs with Interface-confined Code. Limin Jia, Shayak Sen, Deepak Garg, and Anupam Datta. In proceedings of Computer Security Foundations Symposium (CSF) (July 14-18, 2015)

Key Highlights

It is difficult to compositionally verify security properties of extensible commodity systems software (e.g., BIOS, OS, hypervisor) written in low-level languages. We are developing a system called UberSpark that enforces verifiably secure-object abstractions in systems software written in C99 and assembly. UberSpark enforces abstractions found in higher-level languages (e.g., interfaces, function-call semantics for implementations of interfaces, access control on interfaces, forms of concurrency) using a combination of hardware mechanisms and light-weight static analysis. UberSpark also provides a restricted language called CASM to make assemblyverifiable via tools aimed at C99, while retaining its performance and low-level access to hardware. The CASM code is then compiled using the certifying CompCert compiler into executable binaries. After verification, The C code is compiled using a certifying compiler while the CASM code is translated into its corresponding assembly instructions.

Collectively, these abstractions enable compositional verification of security invariants without sacrificing performance.

We have validated UberSpark by building and verifying security invariants of a performant hypervisor and several of its extensions, and demonstrating only minor performance overhead, and low verification costs. We are presently evaluating UberSpark in the context of other interesting application domains such as password hashing and secure cloud based web-services with associated crypto, and formulating important security invariants including functional properties, memory safety and error correctness.

Complementary to UberSpark is our program logic, System M, that allows proofs of safety for programs that execute adversary-supplied code without forcing the adversarial code to be available for deep typing analysis. The key insight is to model adversary-supplied code based on interface-confinement which reduces the task of reasoning about dynamically obtained adversary code into analysis of invariants over the interfaces the adversarial code is confined to.