Proving Circuit Functional Equivalence in Zero Knowledge

Dieses Paper stellt ZK-CEC vor, das erste Framework für die privatsphärewahrende formale Verifikation von Hardware, das mithilfe von Zero-Knowledge-Beweisen die funktionale Äquivalenz geheimer IP-Designs zu öffentlichen Spezifikationen nachweist, ohne die proprietären Details preiszugeben.

Das Wesentliche

Das große Dilemma: Vertrauen ohne Enthüllung

Stellen Sie sich vor, Sie kaufen ein hochkomplexes Auto (einen Chip), das aus vielen Teilen besteht, die von verschiedenen Herstellern stammen. Einer dieser Hersteller (der IP-Hersteller) liefert Ihnen den Motor. Sie wollen sicher sein, dass dieser Motor genau so funktioniert, wie er versprochen hat, und dass er keine versteckten Fallen (wie Hardware-Trojaner) enthält, die das Auto später sabotieren könnten.

Das Problem:

1. Der Hersteller will den Motor nicht zeigen. Wenn er die Baupläne offenlegt, könnte ein Dieb sie stehlen und kopieren.
2. Sie (der Käufer) wollen den Motor nicht blind kaufen. Wenn Sie ihn nicht prüfen, könnten Sie einen defekten oder manipulierten Motor erhalten.

Bisherige Lösungen waren wie ein Testlauf: Der Hersteller ließ den Motor laufen, und Sie schauten zu. Aber das ist wie ein Probefahren nur auf einer geraden Straße. Es gibt keine Garantie, dass der Motor nicht bei einer bestimmten Kurve oder unter extremem Druck versagt (sogenannte "Eckfälle" oder versteckte Trojaner).

Die Lösung: ZK-CEC – Der magische Beweis

Die Forscher haben eine neue Methode namens ZK-CEC entwickelt. Stellen Sie sich das wie einen magischen, durchsichtigen Koffer vor, den Sie nicht öffnen dürfen, aber trotzdem beweisen können, was sich darin befindet.

Die Idee basiert auf zwei genialen Schritten:

1. Der "Geheime Plan" vs. der "Offizielle Bauplan"

Statt den ganzen Motor zu zeigen, teilt der Hersteller den Beweis in zwei Teile:

• Der öffentliche Teil: Das ist der offizielle Bauplan (die Spezifikation), den Sie kennen.
• Der geheime Teil: Das ist der tatsächliche Motor des Herstellers.

Der Hersteller behauptet: "Mein geheimer Motor ist exakt gleich dem öffentlichen Bauplan."

2. Das große "Nicht-Können"-Spiel (Unsatisfiability)

Um zu beweisen, dass beide identisch sind, nutzen sie ein mathematisches Spiel namens Kontradiktion.
Stellen Sie sich vor, Sie versuchen, einen Weg zu finden, bei dem der öffentliche Bauplan und der geheime Motor unterschiedlich funktionieren.

• Wenn Sie einen solchen Weg finden, sind sie nicht gleich.
• Wenn es keinen einzigen Weg gibt, wie sie sich unterscheiden können, dann müssen sie identisch sein.

Der Hersteller muss nun beweisen: "Ich habe nach allen denkbaren Wegen gesucht, um einen Unterschied zu finden, und es gibt keinen."

Das ist wie der Beweis, dass ein Labyrinth keinen Ausgang hat. Normalerweise müsste man das ganze Labyrinth zeigen, um das zu beweisen. Aber mit Zero-Knowledge Proofs (Null-Wissen-Beweise) kann der Hersteller sagen: "Ich habe das Labyrinth durchsucht und keinen Ausgang gefunden, und ich kann es beweisen, ohne Ihnen auch nur einen einzigen Gang des Labyrinths zu zeigen."

Wie funktioniert der Trick? (Die Analogie)

Stellen Sie sich vor, der Hersteller hat einen riesigen Stapel Karten (den geheimen Code). Er behauptet, dass keine dieser Karten eine "falsche Farbe" hat, wenn man sie mit dem offiziellen Muster vergleicht.

Um das zu beweisen, ohne die Karten zu zeigen:

1. Verschlüsselung: Der Hersteller legt die Karten in einen verschlossenen, aber mathematisch verifizierbaren Umschlag.
2. Der Test: Der Käufer (Sie) stellt eine Frage: "Wenn ich eine zufällige Karte aus dem Stapel nehme, ist sie dann mit dem Muster vereinbar?"
3. Der Beweis: Der Hersteller führt eine komplexe mathematische Operation durch (Resolution), die beweist, dass es unmöglich ist, eine Karte zu finden, die das Muster bricht.
4. Das Ergebnis: Sie hören das Ergebnis: "Es gibt keine widersprüchliche Karte." Sie haben die Gewissheit, dass alles stimmt, aber Sie haben keine Ahnung, wie die Karten tatsächlich aussahen oder wie der Motor im Inneren gebaut ist.

