STARSS: Small: Self-reliant Field-Programmable Gate Arrays

现场可编程门阵列(现场可编程门阵列)是系统用户在部署后可以重新配置的硬件电路。现场可编程门阵列是一种引人注目的替代体系结构，可以使硬件性能继续以惊人的速度提高。不幸的是，结合了FPGA的系统可能允许潜在的不受信任的用户在硬件部署后对其进行重新编程。这样的场景实现了新的安全攻击，这些攻击可以泄露用户的私人信息或破坏存储在系统上的关键信息，但完全在硬件中执行。该项目开发了一种方法，用于确保即使在由不受信任的用户编程时也能满足强大的安全策略，而不会引起运行时性能的无意监听。这项研究调查了自动推断电路信息流特性的证明的技术。该项目设计并实现了策略语言、证明语言、检查电路综合器和证明生成器，这些结合在一起将极大地提高基于FPGA的系统的安全性。这些技术将使设备和数据中心能够在新的电路设计中使用现场可编程门阵列，这些电路设计满足强大、精确的安全保证，并且可以动态更新。

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.