Proof-Carrying Hardware: A Novel Approach to Reconfigurable Hardware Security

FPGAs, systems on chip and embedded systems are nowadays irreplaceable. They combine the computational power of application specific hardware with software-like flexibility. At runtime, they can adjust their functionality by downloading new hardware modules and integrating their functionality. Due to their growing capabilities, the demands made to reconfigurable hardware grow. Their deployment in increasingly security critical scenarios requires new ways of enforcing security since a failure in security has severe consequences. Aside from financial losses, a loss of human life and risks to national security are possible. With this work I present the novel and groundbreaking concept of proof-carrying hardware. It is a method for the verification of properties of hardware modules to guarantee security for a target platform at runtime. The producer of a hardware module delivers based on the consumer's safety policy a safety proof in combination with the reconfiguration bitstream. The extensive computation of a proof is a contrast to the comparatively undemanding checking of the proof. I present a prototype based on open-source tools and an abstract FPGA architecture and bitstream format. The proof of the usability of proof-carrying hardware provides the evaluation of the prototype with the exemplary application of securing combinational and bounded sequential equivalence of reference monitor modules for memory safety.

---

FPGAs, System on Chips und eingebettete Systeme sind heutzutage kaum mehr wegzudenken. Sie kombinieren die Rechenleistung von spezialisierter Hardware mit einer Software-ähnlichen Flexibilität. Zur Laufzeit können sie ihre Funktionalität anpassen, indem sie online neue Hardware Module beziehen und deren Funktionalität integrieren. Mit der Leistung wachsen auch die Anforderungen an rekonfigurierbare Hardware. Ihr Einsatz in immer sicherheitskritischeren Szenarien erfordert neue Wege um Sicherheit zu gewährleisten, da ein Versagen der Sicherheit gravierende Folgen mit sich bringt. Neben finanziellen Verlusten sind auch der Verlust von Menschenleben oder Einbußen in der nationalen Sicherheit denkbar. In dieser Arbeit stelle ich das neue und wegweisende Konzept der beweistragenden Hardware vor. Es ist eine Methode zur Verifizierung von Eigenschaften von Hardware Modulen um die Sicherheit der Zielplatformen zur Laufzeit zu garantieren. Der Produzent eines Hardware Moduls liefert, basierend auf den Sicherheitsbestimmungen des Konsumenten, einen Beweis der Sicherheit mit dem Rekonfigurierungsbitstrom. Die aufwendige Berechnung des Beweises steht im Kontrast zu der vergleichsweise unaufwendigen Überprüfung durch den Konsumenten. Ich präsentiere einen Prototypen basierend auf Open Source Werkzeugen und einer eigenen abstrakten FPGA Architektur samt Bitstromformat. Den Nachweis über die Nutzbarkeit von beweistragender Hardware erbringt die Evaluierung des Prototypen zur beispielhaften Anwendung der Sicherung von kombinatorischer und begrenzt sequenzieller Äquivalenz von Referenzmonitor-Modulen zur Speichersicherheit.