Warum ist das neu und wichtig?

Frühere Methoden waren wie ein Testfahrer, der nur ein paar Runden dreht. Wenn der Trojaner nur bei einer sehr seltenen Temperatur aktiv wird, verpasst der Testfahrer ihn.
Die neue Methode ZK-CEC ist wie ein mathematischer Gott, der jede einzelne mögliche Situation durchrechnet und garantiert, dass es niemals zu einem Fehler kommt.

Die Vorteile:

• Sicherheit: Man kann Hardware-Trojaner zu 100 % ausschließen (formale Garantie).
• Privatsphäre: Der Hersteller muss sein geistiges Eigentum nicht preisgeben.
• Effizienz: Die Forscher haben gezeigt, dass dies auch für komplexe Chips (wie Verschlüsselungschips) in akzeptabler Zeit funktioniert.

Zusammenfassung in einem Satz

ZK-CEC ist wie ein magischer Richter, der einem Käufer garantiert, dass ein geheimes Produkt genau so funktioniert wie versprochen, ohne dass der Käufer auch nur einen Blick auf die geheimen Baupläne werfen darf – und das mit mathematischer, nicht nur probabilistischer Sicherheit.

Technische Zusammenfassung

Titel: Nachweis der funktionellen Äquivalenz von Schaltungen im Zero-Knowledge-Modus (ZK-CEC)

Autoren: Sirui Shen, Zunchen Huang, Chenglu Jin (Centrum Wiskunde & Informatica, Amsterdam)

---

1. Problemstellung und Motivation

Der moderne Chip-Entwicklungsprozess ist stark auf die Integration von geistigem Eigentum (IP) von Drittanbietern (3PIP) angewiesen. Dies führt zu einem „Vertrauensdilemma" zwischen IP-Herstellern und Systemintegratoren:

• Sicherheitsrisiken: IP-Hersteller könnten bösartige Schaltungen (Hardware-Trojaner, Backdoors) einschleusen.
• Datenschutz: IP-Hersteller möchten ihre proprietären Designs nicht offenlegen, um Diebstahl zu verhindern.
• Limitationen bestehender Lösungen: Aktuelle privacy-erhaltende Verifikationsmethoden basieren auf Simulationen (z. B. mittels Homomorpher Verschlüsselung oder zkVMs). Diese können zwar das Vertrauen erhöhen, bieten aber keine exhaustiven formalen Garantien. Simulationen erfassen keine Randfälle (Corner Cases) und können subtile Hardware-Trojaner übersehen.
• Lücke in der Forschung: Bestehende Zero-Knowledge-Protokolle für formale Verifikation (wie ZKUNSAT) setzen voraus, dass die zu verifizierende Formel (die Spezifikation) öffentlich ist. Wenn die Formel geheim ist (z. B. das Design des Herstellers), können diese Protokolle nicht verhindern, dass ein böswilliger Beweiser eine gefälschte Formel beweist, was die Soundness (Korrektheit) des Systems untergräbt.

2. Methodik: ZK-CEC Framework

Die Autoren schlagen ZK-CEC vor, das erste privacy-erhaltende Framework für die formale Hardware-Verifikation mittels Combinational Equivalence Checking (CEC).

A. Das Grundgerüst (Blueprint) für geheime Formeln

Um das Soundness-Problem bei geheimen Formeln zu lösen, schlagen die Autoren ein neues Protokoll-Design vor, das die Formel in zwei Teile zerlegt:

1. $\Phi_{sys}$ (Geheim): Das private System-Design des Herstellers.
2. $\Phi_{prop}$ (Öffentlich): Die öffentliche Spezifikation oder Eigenschaft, die verifiziert werden soll.

Das Ziel ist es, zu beweisen, dass die Konjunktion $\Phi_{sys} \land \Phi_{prop}$ unerfüllbar (UNSAT) ist. Dies bedeutet, dass das geheime Design keine Zustände zulässt, die die öffentliche Spezifikation verletzen.

Um die Soundness zu gewährleisten, müssen vier Bedingungen in Zero-Knowledge bewiesen werden:

1. Korrektheit der öffentlichen Formel: $\Phi_{prop}$ ist korrekt und erfüllbar.
2. Erfüllbarkeit des geheimen Systems: $\Phi_{sys}$ ist erfüllbar (keine internen Widersprüche im Design).
3. Variable Isolation: Die Variablen von $\Phi_{sys}$ und $\Phi_{prop}$ überschneiden sich nur an definierten Schnittstellen (Inputs/Outputs).
4. Unerfüllbarkeit der Gesamtkonjunktion: Die Kombination aus System und Spezifikation führt zu einem logischen Widerspruch (UNSAT).

B. Technische Umsetzung

