Proving Circuit Functional Equivalence in Zero Knowledge

Dit paper introduceert ZK-CEC, het eerste privacybehoudende framework voor formele hardwareverificatie dat de functionaliteit van geheime IP-ontwerpen zonder vertrouwelijkheidsverlies kan bewijzen aan de hand van open specificaties, waardoor het de betrouwbaarheid van derden-integratie verbetert zonder de eigendomsrechten van de ontwerper te schenden.

De kern

De "Magische Doos" voor Chipontwerpers: Hoe ZK-CEC Vertrouwen Bouwt zonder Geheimen te Lekken

Stel je voor dat je een enorme, complexe fabriek hebt (een computerchip) die je wilt verkopen aan een grote supermarkt (een systeemintegrator). De fabrikant (de leverancier) zegt: "Mijn fabriek werkt perfect en bevat geen verborgen valstrikken." De supermarkt zegt: "Ik geloof je, maar ik wil het eerst controleren."

Hier zit het probleem:

• Als de fabrikant de blauwdrukken laat zien, kan de supermarkt ze stelen en zelf copies maken. Geen verkoop.
• Als de fabrikat alleen zegt "ik heb het gecontroleerd", gelooft de supermarkt het niet. Misschien heeft de fabrikant een geheime, kwaadaardige schakeling (een "hardware Trojan") verstopt die alleen werkt onder heel specifieke omstandigheden. Geen verkoop.

Tot nu toe was dit een doodlopende weg. De oplossing in dit paper heet ZK-CEC. Laten we uitleggen wat dit is, met een paar leuke vergelijkingen.

1. Het Probleem: De "Zwarte Doos" Dilemma

Vroeger gebruikten ze simpele tests (simulatie). Dat is alsof je een auto rijdt om te zien of hij werkt. Maar wat als de auto alleen kapot gaat als je op een heel specifiek moment op de rem trapt terwijl je naar links kijkt? Een simpele ritje (simulatie) mist dit.

Formele verificatie (wiskundig bewijzen dat iets altijd werkt) is beter, maar die vereist dat je de volledige blauwdruk ziet. En dat wil de fabrikant niet.

2. De Oplossing: De "Magische Doos" (Zero-Knowledge Proof)

De auteurs van dit paper hebben een nieuwe methode bedacht, gebaseerd op Zero-Knowledge Proofs (ZKP).

De Analogie van de Magische Doos:
Stel je hebt een doos met een slot. Je wilt bewijzen aan een vriend dat je de sleutel hebt, zonder de sleutel te laten zien.

• Oude methode: Je laat de sleutel zien. (Geheim is weg).
• Nieuwe methode (ZK-CEC): Je doet een heel moeilijk puzzelstuk in de doos. Je vriend geeft je een willekeurige vraag ("Wat is de kleur van het stukje linksboven?"). Als jij de sleutel hebt, kun je de doos openen, het antwoord geven en de doos weer sluiten. Als je de sleutel niet hebt, kun je de doos niet openen en het antwoord niet geven.
• Als je dit 100 keer achter elkaar doet en elke keer het juiste antwoord geeft, weet je vriend met 99,99% zeker dat je de sleutel hebt, zonder hem ooit te hebben gezien.

3. De Nieuwe Uitvinding: Een Nieuw Spelregels

De auteurs merkten op dat bestaande "magische doos"-technieken een zwak punt hadden. Ze waren ontworpen voor situaties waar de vraag openbaar was. Maar in onze chip-situatie is de fabriek (de vraag) geheim.

Als je de fabriek geheim houdt, kan een slechte fabrikant een nep-fabriekje bouwen, die wel past bij de vraag, maar niet de echte fabriek is. Dat is als iemand die een nep-sleutel maakt die toevallig past bij één specifiek slot, maar niet bij de echte deur.

De "Blauwdruk" van de Auteurs:
Ze hebben een nieuw recept (een "blueprint") bedacht om dit op te lossen. Ze splitsen het probleem in twee delen:

1. Het Publieke Deel: De specificaties (wat de chip moet doen). Dit is openbaar.
2. Het Geheime Deel: De eigenlijke chip van de fabrikant.

Ze bewijzen niet alleen dat de chip werkt, maar dat:

• De publieke specificaties kloppen.
• De geheime chip bestaat (niet leeg of gebroken is).
• De geheime chip en de publieke specificaties precies hetzelfde doen, zonder dat de publieke specificatie ooit de geheime chip "leest".

