"Crafting Secure Systems from the Gates Up"

Abstract:

Program analyses and hardware working together can yield vital insights into complex problems. I will demonstrate this by examining a basic question in computer security: how does information flow inside a machine? Answers to this question are key to achieving true isolation and protected communication, yet capturing all digital flows in a provable manner has long been an open problem.

In this talk, I will present an analysis technique and an architecture that are co-designed to yield a system verifiably free from all digital information leaks.

The verification technique, GLIFT, analyzes complete systems at the level of individual bits and logic gates. GLIFT works on the insight that all  information flows, whether implicit, timing, or explicit, look surprisingly similar at the gate level where weakly defined assembly language descriptions give way to precise logical functions.  By exposing all flows, GLIFT converts the problem of looking for information leaks into writing bit-level assertions that can be automatically checked using standard hardware design tools.

The Execution Lease architecture allows programmers to explicitly control the flow of secret or untrusted information, even with performance optimizations like caches and predictors. It supports a complete embedded system, including a small separation kernel that directly manages all micro-architectural state, and an I/O sub-system that shares a bus among off-the-shelf devices of different security domains. While strict in ways required to cover all flows, the system is both programmable and capable of performing useful computation. This embedded system, all implemented and tested on an FPGA, is then automatically verified to enforce the information flow policy of non-interference using GLIFT. 

Bio

Mohit Tiwari is a Computing Innovation Fellow at University of California, Berkeley. He received his PhD in Computer Science from University of California, Santa Barbara in 2011. His research uses computer architecture and program analyses to build secure, reliable systems, and has received a Best Paper award at PACT 2009, an IEEE Micro Top Pick 2010, and the Outstanding Dissertation award in Computer Science at UCSB in 2011. 

___________________________________________________________________________