PGSLIFT - pattern graph specification language information flow tracking

Abstract

In dieser Arbeit schlagen wir eine Methode vor, die in der Lage ist Informationsflüsse auf Gatterebene zu verfolgen (GLIFT). Dadurch identifizieren wir Informationsflüsse, welche die Spezifikation eines Hardware-Designs verletzen. Ein solches Informationsleck kann zum Beispiel durch eine fehlerhafte Implementierung oder einen zeitbasierten Seitenkanal entstehen. Auch sind böswillige Änderungen im Entwurfsprozess oder bei der Verwendung von externen Bibliotheken (3PIP) möglich. Gängige Methoden wie GLIFT verfolgen den Einfluss von Information auf Gatterebene um ein Informationsleck aufzuspüren. In diesen Arbeiten fehlt es an einer leicht verständlichen Beschreibungssprache um Sicherheitsrichtlinien zu formulieren und den Entwurf dahingehend zu verifizieren. State-of-the-Art Methoden wie SecVerilog verwenden zum Beispiel die SMT-LIB Syntax in Kombination mit neu eingeführten Sprachkonstrukten. Wir nutzen anstelle der gängigen Methoden die Syntax der “Pattern Graph Specification Language (PGSL)”, einer graphbasierten Suchmethode. Mit ihrer Hilfe erstellen wir eine Sicherheitsrichtlinie, welche eine Hierarchie von Sicherheitsdomänen repräsentiert wie sie beispielsweise vom Sicherheitsmodell Bell-LaPadula verwendet wird. Um Informationslecks auf der Grundlage der Sicherheitsrichtlinien zu identifizieren, fügen wir den Objekten in der Hardwarebeschreibungssprache (HDL) zusätzliche Informationen hinzu, um sie Sicherheitsdomänen zuordnen. Wir verwenden die verfügbare Verilog-Syntax, um den Syntheseprozess außerhalb unserer Methode nicht zu beeinträchtigen.Anhand des Hardware-Trojaners AES128-T100 zeigen wir wie unsere Methode verwendet werden kann. Der Hardware-Trojaner wird dabei von trust-hub.org bereitgestellt. Anschließend fassen wir frühere Arbeiten und Methoden zusammen und präsentieren darauf aufbauend unsere Methode. Außerdem vergleichen wir die von uns entwickelte Methode mit der State-of-the-Art-Methode SecVerilog. Die Ergebnisse zeigen, dass unsere Methode flexibler ist, da die verwendeten Sicherheitsrichtlinien lediglich aus einer einzigen Codezeile bestehen. Anhand eines vereinfachten, beispielhaften Designs, welches einen nicht spezifizierten Informationsfluss zu einem Ausgang aufweist, demonstrieren wir wie wir eine Sicherheitsrichtlinie mit PGSL erstellen. Wir zeigen wie unsere Tools verwendet werden können, um diesen nicht spezifizierten Informationsfluss zu erkennen. Im Anschluss erstellen wir eine modifizierte Version dieses Hardware-Designs, welches der Spezifikation entspricht und somit kein unbeabsichtigter Informationsfluss mehr stattfindet. Hier zeigen wir nun, dass unsere Methode nun keinen Informationsfluss mehr erkennt der die Sicherheitsrichtlinie verletzt und die Methode somit funktioniert.GLIFT fügt dem Hardware-Design Schattenlogik hinzu, die auf der Netzliste auf Gatterebene basiert. Dies erhöht die Komplexität des Designs, welche wir anhand der Anzahl der Zellen und Verbindungen auf Gatterebene messen. Um den Ressourcenverbrauch und die Ausführungszeit eines formalen Verifikationsprozesses zu reduzieren, nutzen wir das Wissen über Sicherheitsdomänen und erstellen Segmente des Designs. Wir analysieren den Anstieg der Ausführungszeit, der durch den Segmentierungsprozess entsteht und führen Experimente durch, die unsere Analysen und Annahmen bestätigen. Sowohl die Erstellung der Schattenlogik als auch die Segmentierung sind von linearer Komplexität f = O(n), wobei n der Anzahl der Zellen und Verbindungen im Design entspricht. Durch den Segmentierungsprozess reduzieren wir die Anzahl der Zellen und Verbindungen in dem Design, was sowohl den Speicherverbrauch als auch die Ausführungszeit von Syntheseprozessen reduziert. Die Segmentierung selbst erhöht jedoch die Ausführungszeit. Wir messen einen Anstieg der Ausführungszeit von maximal 15 %, welcher durch den Segmentierungsprozess verursacht wird. Die Verifikationszeit kann danach, je nach Anzahl der Zellen und Verbindungen die bei der Segmentierung entfernt werden, reduziert werden.Wir messen eine Reduzierung der Verifikationszeit um 5,7 %, wenn 2,1 % der Verbindungen und 0,06 % der Zellen im AES128-T100-Design entfernt werden. Durch diese Reduktion der Verifikationszeit können wir die gesamte Laufzeit unserer Methode um 1,9 % verkürzen.Wir kommen zu dem Schluss, dass unsere Methode in der Lage ist nicht spezifizierte Informationsflüsse mit Hilfe von GLIFT und formaler Verifikation zu identifizieren. Unsere Methode entdeckt solche Informationslecks in allen gewählten Testdesigns die einen solchen Informationsfluss aufweisen.

