Designing Verifiably Secure Systems using Gate-Level Information Flow Tracking
Motivation
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.
Tutorial
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.