| Reconfigurable hardware is at the heart of many high-performance embedded systems. Satellites, set-top boxes, electrical power grids, and the Mars Rover all rely on Field Programmable Gate Arrays (FPGAs) to perform their respective functions. Despite the proliferation of reconfigurable devices into critical systems, sound reconfigurable system security remains an unsolved challenge. An FPGA system often has multiple modules (cores) on the same chip that share external resources such as off-chip memory, and these cores operate at different trust levels. While this enables small form factor and low-cost designs, it opens up the opportunity for modules to intercept or even interfere with the operation of each other. Providing a low-cost means to ensure logical isolation of modules is our primary goal, and we will leverage the reconfigurable nature of FPGAs to our advantage in solving this problem.;We propose a novel approach to reconfigurable system security that relies on both static and runtime techniques that work together to isolate the cores. The first element of our isolation strategy is a reference monitor, a runtime mechanism that enforces policies that specify the legal sharing of memory. These policy specifications are expressed as a formal language, and a compiler translates them to a hardware description that can be directly transferred to an FPGA. Our language is powerful enough to express a variety of classic security scenarios. The second element of our strategy is a static technique that uses physical isolation to prevent unintended information flows by surrounding each core with a "moat" that blocks wiring connectivity from the outside. The third element is the detection of possible covert channels in stateful policies by statically analyzing the policy enforced by the reference monitor. This helps to prevent the use of the reference monitor as a covert channel. The fourth element is to make the construction of policies as accurate as possible by providing the embedded systems designer with a higher-level language for expressing security concepts as well as a set of tools that use formal methods to ensure that a policy under construction is mathematically precise. |
