Designing Verifiably Secure Systems using Gate-Level Information Flow Tracking


Consumers demand impenetrable security with negligible overhead, neither of which can be provided by a single layer of the system stack. The role of hardware in this equation must change to better address the sophisticated attack methods now available, the new and complex ways that people use their machines, and the increased cost of failure as we move our businesses and lives online. Everything from datacenters and mobile devices to aircraft, automobiles, and banks require new ways of tightly constraining the flow of information such that untrusted and malicious devices can never affect critical system tasks, or that cryptographic secrets can never leak. To create such systems, information flow controls must be incorporated from the ground up, including at hardware design time, in order to provide a formal basis for a system's root of trust. The audience for this tutorial will come away with a better understanding of how to manage information flow at the hardware and architecture levels, the tools and methods now available to verify those designs, and an overview of the many new avenues of research made possible by these advances.

Gate-Level Inforation Flow Tracking (GLIFT)

Conventional software-based security mechanisms can often be foiled by implicit, timing, and covert information flows that stem from very low-level behavior of the hardware. Instead, we will demonstrate a new method for constructing and analyzing architectures capable of tracking all information flow within the machine, including all explicit data transfers and all implicit flows (those subtly devious flows caused by not performing conditional operations). The key to such an approach is a novel gate-level information flow tracking method (GLIFT) which provides a way to compose complex logical structures with well defined information flow properties. Starting from a simple AND gate, we will demonstrate through lecture and exercises, how to create more complex structures including muxes, control, registers, and finally a small microprocessor.

The basic problem of gate-level information flow tracking is to determine, given some input for a and b and their corresponding trust bits a_t and b_t , whether or not the output out is trusted (which is then added as an extra output of the function out_t ). While past approaches have assumed that any use of untrusted data should lead to an untrusted output, we observe that at the gate level this is overly conservative. If one input to an AND gate is 0, the other input can {\em never} affect the result and thus should have no bearing on the trust of the output. As shown in the figure above, this observation is then used to compute the trust of the output (out_t) as a function of the logical inputs (a and b), the trust of those inputs (a_t and b_t), and the truth table of the original function. For complete details, please refer to our papers on the basic GLIFT technique and the Execution Lease CPU, or the short summary published in IEEE Micro.


This tutorial is targeted towards hardware and system-level architects, but should be of interest to anyone that cares about security and works across the hardware-software stack. Specifically, we will address the following two objectives:

  • Present a toolchain to automatically analyze arbitrary system designs expressed in Verilog or VHDL, using example designs such as bus arbiters, cache controllers, and a small microprocessor
  • Demonstrate simple design principles that can be systematically used to create information flow secure systems. Some knowledge of hardware design languages is helpful but not required.
This tutorial primarily focuses on design automation tools and architecture-level security mechanisms, and will conclude with open problems at the compiler, language, and system levels. Expected Duration and Format: 1/2 Day (45 minutes of talk, 45 minutes of demo/exercises in each of the two sessions)