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:

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.

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.

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).

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.

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).

  • 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