Bitstream equivalence checking

Abstract

Field-programmable gate arrays (FPGAs) provide high performance for various computing applications while still offering a lot of flexibility throughout their life cycle. Algorithms for FPGAs can be exchanged or optimized at a moments notice by programming the FPGA with a new bitstream. This makes FPGAs a popular option for applications in areas ranging from cloud computing to embedded systems. To obtain the final bitstream, a hardware description language (HDL) design experiences a number of transformations to target a specific FPGA. After each of these transformation steps, engineers can ensure that the transformed design is still functionally equivalent to the HDL through equivalence checks and simulations. After placement and routing, design rule checks and timing simulations ensure the desired behavior. The final step in the process is to encode the design to a bitstream. This bitstream configures the appropriate hardware resources on the FPGA. However, bitstream formats and the accompanying encoding process obfuscate the functionality of the design — thereby masking accidental or maliciously inserted bit flips. Extensive testing in hardware testbeds can help to detect unexpected behavior, but it is expensive and cannot be exhaustive from a certain design size on. In this thesis, we show that it is possible to use design constraints as a ground truth to verify the parametric correctness of encoded bitstreams and develop a general verification flow based on this idea. In short, we perform an equivalence check between the representation before encoding (Xilinx Design Constraint (XDC) and the representation after encoding (FPGA Assembly (FASM)). We use FASM — a file format that describes the configuration of hardware resources on FPGAs — to represent the decoded bitstream and export design constraints before bitstream encoding. The exported design constraints provide transparent information about the last valid snapshot of the resource utilization. Based on mapping rules from design constraints to FASM we can verify that the bitstream represents the correct hardware resources. We implement our flow for the Xilinx 7-series and demonstrate that it reliably detects parametric modifications like re-routed net paths or disconnected Trojan trigger circuits that stay undetected with current verification approaches. This tightens the currently existing verification gap and increases the trust in bitstreams.

Sogenannte FPGAs (Field Programmable Gate Arrays) sind aus Cloud-Computing Anwendungen oder eingebetteten Systemen nicht mehr wegzudenken. Gründe dafür sind unter anderem die hohe Leistungsfähigkeit und Flexibilität für unterschiedliche Rechenanwendungen. Algorithmen können jederzeit verändert und optimiert werden, indem der FPGA mit einem neuen Bitstream programmiert wird. Um einen Bitstream zu erhalten durchläuft eine Schaltung in Hardwarebeschreibungssprache (HDL — Hardware Description Language) mehrere Syntheseschritte um sie an den gewünschten FPGA anzupassen. Nach jedem dieser Schritte kann überprüft werden, ob die funktionelle Äquivalenz zum Ausgangsdesign noch gegeben ist. Entwurfsregelprüfungen (DRC — Design Rule Checks) und Simulationen stellen sicher, dass sich der FPGA wie gewünscht verhält, nachdem alle Hardwareressourcen platziert und verbunden wurden. In einem letzten Schritt wird das Design zu einem Bitstream kodiert. Der Bitstream konfiguriert die einzelnen elektronischen Schaltungen auf dem FPGA. Bitstream Formate oder auch der Kodierungsprozess können jedoch die eigentliche Funktionsweise der Schaltung verschleiern und dabei sogenannte Bitflips — zufällig oder beabsichtigt auftretende — verbergen. Umfangreiche Hardware-Tests können ein unerwartetes Verhalten des FPGA entdecken. Solche Test sind jedoch teuer und ab einer gewissen Designgröße sind allumfassende Tests nicht mehr praktikabel. Die vorliegende Masterarbeit zeigt, dass es möglich ist, die parametrischen Designvorgaben (welche Ressourcen wo am FPGA genutzt werden) als Grundwahrheit zur Überprüfung des kodierten Bitstreams zu nutzen. Weiters wird darauf aufbauend eine allgemeine Vorgehensweise zur Überprüfung von Bitstreams entwickelt. Zur Darstellung des dekodierten Bitstreams nutzen wir FASM, ein Dateiformat, das die Konfiguration der Hardwareres- sourcen auf FPGAs beschreibt. Die parametrischen Designvorgaben exportieren wir vor der Kodierung des Bitstreams. Die parametrischen Designvorgaben liefern Informationen über die letzte gültige Verwendung der Ressourcen auf dem FPGA. Mit Hilfe von Regeln definieren wir den Zusammenhang zwischen parametrischen Designvorgaben und FASM. Dadurch können wir Schlüsse über die korrekte oder inkorrekte Konfiguration der Hardwareressourcen im Bitstream ziehen. Wir implementieren den von uns entwickelten Prozess für die Xilinx 7-Series und zeigen, dass er Veränderungen von Parametern, wie z.B. umgeleitete Signalpfade oder von der Schaltung getrennte trojanische Trigger-Schaltungen zuverlässig erkennt. Bestehende Verifikationsprozesse können diese Veränderungen nicht erkennen. Die vorgestellte Vorgehensweise schließt diese bei aktuellen Methoden bestehende Lücke bei der Verifikation und stärkt somit das Vertrauen in Bitstreams.