Fuzzing zur Validierung der SoC-Sicherheit. Innovation in der Verifizierung

Beim Fuzzing handelt es sich um die Software-Verifizierung, bei der Randomisierung um die Hardware-Verifizierung. Kann ein Fuzzing-Ansatz die Hardware-Sicherheitstests verbessern? Paul Cunningham (GM, Verification bei Cadence), Raúl Camposano (Silicon Catalyst, Unternehmer, ehemaliger CTO von Synopsys) und ich setzen unsere Reihe über Forschungsideen fort. Feedback ist wie immer willkommen.

Die Innovation

Die Auswahl dieses Monats ist HyperFuzzing für die SoC-Sicherheitsvalidierung. Die Autoren präsentierten dieses Papier auf der ICCAD 2020. Sie stammen vom IIT Kanpur.

Dies ist ein faszinierender Fuzzing-Ansatz, der speziell an das moderne SoC-Design angepasst wurde. Es baut darauf auf Hyper-Eigenschaft Einchecken dynamischer Simulationen. Diese Hypereigenschaften führen zu Verhaltensweisen Sätze von Spuren, ein Ansatz, der sich gut für die Sicherheitsüberprüfung eignet. Als Beispiele nennen die Autoren Informationsflussprüfungen (privilegierte Daten können beispielsweise nicht von A nach B gelangen) und Nichteinmischungsprüfungen (gegnerische Aktionen dürfen den Rechenfluss nicht beeinträchtigen). Anschließend wird die Sicherheit überprüft, indem Bündel von Simulationsspuren mit und ohne Manipulation verglichen werden.

Durch Manipulationen bei diesem Ansatz können verschiedene Arten von Schwachstellen für nicht vertrauenswürdige Quellen entstehen. Schreiben Sie durch zufälliges Zuordnen von Firmware-Anweisungen Anweisungen von einer Komponente zum NoC oder wenden Sie Bit-Flips in einem Speicher an. Die Autoren schlagen außerdem mehrere neuartige Abdeckungsmetriken vor. Diese dienen dazu, Iterationen zu Manipulationen in Fällen zu leiten, die am stärksten von früheren Manipulationsläufen beeinflusst wurden.

Ihr Testfall ist ein kleiner, aber repräsentativer SoC (Details in GitHub) Firmware-Tests gegen kryptografische Blöcke durchführen und auf Nichtinterferenz und andere Schwachstellen prüfen. Sie führen auch einen sicheren Start mit Datenblockprüfungen durch. Sie fanden mehrere Sicherheitsverstöße in den Kryptoblöcken, außer wenn die Blöcke ECC-Schutz enthielten.

Pauls Ansicht

Die Sicherheitsüberprüfung ist ein so wichtiges Thema, und hier wird sowohl in der Wissenschaft als auch in der Industrie viel gearbeitet. In diesem Artikel werden randomisierte, mutationsbasierte Abdeckung und „Hypereigenschaften“ über Sätze von Simulationsspuren gut zusammengeführt, um eine innovative Lösung zu schaffen, die sowohl skalierbar als auch effektiv beim Nachweis von Sicherheitslücken ist.

Einige Sicherheitseigenschaften können formal nur über eine Reihe von Simulationsspuren definiert werden. „Nichteinmischung“ bedeutet beispielsweise, dass ein Angreifer bestimmte geschützte Berechnungen in einem Design nicht beeinträchtigen kann. Um die Interferenz nachzuweisen, müssen Sie zwei Spuren vergleichen, die im Eingabereiz identisch sind, mit Ausnahme des Vorhandenseins einiger Angreiferaktionen in einer Spur. Wenn geschützte Berechnungen im angegriffenen Trace von denen im Golden Trace abweichen, liegt eine Störung vor.

Die Autoren erstellen ihre eigene spezielle Sprachvariante für Behauptungen über mehrere Spuren und formulieren damit Sicherheitseigenschaften für Nichteinmischung und Vertraulichkeit. Sie erstellen einen benutzerdefinierten Ablauf, um Simulationen nach dem Zufallsprinzip zu manipulieren und ihre Sicherheitseigenschaften zwischen manipulierten und nicht manipulierten Simulationen zu überprüfen. Ihr zufälliger Manipulationsalgorithmus verfügt außerdem über eine elegante, auf Abdeckung basierende Lernheuristik, die ihn dabei unterstützt, Sicherheitslücken effizienter zu finden.

Die Idee von Behauptungen über mehrere Simulationen ist sehr wirkungsvoll. Ich frage mich, ob es möglich wäre, SystemVerilog sauber zu erweitern, um diese Art von Behauptungen zu unterstützen. Dies könnte die Tür zu einigen überzeugenden nativen Erweiterungen kommerzieller Simulations- und formaler Tools öffnen. Eine andere Möglichkeit könnte darin bestehen, den neuen Portable Stimulus Standard (PSS) um Aussagen zu erweitern, die sich über mehrere generierte Tests erstrecken.

Die Lektüre dieses Aufsatzes ist leicht und macht Spaß, auch wenn ich mir gern mehr Details zu den Ergebnissen wünsche. Die Autoren behaupten, dass ihre Lösung Sicherheitslücken in ihrem Open-Source-SoC-Testfall findet, es gibt jedoch keine Details darüber, was diese Lücken sind oder wie ihr Ansatz im Vergleich zu anderen Ansätzen in der Literatur abschneidet, die zum Auffinden derselben Lücken angewendet werden könnten.

Raúls Ansicht

Ich werde dies zunächst unter dem Gesichtspunkt der Technologiereife betrachten. Die Idee gefällt mir im Allgemeinen, ein sehr interessanter Ansatz zur Bewertung der Sicherheit in einem Design. Allerdings erfordert jedes Design von Designern die Bereitstellung von Seed-Tests, Manipulationen und Sicherheitsspezifikationen in einer neuartigen Behauptungssprache. Für mich grenzt dies den Ansatz vorerst fest an den akademischen Bereich. Großartig für Dissertationen und Aufsätze, aber noch nicht annähernd geeignet für den Sprung in die kommerzielle Anwendung.

Für die zweite Herausforderung setze ich meinen Investorenhut auf. Sicherheit ist ein wichtiges Thema, keine Frage. Aber abgesehen von einigen Bereichen, die wir bereits kennen – zum Beispiel Luft- und Raumfahrt, Verteidigung, Zahlungssysteme und Prozessoren/Server. Für die meisten OEMs und Komponentenhersteller ist es immer noch kein existenzielles Problem. Sie sind bereit, ein Kästchen anzukreuzen, wenn dies allgemein erwartet wird. Aber nur, wenn die Auswirkungen auf die Kosten oder die Markteinführungszeit gering sind. Denn ihre Kunden zahlen in der Regel nicht mehr für Sicherheit. Daher hängt die Sicherheit in den meisten Märkten immer noch von schlüsselfertigem IP ab, wie z. B. Hardware-Roots of Trust und benutzerfreundlichen Apps. Auf eine dieser Arten verpackte Lösungen sind investierbar, sonst eher nicht.

Meine Sicht

Paul und Raúl deckten das meiste ab, was ich hätte vorschlagen können. Mir gefällt Pauls Idee, SVA zu erweitern, zumindest um das Experimentieren mit Hypereigenschaften zu fördern. Dies muss eine neue Klasse interessanter Tests eröffnen, die schließlich zu neuen gebündelten Verifizierungsmethoden führen.

Teile diesen Beitrag über: Quelle: https://semiwiki.com/eda/299391-fuzzing-to-validate-soc-security-innovation-in-verification/