In-system formal verification

Abstract

The utilization of field-programmable gate arrays (FPGAs) in cyber-physical systems embedded into the environment is rising as they provide high performance, parallelism, and adaptability. On the one hand, this creates new opportunities, such as the possibility of updating the reconfigurable hardware parts of the system after deployment. On the other hand, those system alterations entail significant challenges, especially for verifying mixed-criticality systems. Post- deployment hardware updates of mixed-criticality systems are problematic, as those systems are often certified to allow their operation in safety-critical environments. The re-certification after updates is time-consuming, costly, and requires tremendous effort, especially if the system is deployed in the field or inaccessible, resulting in a high demand to prevent re-certification. In this work we aim to develop a methodology to potentially avoid re-certifications after reconfigurable hardware updates. We propose a method for in-field formal bitstream verification for mixed-criticality systems, and we evaluate this method on a proof-of-concept implementation. The presented method extracts the netlist of a bitstream and performs formal property checking. We use SystemVerilog assertion (SVA) properties to create a safety specification for our experiments. At the moment, properties are specified manually, but could be derived from a safety standard in the future (if safety standards evolve to be more formal). We then use satisfiability modulo theories (SMT) solvers for the formal verification and show that our method can verify a bitstream’s conformance to a safety specification. In the future, this would mean that a toolchain qualification and certification of the SVA properties could potentially avoid re-certification after updating reconfigurable hardware and enable easy regression tests. We perform a feasibility study to evaluate the performance of our method. This feasibility study analyzes an intelligent traffic light controller, arithmetical logical units (ALUs), and a packet buffer counter with different bit-width. We use a Raspberry Pi model 3b+ with a Raspbian operating system (OS) as an experimental setup. Our experiments present evidence of the methodologies’ correct functionality and provide an extensive benchmark of the verification times when executed on a Raspberry Pi. For instance, the method takes under 30 seconds to verify a 16-bit packet-buffer counter thoroughly. Also, we demonstrate the influence of different SMT solvers on the verification time on the sample of Boolector, Yices2, and Z3 and show that we can reduce the verification time by 69% using the appropriate solver for the respective problem. To allow an estimation of the expected verification time, we suggest estimation methods and introduce an estimation score to ease its determination.We conclude that our method is potentially feasible for safety-critical systems if verification time is irrelevant. Our experimental results indicate the possibility of verifying designs with arbitrary size and complexity in-field if there is enough time to solve the formal problem. For safety-critical systems, this trade-off is realistic considering that we can potentially avoid costly re-certification.

Die Anwendung von Field-Programmable Gate Arrays (FPGAs) in cyberphysischen Systemen nimmt aufgrund ihrer hohen Performance, des Parallelismus und ihrer Adaptierbarkeit, stark zu. Einerseits schafft dies neue Möglichkeiten, wie beispielsweise die Rekonfigurierbarkeit der Hardware. Andererseits zieht eine erneute Programmierung, vor allem bei sicherheitskritischen Systemen, signifikante Herausforderungen nach sich. Hardware-Updates, die nach der Inbetriebnahme erfolgen, sind besonders problematisch, da sicherheitskritische Systeme meist zertifiziert sind um den Betrieb in sicherheitsrelevanten Umgebungen zu ermöglichen. Wenn die Systeme bereits im Feld im Einsatz oder überhaupt unzugänglich sind, ist eine Neuzertifizierung nach einem Update aufwändig, kosten- und zeitintensiv. Deshalb ist der Bedarf eine erneute Zertifizierung zu verhindern groß. Das Ziel dieser Arbeit ist, eine Methodik zu entwickeln, die potentiell dafür geeignet ist eine erneute Zertifizierung nach einem Hardwareupdate zu verhindern. Wir schlagen eine Methode zur formalen Bitstream-Verifizierung für sicherheitskritische Systeme im Feld vor und evaluieren diese Methode anhand einer Proof-of-Concept Implementierung. Die präsentierte Methodik extrahiert die Netzliste des Bitstreams und verifiziert diese durch formales Property-Checking. Wir verwenden SystemVerilog As- sertion (SVA) Objekte, um eine Sicherheitsspezifizierung für unsere Experimente zu erstellen. Im Moment wird dieser Vorgang noch manuell durchgeführt, in der Zukunft jedoch könnten die SVA Objekte von einem Sicherheitsstandard abgeleitet werden (falls die Standards formaler werden). Danach verwenden wir Satisfiablity Modulo Theories (SMT) Solver für die formale Verifizierung und zeigen, dass unsere Methode die Konformität des Bitstreams zur Sicherheitsspezifizierung überprüfen kann. Für die Zukunft bedeutet das, dass eine Toolchain-Qualifizierung und eine Zertifizierung der SVA Objekte zusammen mit unserer Methodik potentiell dazu in der Lage sind, eine erneute Zertifizierung des Systems zu verhindern und Regressionstests zu erleichtern. Wir führen eine Machbarkeitsstudie durch und evaluieren die Performance unserer Methode. Unsere Machbarkeitsstudie analysiert eine intelligente Verkehrsampelsteuerung, eine arithmetische logische Recheneinheit (ALU) und einen Paketpufferzähler in verschiedenen Bitweiten. Als experimentellen Aufbau verwenden wir einen Raspberry Pi 3 (Modell B+) mit einem Raspbian Betriebssystem. Unsere Experimente zeigen die korrekte Funktionalität unserer Methodik und stellen eine umfangreiche Benchmark der auf dem Raspberry Pi benötigten Verifizierungszeiten zur Verfügung. Um einen 16-Bit Paketpufferzähler vollständig zu verifizieren benötigt unsere Methode weniger als 30 Sekunden. Zusät- zliches demonstrieren wir den Einfluss der Verwendung verschiedener SMT-Solver auf die Verifizierungszeit. Am Beispiel der SMT-Solver Boolector, Yices2 und Z3 zeigen wir, dass durch die Wahl, des zum jeweiligen Problem passenden Solvers, die Verifizierungszeit um bis zu 69% reduziert werden kann. Um eine Einschätzung der zu erwartenden Verifizierungszeit durchführen zu können, führen wir einen Schätzfaktor ein um die Ermittlung zu erleichtern. Zusammenfassend stellen wir fest, dass - wenn die dafür benötigte Zeit nicht entscheidend ist - unsere Methode zur Verifizierung von sicherheitskritischen Systemen potentiell sehr gut geeignet ist. Unsere Experimente legen nahe, dass mit unserer Methodik die Möglichkeit besteht, beliebig große und komplexe Designs im Feld zu verifizieren, falls genug Zeit zur Verfügung steht um das formale Problem zu lösen. Für sicherheitskritische Systeme ist dieser Trade-Off realistisch, weil eine erneute, aufwändige Zertifizierung des Systems potentiell vermieden werden könnte.