We propose a method that is capable of performing gate level information flow tracking (GLIFT) using security policies expressed as a pattern graph specification language (PGSL) pattern. Using it we identify information flows violating a hardware design’s specification. Sensitive data is often prohibited from being transferred to certain parts of a hardware design such as an output port. Such an information leak can be the result from different causes, such as implementation errors, timing based side channels or malicious information leaks introduced by third-party IP (3PIP).Different approaches have been published that try to conclude on whether there is an information leak or not. GLIFT as used by SecVerilog tracks the influence of input values to output values on the gate level whereas register transfer level information flow tracking (RTLIFT) tracks information flows on the register transfer level (RTL). GLIFT adds socalled shadow logic to the design based on its initial gate level cells. This increases the complexity of the hardware design which is expressed as the number of cells and wire bits and increases the execution time of operations done on the design and formal verification. The state-of-the-art method SecVerilog uses SMT-LIB syntax combined with nonstandard Verilog syntax. The policies used by SecVerilog are both complicated and can not be modified in a user-friendly way. In those works we identify the lack of a comprehensive description language that allows defining security policies that have high human-readability and are simple to create. We show that we can utilize the syntax of PGSL, a regex like graph search methodology, to create a security policy that represents a hierarchy of security domains. In order to identify information leaks based on this security policy we add information to objects in the design using Verilog attributes. Security labels are introduced to the hardware description language (HDL) using available Verilog syntax that does not interfere with any synthesis process done outside our method. We then use formal verification to identify possible information leaks violating the security policy. To reduce the resource consumption and the execution time of formal verification, caused by the additional design elements originating in shadow logic, we use knowledge of security domains and create segments of the design.We provide a motivating example showing the usage of our method by testing it on a modified version of the hardware Trojan AES128-T100 provided by trust-hub.org. Then we summarize previous work and methods. We further compare our method to the state-of-the-art method SecVerilog. Our results show that our method uses a more human-readable security policy that also allows modifications with less overhead. This increases simplicity and makes our method more simple to use. Further, this potentially reduces human errors at creating security policies.Using an exemplary design that features an unspecified information flow to an output we demonstrate how we compose a security policy using PGSL and show how our tool chain is used to detect this unspecified information flow. After that, we provide a modified version of this hardware design where the information leak is avoided using additional logic. In this design our method does not identify an information leak. These designs also present our benchmarks to validate our methodology. Further, we test our method on the designs AES-T100 and RSA-T100 provided by trust-hub.org and show that it is able to detect information flows.We analyze the execution time overhead created by the segmentation process and perform experiments that confirm our analysis and assumptions. Both shadow logic creation and segmentation are of linear complexity f = O(n) with n being the number of cells and wires in the design. We measure an execution time overhead caused by the segmentation process with a maximum of 15.5 %.Verification time can be reduced based on the number of cells and wire bits that are removed at segmentation. We measure a reduction of 6.4 % in verification time when removing 2.1 % of wire bits and 0.06 % of cells in the AES128-T100 design. Overall the execution time of formal verification could be reduced by 1.9 % using segmentation based on the security policy.We conclude that our method is capable of identifying unspecified information flow using GLIFT and formal verification. In the design AES128-T100 we could identify an information flow in 794 s which we could reduce to 743 s using our segmentation process. Information leaks are detected in all test designs that feature such an information flow.