• Arithmetisierung: Boolesche Logik wird in univariate Polynome über einem endlichen Körper $\mathbb{F}$ übersetzt. Klauseln werden als Polynome kodiert, deren Wurzeln den Literalen entsprechen.
• VOLE-basierte Zero-Knowledge-Proofs (ZKP): Das Framework nutzt Vector Oblivious Linear Evaluation (VOLE) als Backend für effiziente Commitments und Berechnungen.
• Sub-Protokolle:
  • $\Pi_{P1}$: Verifiziert die öffentliche Spezifikation und die Miter-Schaltung.
  • $\Pi_{P2}$: Beweist die Unerfüllbarkeit (UNSAT) der Miter-Schaltung unter Verwendung eines Resolution-Beweises (basierend auf ZKUNSAT, aber angepasst für kommittierte Formeln).
  • $\Pi_{P3}$: Beweist, dass das geheime Design erfüllbar ist (SAT), ohne den Beweis selbst preiszugeben.
  • $\Pi_{P4}$: Stellt sicher, dass geheime und öffentliche Klauseln keine unerlaubten Variablen teilen (außer an der Schnittstelle).
• Optimierung: Um die Rechenkosten für lange Resolution-Beweise zu senken, wird eine Kompressionstechnik eingeführt, bei der mehrfach verwendete Resolventen (gelernte Klauseln) zusammengefasst werden. Dies beschleunigt den Beweis, ohne die Sicherheit signifikant zu gefährden (Analyse der unteren Schranke für die Rekonstruktion der Beweisstruktur).

3. Schlüsselbeiträge

1. Erster ZKP-Ansatz für formale Hardware-Verifikation: ZK-CEC ist das erste Protokoll, das die funktionelle Äquivalenz eines geheimen IP-Kerns zu einer öffentlichen Spezifikation mathematisch beweist, ohne das Design preiszugeben.
2. Allgemeines Blueprint für geheime Formeln: Die Autoren lösen das Soundness-Problem bei der Verifikation geheimer Formeln durch eine Trennung in öffentliche und private Komponenten mit strengen Kreuz-Beschränkungen.
3. Praktische Implementierung: Das Protokoll wurde im EMP-Toolkit implementiert und auf einer Vielzahl von Schaltungen getestet.
4. Leakage-Analyse und Optimierung: Es wird gezeigt, dass die eingeführte Optimierung (Resolventen-Kompression) nur minimale zusätzliche Informationen preisgibt (Länge der Beweisbäume), die jedoch nicht ausreichen, um das ursprüngliche Design zu rekonstruieren.

4. Ergebnisse und Evaluation

Die Autoren haben ZK-CEC auf 37 verschiedenen kombinatorischen Schaltungen evaluiert, darunter:

• Arithmetische Einheiten (Addierer, Multiplizierer).
• Steuerlogik (Barrel-Shifter, Decoder, FSMs).
• Kryptografische Komponenten (AES-S-Box, SM4, Ascon, Present).
• Fehlererkennungsmodule (CRC, Parity).

Wichtige Messwerte:

• Funktionalität: Das Protokoll konnte praktische Designs wie die AES-S-Box erfolgreich verifizieren.
• Performance: Die Verifikation der Unerfüllbarkeit (UNSAT) ist der dominierende Kostenfaktor (da UNSAT ein co-NP-vollständiges Problem ist).
• Beschleunigung: Durch die Kompressions-Optimierung konnte die Beweiszeit um den Faktor bis zu 2,88x reduziert werden.
• Skalierbarkeit: Bei sehr großen Schaltungen (z. B. 6x6 Multiplizierer) stießen die Ressourcen (RAM) an Grenzen, was auf die exponentielle Wachstumsrate der Resolution-Beweise hinweist. Dennoch ist das Framework für viele praktische Anwendungen geeignet.

5. Bedeutung und Ausblick

• Vertrauensbildung: ZK-CEC ermöglicht eine vertrauenswürdige Lieferkette für Hardware, bei der IP-Hersteller ihre Designs schützen können, während Systemintegratoren eine formale Garantie gegen Trojaner und Designfehler erhalten.
• Paradigmenwechsel: Der Übergang von simulationsbasierten zu formalen, Zero-Knowledge-basierten Verifikationsmethoden stellt einen Meilenstein dar, da er mathematische Sicherheit ohne Offenlegung des Quellcodes bietet.
• Zukünftige Anwendungen: Das vorgestellte Blueprint ist nicht auf Hardware beschränkt und kann potenziell auf Software-Verifikation und cyber-physische Systeme angewendet werden.

Zusammenfassend stellt ZK-CEC einen Durchbruch dar, der die Lücke zwischen dem Bedarf an strengster Sicherheit in der Hardware-Lieferkette und dem Schutz geistigen Eigentums schließt, indem es Zero-Knowledge-Proofs mit formaler Logik verknüpft.