Field-programmable gate arrays (FPGAs) are hardware circuits that can be reconfigured by a system user after being deployed. FPGAs are a compelling alternative architecture that may allow hardware performance to continue to improve at a dramatic rate. Unfortunately, systems that incorporate an FPGA may allow a potentially untrusted user to reprogram hardware after it has been deployed. Such a scenario enables novel security attacks that can leak a user's private information or corrupt critical information stored on a system, but are performed entirely in hardware. This project develops an approach for ensuring that FPGAs satisfy strong security policies even when programmed by an untrusted user that will incur no overheard for runtime performance. This research investigates techniques that automatically infer proofs of information-flow properties of circuits. This project designs and implements policy languages, proof languages, checking-circuit synthesizers, and proof generators, which in combination will dramatically improve the security of FPGA-based systems. These techniques will enable devices and data-centers to use FPGAs in novel circuit designs that satisfy strong, precise security guarantees and can be updated dynamically.
STARSS: Small: Self-reliant Field-Programmable Gate Arrays