Het is alsof je twee mensen in gescheiden kamers zet. Ze krijgen elk een lijst met regels. Ze moeten bewijzen dat ze exact dezelfde antwoorden geven op dezelfde vragen, zonder ooit door de muur te kijken wat de ander doet.

4. Waarom is dit belangrijk?

Dit is de eerste keer dat dit wiskundig bewezen kan worden voor hardware.

• Voor de leverancier: Ze kunnen hun chip verkopen zonder hun "geheime recept" (Intellectual Property) te stelen.
• Voor de koper: Ze weten zeker dat er geen verborgen valstrikken (Trojans) in de chip zitten, omdat het wiskundig onmogelijk is om een vals bewijs te leveren.

5. De Resultaten: Werkt het in de praktijk?

De auteurs hebben dit gebouwd en getest op echte chips, zoals de "AES S-Box" (een onderdeel dat gebruikt wordt voor versleuteling in je bank-app of WhatsApp).

• Snelheid: Het werkt snel genoeg. Het kost niet eeuwen om te bewijzen.
• Efficiëntie: Ze hebben een slimme truc bedacht (compressie) die het bewijs maken tot wel 2,88 keer sneller maakt.

Samenvatting in één zin

ZK-CEC is een digitale "magische doos" die het mogelijk maakt om te bewijzen dat een computerchip veilig en correct is, zonder dat de ontwerper ooit hoeft te laten zien hoe de chip er van binnen uitziet.

Het lost het eeuwige vertrouwenprobleem op: je kunt nu vertrouwen op een chip zonder de blauwdrukken te hoeven zien.

Technische samenvatting

Titel: Bewijzen van Functionele Equivalentie van Circuits met Zero-Knowledge

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

---

1. Probleemstelling

De moderne geïntegreerde schakeling (IC) ecosysteem is sterk afhankelijk van de integratie van intellectuele eigendom van derden (3PIP). Dit creëert een "vertrouwensdilemma" tussen IP-leveranciers en systeemintegratoren:

• Risico's: Leveranciers kunnen kwaadaardige hardware Trojaanse paarden, backdoors of fouten in hun ontwerpen verstoppen.
• Privacy: Als een koper volledige transparantie eist om het ontwerp te verifiëren, loopt de leverancier het risico op IP-piraterij.
• Beperkingen van bestaande methoden: Huidige privacy-bewuste verificatiemethoden zijn gebaseerd op simulatie (bijv. met homomorfische encryptie of zero-knowledge virtual machines). Simulatie kan nooit alle mogelijke invoercombinaties testen en mist daarom de garantie om zeldzame, maar kritieke fouten (zoals stealthy Trojaanse paarden) te detecteren.
• Formele verificatie: Combinatorische equivalentie-checking (CEC) biedt wiskundige zekerheid, maar bestaande zero-knowledge protocollen voor formele verificatie (zoals ZKUNSAT) vereisen dat de formule (het probleem) publiek is. Als de formule geheim is, kan een kwaadaardige bewijsgever een vals bewijs leveren voor een vervalste formule, waardoor de soundness (geloofwaardigheid) van het protocol verloren gaat.

2. Methodologie

De auteurs stellen ZK-CEC voor, het eerste privacy-bewuste framework voor formele hardware-verificatie. De aanpak combineert formele verificatie met zero-knowledge proofs (ZKP) op basis van Vector Oblivious Linear Evaluation (VOLE).

A. Het Blueprint voor Geheime Formules

Om het soundness-probleem op te lossen, introduceren de auteurs een nieuw blueprint voor het verifiëren van een geheime formule ($\Phi_{sys}$) tegen een publieke specificatie ($\Phi_{prop}$):

1. Splitsing: Het bewijs dat de geheime implementatie correct is, wordt vertaald naar het bewijzen dat de conjunctie van de geheime systeemformule en de publieke eigenschapsformule onvervulbaar (UNSAT) is.
2. Validatie van Soundness: Om te voorkomen dat een kwaadaardige bewijsgever een willekeurige, tegenstrijdige formule gebruikt, moet het protocol drie extra eigenschappen verifiëren in zero-knowledge:
   • P1: De publieke formule is correct en vervulbaar.
   • P2: De gecombineerde formule (miter-circuit) is onvervulbaar.
   • P3: De geheime formule is op zichzelf vervulbaar (geen interne tegenstrijdigheden).
   • P4: De geheime en publieke formules overlappen alleen op de gedefinieerde interface (in- en output), niet op interne variabelen.

