Visible to the public Secure Composition of Systems and Policies - April 2017Conflict Detection Enabled

Submitted by Jamie Presken on Mon, 03/13/2017 - 10:11am

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: Amit Vasudevan (Cylab/CMU), Sagar Chaki (SEI/CMU), Petros Maniatis (Google Inc.)

1) HARD PROBLEMS ADDRESSED

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.

2) PUBLICATIONS (Current Quarter)

N/A this quarter

3) 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 assembly verifiable 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.

4) COMMUNITY ENGAGEMENTS (If applicable)

We have open-sourced and released the first academic prototype of UberSpark. The development and evolution of the framework continues at http://uberspark.org

Our hope, and ultimate vision with UberSpark is to foster the growth of the next generation of systems developers who can design and develop low-level verifiable and trustworthy systems with a focus on verifiability, development compatibility and performance.

5) EDUCATIONAL ADVANCES (If applicable)

N/A

Groups: