Verifikation der Sicherheit und Funktionalität von RISC-V-Cores

Die Verifikation der Prozessorhardware gehört zu den am schwersten zu lösenden Aufgaben, denen sich Entwickler bei der Verifikation aktueller Prozessordesigns stellen müssen. Fortschrittliche Funktionen wie mehrstufige Pipelines, mehrstufige Caches, Out-of-Order-Ausführung, Sprungvorhersage, spekulative Ausführung und Pre-Fetching sind schwer zu entwickeln und noch schwerer zu verifizieren.

Es gibt viele Kombinationen von Verhaltensweisen und außergewöhnlichen Randbedingungen, die sich mit hoher Wahrscheinlichkeit nicht gründlich genug mit Hilfe Constrained Random Testbenches verifizieren lassen. Das uneingeschränkte Vertrauen in ein Prozessordesign setzt daher eine formale Verifikation voraus, die sicherstellt, dass die Hardware nicht nur das tut, was sie tun soll, sondern auch, dass sie nichts tut, was sie nicht tun soll. Nur so ist gewährleistet, dass ein Design funktional korrekt, sicher und vertrauenswürdig ist. Die Verifikation ist bei RISC-V-Prozessorkerndesigns (Bild 1) besonders herausfordernd, da es viele Anbieter und viele Implementierungsvarianten gibt. Es wird eine gemeinsame Verifikationsmethode benötigt, die sowohl für Anbieter von RISC-V-Cores als auch für System-on-Chip-Teams (SoC-Teams), die diese Kerne integrieren, verfügbar ist.

Das sind die Herausforderungen bei der Verifikation von RISC-V-Cores

2010 wurde an der University of California in Berkeley das RISC-V-Projekt mit dem Zweck gegründet, eine RISC ISA (Reduced Instruction Set Computer, Bfehlssatzarchitektur) der fünften Generation zu definieren und zu implementieren. Zu den selbst gesteckten Zielen gehörte unter anderem die Unterstützung einer großen Bandbreite an Implementierungen, die sich in verschiedenen Endanwendungen einsetzen ließen.

Die dafür erforderliche Flexibilität des RISC-V führte zu drei Merkmalen, die eine Verifikation der Designs besonders erschweren. Erstens besitzt die definierte Befehlssatzarchitektur viele optionale Eigenschaften und mögliche Variationen. Der Prozessor verfügt über 32 Register, die 32 Bit, 64 Bit oder 128 Bit breit sein können. Der grundlegende Befehlssatz "I" hat eine optionale "E"-Version, die nur über 16 32-Bit-Register verfügt und für eingebettete Anwendungen konzipiert ist. Zusätzliche Befehle, die unterstützt werden können, sind:

• die “M”-Erweiterung für die Multiplikation/Division ganzer Zahlen
• die “A”-Erweiterung für atomare Speicherzugriffe
• die “F”-Erweiterung für Gleitkomma-Berechnung (32 Bit)
• die “D”-Erweiterung für Gleitkomma-Berechnung (64 Bit)
• die “Q”–Erweiterung für Gleitkomma-Berechnung (128 Bit)
• die “C”-Erweiterung für komprimierte Berechnung (16 Bit)

Die optionalen Gleitkommabefehle fügen 32 weitere Register mit entsprechender Breite hinzu. Die RISC-V-ISA definiert drei Privilegierungsstufen, neun Ausnahmen in Verbindung mit privilegierten Befehlen und 4.096 Steuer- und Statusregister (CSRs). Das macht deutlich, dass schon die Überprüfung der Konformität mit der ISA eine große Herausforderung darstellt. Die vollständige Verifikation eines RISC-V-Kerns auf funktionale Korrektheit geht jedoch noch darüber hinaus. Die ISA erlaubt die Definition eigener Befehle. Auch diese müssen verifiziert werden, um sicherzustellen, dass sie korrekt funktionieren und dabei nicht die Konformität der Standardbefehle verletzen.

Zweitens wurde die RISC-V-ISA so konzipiert, dass sie auf viele verschiedene Mikroarchitekturen abgebildet werden kann - von kleinen Controllern bis hin zu Multi-Core-Implementierungen mit den fortschrittlichsten Prozessorfunktionen. Ein Core-Anbieter muss in der Lage sein, nicht nur die ISA-Konformität, sondern das gesamte Design einschließlich der mikroarchitektonischen Details zu verifizieren. Darüber hinaus möchte ein Core-Integrator möglicherweise einen Abnahmetest anbieten, für den er einen Teil der Verifikationsschritte oder den kompletten Verifikationsprozess wiederholen möchte. Drittens muss jeder Entwurf auf Register-Transfer-Level (RTL) statisch analysiert werden, um häufige Kodierungsfehler zu beseitigen.

Dabei kann nur ein Verfahren auf Basis formaler Technik alle Anforderungen erfüllen, die ein RISC-V-Core an die Verifikation stellt. Jeder Ansatz, der auf Simulation oder Emulation basiert, kann dagegen nur einen marginalen Prozentsatz der Designfunktionalität untersuchen. Mit Hilfe von Constrained Random Testbenches lässt sich nicht garantieren, dass alle Hardwarefehler aufgedeckt werden, nur formale Tests können diesen Nachweis liefern. Entsprechend kann nur eine formale Verifikation die Abwesenheit von etwas beweisen.

Im vorliegenden Fall die Absenz von Designbestandteilen, die für Endanwendungen mit hohen Sicherheits- oder Vertrauensanforderungen ein Risiko darstellen könnten. Eine solche formal-basierte Methode existiert. Sie ist bereits bei mehreren RISC-V-Core-Designs zur Anwendung gekommen. Diese Methode deckt die funktionale Korrektheit, die Sicherheit und die Vertrauenswürdigkeit von RISC-V-Designs ab und kann sowohl von Core-Anbietern als auch von Core-Integratoren eingesetzt werden.

Für die Verifikation der Mikroarchitektur muss der Prozess unter anderem mit dem RTL-Code des Kerns, den formal erfassten ISA-Compliance-Regeln und Informationen des Core-Anbieters zu Designentscheidungen, wie der Anzahl der Pipeline-Stufen, gefüttert werden. Dann unterstützt die Methode das ganze Spektrum der RISC-V-Verifikation und erfüllt alle skizzierten Herausforderungen.

Das Herzstück des Verfahrens ist die Formalisierung der RISC-V-ISA in Form einer Menge von SystemVerilog Assertions (SVA) unter Verwendung einer neuartigen "Operational Assertion"-Bibliothek (Bilder 2 und 3). Dieser Ansatz definiert High-Level-Transaktionen ähnlich präzise wie Timing-Diagramme und ist ideal, um die erwarteten Ergebnisse für Prozessorbefehle zu erfassen.

Jeder Befehl in der RISC-V-ISA wird in einer einzelnen Operational Assertion erfasst, die für jede mikroarchitektonische Implementierung des Befehls gilt. Formale Engines verifizieren, dass der Prozessorzustand bei jedem Befehl nach der Ausführung mit der Spezifikation übereinstimmt. Da dieser Ansatz formal arbeitet, findet er alle Fehler in Bezug auf die funktionale Korrektheit und beweist dann, dass keine weiteren Fehler existieren. Er ist flexibel genug, um anwenderspezifische Erweiterungen, die über die ISA hinausgehen, zu handhaben.

Die formalen Engines verifizieren den kompletten RISC-V-Kern einschließlich der Mikroarchitektur und gehen damit über die Prüfung der ISA-Konformität hinaus. Die Methode sieht auch die Durchführung einer statischen Analyse des Kerns vor, um häufige Designfehler zu finden. Diese reichen von einfachen Syntaxfehlern und Tippfehlern im RTL-Code bis hin zu Schwachstellen, die den finalen Chip gefährden könnten.

Dieser Prozess ist vollständig automatisiert, so dass viele Design-Teams den RTL-Code jedes Mal vor dem Einchecken in ein Revisionskontrollsystem anstoßen.

Einige Anwendungen für RISC-V-Prozessoren haben strenge Sicherheitsanforderungen, damit böswillige Angreifer keine im Design vorhandenen Schwachstellen ausnutzen können. Die Sicherheitsüberprüfung muss einen strengen Prozess beinhalten, der alle Fehler und Schwachstellen erkennt und genau festlegt, was im Design vorkommen kann und was nicht. Die formalbasierte RISC-V-Verifikationsmethode beinhaltet eine Vielzahl automatisierter Prüfungen des Core-RTL-Designs, die schnell viele Klassen häufiger Codierungs- und Designfehler eliminiert. Zu diesen Prüfungen gehören:

• Strukturelle Analyse: syntaktische und semantische Analyse des Quellcodes
• Sicherheitsprüfungen: erschöpfende Verifikation der Abwesenheit allgemeiner Probleme beim Betrieb sequenzieller Designs
• Aktivierungsprüfungen: Nachweis, dass alle Designfunktionen ausgeführt werden können und nicht durch nicht erreichbaren Code blockiert sind

Einige der durch diese Prüfungen aufgedeckten Probleme stellen Sicherheitsrisiken dar, die von Angreifern ausgenutzt werden könnten. Ein unvollständiger Case-Befehl lässt z. B. offen, was passiert, wenn ein unerwarteter Wert auftritt. Solche Probleme können bereits in einem frühen Stadium des Entwurfsprozesses automatisch gefunden und behoben werden.

Vertrauenswürdigkeit der RISC-V-Cores überprüfen

Ungewollte Schwachstellen sind besorgniserregend, aber absichtlich eingefügter bösartiger Code (Hardware-Trojaner) ist ein noch größeres Problem für vertrauenskritische Anwendungen, wie es autonome Fahrzeuge und Kernkraftwerke sind. Der Entwicklungsprozess für Prozessorkerne und SoCs ist komplex und bietet oft mehrere Einfallstore für die Einführung von Trojanern.

So können sich während der Logiksynthese Probleme einschleichen, entweder durch absichtliches Handeln oder durch Werkzeugprobleme. Die Integration von Cores wie RISC-V-Prozessoren stellt ein zusätzliches Risiko dar, da das SoC-Team die Details dieser Designs nicht kennt. Auch während des Place&Route-Prozesses besteht die Gefahr von Tool-Fehlern oder absichtlichen Netzlistenänderungen. Die RISC-V-Verifikationsmethode umfasst zwei Schritte, um das Vertrauen in einen Prozessorkern zu gewährleisten und auf jedes SoC auszudehnen, in das er integriert wird.

Das Vertrauen in das Design selbst hängt von der Fähigkeit der formalen Verifikation ab, zu erkennen, wann ein Design etwas tun kann, was es nicht tun soll. Über die Überprüfung der Konformität mit der RISC-V-ISA hinaus stellt das Verfahren sicher, dass die Assertions das gesamte Core-Design abdecken. Hier kommt die neuartige GapFreeVerification-Technik ins Spiel (Bild 4), die alle nicht abgedeckten Teile und Fehler bei der Umsetzung der Spezifikation sowie Lücken im Verifikationsplan und nicht verifizierte RTL-Funktionen erkennt und meldet.

Jede unerwartete Funktionalität wird gekennzeichnet, da es sich möglicherweise um einen Hardware-Trojaner handeln könnte, der während des Entwurfsprozesses eingefügt wurde. Core-Anbieter möchten, dass ihren Produkten vertraut wird, und Core-Integratoren möchten diese Vertrauenswürdigkeit möglicherweise selbst überprüfen.

Für den verbleibenden Entwicklungsprozess jenseits der RTL-Phase verwendet die RISC-V-Verifikationsmethode eine formale Äquivalenzprüfung, um sicherzustellen, dass während der Logiksynthese oder des Place&Routing keine neue Logik eingeführt wurde.

Dieser Prozess stellt auch sicher, dass die aggressiven Optimierungen, die während der Implementierung zur Verfügung stehen, für das Design angemessen sind und es nicht auf unerwartete Weise verändert haben. Die Verifikation von Netzlisten nach der Synthese und nach dem Routing gegen die nachweislich korrekte Eingabe-RTL-Spezifikation gewährleistet Vertrauen in jeder Phase des Core- und SoC-Entwicklungsprozesses.

Ergebnisse aus der praktischen Anwendung

Die beschriebene Verifikationsmethode wurde von verschiedenen Design-Teams genutzt und auf verschiedenen RISC-V-Prozessorkern-Implementierungen angewendet. Erkenntnisse aus der Arbeit mit zwei Kernen aus Open Source Repositories können mit der Öffentlichkeit geteilt werden. Der erste ist RI5CY, eine 32-Bit-Implementierung mit einer vierstufigen In-Order-Pipeline (Bild 5).

Er unterstützt die "IMFC"-Befehlssätze sowie benutzerdefinierte Befehlssatzerweiterungen für die Signalverarbeitung. Die RISC-V-Verifizierungsmethode hat bis zum Zeitpunkt der Erstellung dieses Artikels 13 Probleme identifiziert. Diese Probleme wurden an die RI5CY-Entwickler zurückgemeldet, die vier der Probleme als Fehler eingestuft und drei davon behoben haben.

Die restlichen Fälle werden noch untersucht. Zu den gefundenen Problemen gehören:

• Falscher Wert in einen CSR geschrieben
• Zwei Verstöße gegen die Regeln der Ausnahmebehandlung
• Sechs Fälle, in denen Ausnahmen hätten auftreten sollen, aber nicht auftraten
• Falscher dynamischer Fließkommarundungsmodus
• Falsches Ergebnis aus Fließkommaberechnung
• Verletzung der Trap-Rücksprungbehandlung
• CSRs während des Debug-Modus aktualisiert

Das zweite mit der Methode verifizierte Design ist Rocket Core, eine 64-Bit-Implementierung von RISC-V mit einer fünfstufigen Pipeline, bei der pro Zyklus ein Befehl (single issue) gemäß der programmierten Reihenfolge (in-order) abgearbeitet wird (Bild 6).

Er verfügt über eine ausgeklügelte Mikroarchitektur mit Sprungvorhersage, Befehlswiederholung und Out-of-Order-Completion von Befehlen mit langer Latenzzeit, wie eine Division. Es wurden fünf Probleme gefunden und an die Rocket Core-Entwickler gemeldet:

Sprungbefehle speichern unterschiedliche Return-Programmzähler (PC)

• Unzulässige Opcodes werden wiederholt (und dabei Speicherzugriffe erzeugt)
• Ergebnis eines DIV-Befehls (Divide) wird nicht in die Registerdatei geschrieben
• Rücksprung aus dem Debug-Modus ist außerhalb des Debug-Modus ausführbar
• Kern enthält undokumentierten Nicht-Standard-Befehl

Das erste Problem wurde nicht als Fehler eingestuft, da die Befehlsabrufeinheit dafür verantwortlich ist, dies zu verhindern. Das zweite Problem wird noch untersucht. Die restlichen drei Probleme wurden von den Entwicklern als Fehler bestätigt und behoben. Der letzte Fehler ist besonders interessant: Die formalen Engines meldeten, dass der Kern einen unerwarteten Befehl enthielt, bei dem es sich sehr wohl um einen Hardware-Trojaner handeln konnte.

Allerdings stellte sich heraus, dass das Entwicklungsteam einen neuen Befehl hinzugefügt hatte, diese aber noch nicht in der Spezifikation dokumentiert hatte, die das Verifikationsteam zur Entwicklung der Operational Assertions für die benutzerdefinierten Befehle verwendete. Jedes Integrationsteam, das dieselbe Version des Kerns verwendet hätte, wäre mit unbekannter und nicht dokumentierter Funktionalität im Design konfrontiert gewesen. Nur GapFreeVerification hätte bei diesen Anwendungen dies Problem erkennen und aufdecken können.

RISC-V verändert die Prozessor- und SoC-Industrie, stellt aber sowohl Core-Anbieter als auch SoC-Integratoren hinsichtlich der Verifikation vor große Herausforderungen. Die Verifikation muss über die ISA-Konformität hinausgehen und auch die Mikroarchitektur, benutzerdefinierte Anpassungen, die Sicherheit und die Vertrauenswürdigkeit abdecken. In diesem Beitrag wurde eine Methode beschrieben, die das gesamte Spektrum abdeckt.

Die bei der Verifikation zweier populärer Open-Source-RISC-V-Kerne ermittelten Ergebnisse haben den Wert dieser Lösung belegt. Beide wurden mehrfach verifiziert und für die Produktion vorbereitet (tape-out), dennoch fand die Methode noch Designfehler, die von den Prozessorkernentwicklern bestätigt wurden. Es besteht keine Notwendigkeit für Core-Anbieter oder Core-Integratoren, Fehler im Silizium zu finden. Eine von beiden Seiten nutzbare Lösung eines Drittanbieters, die RISC-V-Designs ermöglicht, die die höchsten Standards im Hinblick auf Funktionalität, Sicherheit und Vertrauen erfüllen, ist bereits verfügbar. (na)