B. Arithmetisering en Protocollen

De auteurs coderen booleaanse logica naar univariate polynomen over een eindig veld ($\mathbb{F}$).

• Codering: Clauses worden vertaald naar polynomen waarbij literalen wortels zijn.
• Sub-protocollen:
  • $\Pi_{P1}$: Verifieert de correctheid van de publieke specificatie door commitments te openen.
  • $\Pi_{P2}$: Gebruikt een aangepaste versie van ZKUNSAT om een resolutie-bewijs (refutation proof) te verifiëren dat de miter-circuit onvervulbaar is.
  • $\Pi_{P3}$: Bewijst dat de geheime formule vervulbaar is door een geldige toewijzing (assignment) te tonen zonder de inhoud te onthullen.
  • $\Pi_{P4}$: Verifieert dat er geen ongeoorloofde overlap is tussen geheime en publieke variabelen.
• Optimalisatie: Er wordt een compressietechniek voorgesteld waarbij herhaald gebruikte tussenresultaten (resolvents) in het bewijs worden samengevoegd. Dit vermindert de rekentijd aanzienlijk zonder dat de verifier de oorspronkelijke formule kan reconstrueren (geanalyseerd via een ondergrens voor de complexiteit van het reconstrueren van de bewijstreeks).

3. Belangrijkste Bijdragen

1. Eerste Framework: ZK-CEC is het eerste protocol dat formele equivalentie-checking (CEC) uitvoert in zero-knowledge voor geheime hardware-ontwerpen.
2. General Blueprint: Een nieuw theoretisch kader dat het soundness-probleem van ZKUNSAT oplost voor geheime formules door het probleem te decomponeren in verificatie van publieke en geheime componenten.
3. Implementatie: Een volledige implementatie van het protocol $\Pi_{ZK-CEC}$ met gebruik van de EMP-toolkit en NTL-bibliotheken.
4. Performance Optimalisatie: Een compressie-algoritme voor resolutie-bewijzen dat de bewijstijd met tot 2,88x versnelt, met een wiskundige garantie dat dit geen extra informatielekkage veroorzaakt die tot reconstructie leidt.

4. Resultaten

De auteurs hebben het framework geëvalueerd op 37 verschillende combinatieschakelingen, waaronder:

• Rekenkundige eenheden (adders, multipliers).
• Cryptografische componenten (AES S-Box, SM4, Ascon).
• Logische blokken (decoders, FSM's, arbiters).

Kernbevindingen:

• Correctheid: Het protocol slaagt erin om praktische ontwerpen (zoals de AES S-Box) binnen redelijke tijdslimieten te verifiëren.
• Performance: De verificatie van de onvervulbaarheid (P1+P2) is de grootste bottleneck, wat logisch is gezien de co-NP-karakteristiek van het probleem. De tijd groeit lineair met de grootte van het bewijs.
• Schaalbaarheid: Zonder optimalisatie stuiten grotere circuits op geheugen- en tijdslimieten. Met de compressie-optimalisatie wordt de totale bewijstijd significant verkort (bijv. van ~4936s naar ~1763s voor de AES S-Box).
• Leakage: Het protocol onthult alleen de lengte en breedte van het bewijs (aantal stappen en gate-count), maar niet de interne structuur van het circuit.

5. Betekenis en Impact

Dit werk is een doorbraak voor de beveiliging van de hardware-leveringsketen:

• Vertrouwen zonder Transparantie: Het lost het fundamentele conflict op tussen IP-bescherming en beveiligingsverificatie. Kopers kunnen wiskundig bewijzen dat een chip geen Trojaanse paarden bevat of functioneel correct is, zonder dat de leverancier het ontwerp hoeft te onthullen.
• Van Simulatie naar Formeel: Het verschuift de industriestandaard van onvolledige simulatie naar exhaustieve formele verificatie binnen privacy-bewuste contexten.
• Toepasbaarheid: Het voorgestelde blueprint is niet beperkt tot hardware; het kan worden toegepast op software en cyber-fysische systemen waar formele eigenschappen moeten worden geverifieerd zonder de broncode of logica prijs te geven.

Samenvattend biedt ZK-CEC een robuuste, wiskundig onderbouwde oplossing voor het "vertrouwensdilemma" in de chipindustrie, waarbij privacy en veiligheid hand in hand gaan.