GLIFT at a High Level
With the end of Dennard Scaling, computer system developers are integrating more application specific functionality in silicon than ever before. At the same time, the integration of general purpose CPUs in all manner of critical systems from automotive control, to medical devices, to avionics, and of course all manners of finance continues to grow. System developers need new methods to help them understand the security properties of their designs, but these properties are a function of both the hardware and the software working together. Since 2006 our team has been examining these issues. The result of this extended research effort has resulted in GLIFT: this first method for analyzing, statically verifying, and dynamically managing the information-flow behavior of mixed hardware/software systems. The big advantages of this approach include:
- An analysis that cuts through all of the layers of digital abstraction -- from the application, through the OS, the firmware, and through machine code, to reveal the true behavior of the actual machine implementation rather than the behavior described by a (potentially out-of-date or imprecise) specification or abstraction.
- We are able to unify and identify all potential digital flows of information including side-channels such as timing and storage channels, implicit flows, and of course all explicit flows. Anything that effects any of the bits, or even the timing of those bits, on the system is captured with our methodology.
- We can prove the absence of these undesired flows of information in a way that other assurance methods that reply on penetration testing and adherence to specific software design practices will simply never be able to achieve. This can be either done dynamically (by adding extra enforcement logic) or statically which, as long as the design is sound, requires no extra GLIFT hardware to be inserted into the production design.
- We can (and do!) build real systems that manage all of these information flows in a reasonable way to implement provable non-interference and one-way information flow policies. We have demonstrated this on numerous occasions, by building cache controllers, USB hubs, networks on chip, and full general purpose microprocessors.
Because this project has progressed significantly over the years, we thought it would be useful to describe the arc this research has taken. Below you can find a high level description of some of the most important GLIFT papers. These are not just copies of the abstracts. Rather they are our thoughts as to what the most important contributions are.
- Mohit Tiwari, Hassan Wassel, Bita Mazloom, Shashidhar Mysore, Frederic Chong, and Timothy Sherwood. Complete Information Flow Tracking from the Gates Up Proceedings of the 14th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), March 2009. Washington, DC
This paper is the first publication of our GLIFT ideas which formalizes the idea of hardware-level information flow tracking. We show how, given a circuit, you can generate a new circuit that describes how information flows through the original circuit. The method can be done either exactly (which requires walking through the truth table) or with a one-sided error (which is compositional and sound -- if we say there is no flow, then there is no flow, but false positives are possible). We propose to generate information tracking logic which can either be built in along with the design, or can be used simply for testing purposes. If the logic is included with the final design (to assist in run-time information flow tracking) rather than just for testing, the overhead is significant (around 1.7x) a number in later papers we are able to bring down to only 2%. We demonstrate this technique on a very restricted and generally horrible little processor (with predication but no general purpose branching). However, this is the first paper to show that timing and storage channels can be unified at the gate level and really set in place the information flow analysis that is the basis for all our future work.
- Mohit Tiwari, Xun Li, Hassan M G Wassel, Frederic T Chong, and Timothy Sherwood. Execution Leases: A Hardware-Supported Mechanism for Enforcing Strong Non-Interference , Proceedings of the International Symposium on Microarchitecture (Micro), December 2009. New York, NY
Here we propose a much better way of designing microprocessors with explicit instructions to help the software manage the information flow of the underlying machine. The instructions implement an idea called "execution leases" through which regions of execution (in both space and time) can be tightly quarantined and their side effects to be tightly bounded. This both a) makes the complete information-flow properties of the machine fully explicit and available to the programmer and b) allows those properties (including properties as strict as non-interference) to be verified all the way down to the gate-level implementation the design. We demonstrate the effectiveness of the resulting design by building a synthesizable prototype of the machine and hand writing software to run on top of it. This is the first paper to show an architecture mechanism that can support policies as strict as non-interference and the first general purpose programmable system to be shown secure with GLIFT.
- Jason Oberg, Wei Hu, Ali Irturk, Mohit Tiwari, Timothy Sherwood, and Ryan Kastner Information Flow Isolation in I2C and USB Proceedings of the 47th Design Automation Conference (DAC) June 2011. San Diego, CA.
In any system, one of the points at which information and agents of different trustworthiness and secrecy must co-mingle is in the communication hardware. Many high-assurance systems today have completely separate buses for "high" and "low" data to prevent an interference, but increasingly engineers are pressured to combine functions in ways that are tough to argue are safe. In this paper we show that it is possible to retrofit a strong notion of security onto existing protocols in such as way that the resulting designs can be verified all the way down to the gate level implementation. We demonstrate this by implementing and verifying an I2C hub (to demonstrate the core ideas) and a USB controller (to show that the ideas can be applied to even modern complex protocols).
- Wei Hu, Jason Oberg, Ali Irturk, Mohit Tiwari, Timothy Sherwood, and Ryan Kastner Theoretical Fundamentals of Gate Level Information Flow Tracking IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD) To appear.
One of the questions left unanswered in the original GLIFT paper was the cost of precision. We knew that it was sound to compose our analysis (we should never get false negatives), but we knew also that composition would introduce false positives in certain cases. For example, an analysis of a MUX that is done on a gate level implementation (the ANDs and ORs implementing the MUX) as opposed to the full truth table of a MUX introduces a false positive when a "tainted" select signal is selecting between to "untainted" signals that are the same value. Intuitively, the select signal can never effect the output and thus does not "taint" the output. In this paper we formalize GLIFT, and find that while it is possible to remove all false positives, the problem of generating the precise taint tracking logic is in co-NP. We further explore the tradeoffs between speed and precision and analyze their cost/effectiveness across a set of circuit benchmarks.
- Mohit Tiwari, Jason Oberg, Xun Li, Jonathan K Valamehr, Timothy Levin, Ben Hardekopf, Ryan Kastner, Frederic T Chong, and Timothy Sherwood. Crafting a Usable Microkernel, Processor, and I/O System with Strict and Provable Information Flow Security Proceedings of the International Symposium of Computer Architecture. (ISCA) June 2011. San Jose, California
One of the concerns when we did the execution leases paper was whether we could really build a full system that could be verified in this way. In this paper we answer those criticisms by designing, testing, and statically verifying the information-flow security of a hardware/software system complete with support for unbounded operation, inter-process communication, pipelined operation, and I/O with traditional devices. The resulting system is provably sound even when adversaries are allowed to execute arbitrary code on the machine, yet is flexible enough to allow caching, pipelining, and other common case optimizations. We implement a micro-kernel for our microprocessor that uses leases to manage shared buffers for provably safe interprocess communication, and we introduce a simple form of abstract interpretation (via *-logic) to allow us to more quickly statically verify the design (which means no special GLIFT logic ever need be introduced to the final design, it can be used for analysis alone).
- Xun Li, Mohit Tiwari, Jason Oberg, Vineeth Kashyap, Frederic T. Chong, Timothy Sherwood, and Ben Hardekopf Caisson: A Hardware Description Language for Secure Information Flow 32nd ACM Conference on Programming Language Design and Implementation. (PLDI) June 2011. San Jose, California
- Hassan Wassel, Ying Gao, Jason Oberg, Ted Huffmire, Ryan Kastner, Frederic Chong, and Timothy Sherwood. SurfNoC: A Low Latency and Provably Non-Interfering Approach to Secure Networks-On-Chip Proceedings of the International Symposium of Computer Architecture. (ISCA) June 2013. Tel Aviv, Israel
- Jason Oberg, Sarah Meiklejohn, Timothy Sherwood, and Ryan Kastner. A Practical Testing Framework for Isolating Hardware Timing Channels The Conference on Design Automation and Test in Europe (DATE) To appear.
Contributors
This work is the result of a great deal of effort across multiple campuses. We have provided below an alphabetic list of the contributors and the institution where their work was done.
- Prof. Frederic Chong, UC Santa Barbara
- Ying Gao, UC Santa Barbara
- Prof. Ben Hardekopf, UC Santa Barbara
- Wei Hu, UC San Diego
- Prof. Ted Huffmire, UC San Diego
- Ali Irturk, UC San Diego
- Prof. Ryan Kastner, UC San Diego
- Vineeth Kashyap, UC Santa Barbara
- Xun Li, UC Santa Barbara
- Bita Mazloom, UC Santa Barbara
- Shashidhar Mysore, UC Santa Barbara
- Jason Oberg, UC San Diego
- Prof. Timothy Sherwood, UC Santa Barbara
- Mohit Tiwari, UC Santa Barbara
- Jonathan K Valamehr, UC Santa Barbara
- Hassan Wassel, UC Santa Barbara