A Deductive System for Contract Satisfaction Proofs

Dit artikel introduceert een bewijsbaar correct en compleet deductief systeem, geïmplementeerd in de Rocq-bewijshulpmiddel, dat interactieve bewijzen voor contracttevredenheid in hardware-software-systemen mogelijk maakt door het probleem te reduceren tot relatieve sporengelijkheid en relatieve bisimulatie.

De kern

Stel je voor dat je een heel duur, super-snel raceauto (de computerprocessor) hebt. Maar er is een probleem: de auto lekt een beetje olie. In de wereld van computers is die "olie" eigenlijk geheime informatie die per ongeluk naar buiten komt via de snelheid van de motor, de temperatuur van de banden of het geluid van de uitlaat. Hackers kunnen deze "lekken" gebruiken om te achterhalen wat je aan het doen bent, zelfs als je wachtwoorden goed beveiligd zijn.

Om dit te voorkomen, hebben ingenieurs een slimme truc bedacht: ze maken een contract.

Wat is dit "Contract"?

Stel je voor dat je een autohuurcontract tekent. In plaats van dat je zelf moet weten hoe de motor intern werkt (de zuigers, de brandstofpomp), zegt het contract simpelweg: "Als je deze knop indrukt, gebeurt er dit, en er komt geen olie uit."

Dit contract is een belofte van de hardwarefabrikant aan de softwareontwikkelaar. De ontwikkelaar hoeft niet te weten hoe de chip precies werkt; hij hoeft alleen maar te weten of zijn programma veilig is volgens het contract.

Maar hier zit de hak: Hoe weet je zeker dat de fabriek zijn belofte waarmaakt? Dat de chip inderdaad doet wat het contract zegt, en niet meer? Dat is wat deze paper oplost.

Het Probleem: De "Pen-en-Papier" Chaos

Vroeger moesten mensen handmatig bewijzen dat de chip het contract naleeft. Ze deden dit met pen en papier.

• Het probleem: Het bewijs was zo complex en lang (soms 25 pagina's vol met wiskunde) dat het bijna onmogelijk was om te controleren of er geen foutjes in zaten. Het was als proberen een heel ingewikkeld puzzelstukje te controleren terwijl je blind bent.

De Oplossing: Een Digitale "Rechter"

De auteurs van dit paper hebben een nieuw systeem bedacht, een deductief systeem, dat werkt als een digitale rechter in een computerprogramma genaamd Rocq (een bewijshulp).

In plaats van te proberen het hele bewijs in één keer te zien, laten ze de computer stap voor stap controleren. Ze gebruiken een slimme methode die ze "Relatieve Bisimulatie" noemen.

De Analogie: De Twee Dansers

Stel je voor dat je twee dansers hebt die precies hetzelfde moeten doen:

1. Danser A (Het Contract): Dit is de belofte. Hij dansst heel strak en voorspelbaar.
2. Danser B (De Hardware): Dit is de echte chip. Hij is soms wat chaotischer en doet dingen sneller of langzamer.

Het doel is om te bewijzen: "Als Danser A en Danser A' (een andere versie van Danser A) exact dezelfde dansstappen doen, dan moeten Danser B en Danser B' ook exact dezelfde stappen doen."

De uitdaging:

• Soms doet Danser A twee stappen, terwijl Danser B maar één stap doet (en vice versa). Ze dansen niet perfect synchroon.
• Soms doet Danser A een stap die Danser B niet hoeft te doen, omdat het contract "slim" is en dingen vooruit schuift.

De Magische Truc: "Stap-voor-Stap" Bewijzen

Het oude systeem vroeg je om alle mogelijke stappen van tevoren te voorspellen (een groot net van regels). Dat was te moeilijk.

Het nieuwe systeem van dit paper werkt als een interactieve game:

1. Je begint met een lege lijst.
2. Je zegt tegen de computer: "Kijk, als we deze stap doen, dan komen we hier uit."
3. De computer zegt: "Oké, maar dan moet je ook bewijzen dat de volgende stap veilig is."
4. Je bouwt het bewijs terwijl je het doet. Je hoeft niet het hele pad van tevoren te kennen. Je bouwt een "veiligheidsnet" (een invariant) op terwijl je beweegt.

Als je eenmaal een patroon hebt gevonden (bijvoorbeeld: "Elke keer als we hier zijn, zijn we weer veilig"), kan de computer zeggen: "Ah, ik heb dit al eerder gezien! Dan is het bewijs compleet."

Waarom is dit geweldig?

1. Geen gissen meer: Je hoeft niet meer raden welke complexe regels je nodig hebt. Het systeem helpt je om ze te vinden terwijl je werkt.
2. Fouten zijn onmogelijk: Omdat het bewijs door de computer wordt gecontroleerd, kun je zeker weten dat er geen logische foutjes in zitten. Het is als een onfeilbare scheidsrechter.
3. Flexibel: Het systeem kan omgaan met de "chaos" van de echte chip (waar dingen soms sneller of langzamer gaan) zonder dat het bewijs instort.

Samenvatting in één zin

Dit paper introduceert een slimme, interactieve manier om met een computer te bewijzen dat een chip zijn belofte (het contract) waarmaakt, zodat softwareontwikkelaars veilig kunnen werken zonder zich zorgen te hoeven maken over de ingewikkelde details van de chip zelf.

Het is alsof je van een handgeschreven, onleesbaar recept voor een taart overschakelt naar een robot die je stap voor stap laat zien dat de taart perfect gebakken is, zodat je zeker weet dat er geen giftige ingrediënten in zitten.

Technische samenvatting

Titel: Een Deductief Systeem voor Bewijzen van Contractvoldoening (Extended Version)

Auteurs: Arthur Correnson, Haoyi Zeng, en Jana Hofmann.
Context: Het paper presenteert een nieuwe aanpak voor het formeel verifiëren van hardware-software contracten, specifiek gericht op het afdekken van side-channel lekken in CPU's.

---

1. Het Probleem

Bij het uitvoeren van berekeningen op gedeelde hardware (bijv. in de cloud) kunnen geheime data lekken via microarchitecturale kanalen (zoals caches, buffers en branch predictors). Bekende aanvallen zoals Meltdown en Spectre hebben de ernst hiervan aangetoond.

Om software ontwikkelaars in staat te stellen de veiligheid van hun programma's te verifiëren zonder diepgaande kennis van de microarchitectuur, worden hardware-software contracten gebruikt. Een contract is een abstracte specificatie van het verwachte lekgedrag van een CPU op het niveau van de Instruction Set Architecture (ISA).

De kernuitdaging is het bewijzen van contractvoldoening (contract satisfaction):

• Definitie: Een hardware-implementatie voldoet aan een contract als, voor elk programma en elke twee invoeren, het contract voorspelt dat de lekken gelijk zijn, de daadwerkelijke hardware-uitvoeringen ook ononderscheidbaar zijn.
• Complexiteit: Dit is een relationeel probleem (een hyperproperty) dat vier uitvoeringstraces tegelijkertijd vergelijkt (twee contract-traces en twee hardware-traces).
• Huidige beperkingen: Bestaande methoden gebruiken vaak model-checking (semi-automatisch zoeken naar invarianten) of pen-en-papier bewijzen. Model-checking kan vastlopen of fouten bevatten in de implementatie, terwijl pen-en-papier bewijzen vaak te complex en lang zijn om handmatig te verifiëren (bijv. 25 pagina's voor een simpele processor).

2. Methodologie

De auteurs introduceren een deductief systeem gebaseerd op interactieve bewijshulpmiddelen (specifiek Rocq, de opvolger van Coq). De kern van hun aanpak bestaat uit de volgende stappen:

A. Relative Trace Equality en Relative Bisimulatie

Het paper observeert dat contractvoldoening een specifiek geval is van een algemener probleem: Relative Trace Equality ("trace-gelijkheid impliceert trace-gelijkheid").

• In plaats van een simulatie-relatie vooraf te definiëren, introduceren de auteurs Relative Bisimulatie.
• Dit is een 4-ary (vier-talige) relatie die de staat van twee contracten ($s_1, s_2$) en twee hardware-uitvoeringen ($h_1, h_2$) relateert.
• Het doel is te bewijzen: Als de contract-traces gelijk zijn ($\llbracket s_1 \rrbracket_C = \llbracket s_2 \rrbracket_C$), dan zijn de hardware-traces ook gelijk ($\llbracket h_1 \rrbracket_H = \llbracket h_2 \rrbracket_H$).

B. Asynchrone Redenering en Fixpoints

Een groot obstakel is dat contracten en hardware niet noodzakelijk in "lockstep" (stap voor stap) evolueren. Een contractstap kan overeenkomen met meerdere hardware-stappen of vice versa.

• De auteurs definiëren relative bisimulatie als een combinatie van een grootste fixpunt (co-inductie) en een kleinste fixpunt (inductie).
• Co-inductie wordt gebruikt voor hardware-stappen (om oneindige traces te behandelen).
• Inductie wordt gebruikt voor contract-stappen (om de aanname van gelijke contract-traces te "ontrollen" totdat er een verschil in lekken wordt gevonden).
• Deze mix maakt het mogelijk om asynchrone stappen te hanteren zonder de correctheid van het bewijs te verliezen.

C. Het Deductieve Systeem (Proof Quintuples)

Om het bewijzen te vereenvoudigen, ontwikkelen de auteurs een deductief systeem gebaseerd op Parameterized Coinduction (Paco).

• Bewijzen worden uitgevoerd met Proof Quintuples (bewijs-kwintupels), genoteerd als $R \vdash \begin{bmatrix} s_1 & s_2 \\ h_1 & h_2 \end{bmatrix}$.
• Het systeem gebruikt regels zoals:
  • C-Leak / C-Step: Handelen contract-stappen (inductief).
  • H-Step: Handelt hardware-stappen (co-inductief) en vereist gelijke observaties.
  • Invariant: Stelt een relationele invariant in die tijdens het bewijs kan worden uitgebreid.
  • Cycle: Sluit een bewijs als de huidige staat al in de hypothese zit.
• Dit systeem is sound (correct) en compleet voor relative trace equality.

D. Up-To Technieken

Om bewijzen te vereenvoudigen, worden "Up-To" technieken geïntegreerd. Deze maken het mogelijk om te redeneren over symmetrie, transitiviteit en het vervangen van toestanden door lek-équivalente toestanden, zelfs halverwege een bewijs.

3. Belangrijkste Bijdragen

1. Conceptuele Innovatie: Het identificeren van contractvoldoening als een instance van "Relative Trace Equality" en het introduceren van Relative Bisimulatie als de bijbehorende bewijstechniek.
2. Deductief Systeem: De ontwikkeling van een volledig formeel deductief systeem dat asynchrone redenering ondersteunt via een combinatie van inductie en co-inductie.
3. Formalisatie: De volledige formalisatie van het systeem in de Rocq proof assistant, inclusief het bewijs van de soundness en volledigheid.
4. Up-To Techniques: De integratie van geavanceerde redeneertechnieken (symmetrie, transitiviteit) die bewijzen modularer en beknopter maken.
5. Case Studies: Toepassing van het systeem op twee uitdagende scenario's:
   • Always-Mispredict Contract: Bewijst dat een CPU met branch-speculatie voldoet aan een contract dat altijd beide takken van een branch uitvoert (om Spectre-aanvallen te modelleren).
   • Sequential Contract: Bewijst dat een CPU met out-of-order uitvoering voldoet aan een contract dat instructies strikt sequentieel uitvoert.

4. Resultaten

• De auteurs hebben succesvol twee complexe contractvoldoening-bewijzen mechaniseerd in Rocq.
• Het systeem bleek in staat om de asynchroniteit tussen contract- en hardware-stappen correct te hanteren, wat een groot probleem was voor eerdere handmatige bewijzen.
• De "Up-To" technieken bleken essentieel om de complexiteit van de bewijzen beheersbaar te houden, vooral bij het hanteren van transitiviteit en symmetrie.
• Het bewijs voor de "Always-Mispredict" techniek toont aan dat het systeem kan omgaan met speculatie en het terugdraaien (rollback) van architecturale toestanden, terwijl microarchitecturale effecten (zoals cache-lekken) correct worden geanalyseerd.

5. Betekenis en Impact

• Verhoogde Betrouwbaarheid: Door bewijzen in een proof assistant te mechaniseren, wordt de kans op menselijke fouten in complexe pen-en-papier bewijzen geëlimineerd.
• Modulariteit: Het systeem stelt hardware- en software-ontwikkelaars in staat om hun respectievelijke onderdelen onafhankelijk te verifiëren, zolang ze zich houden aan het contract.
• Schaalbaarheid: De methode biedt een pad naar het verifiëren van complexere CPU-functies (zoals geneste speculatie en geavanceerde pipelines) die nu te complex zijn voor handmatige verificatie.
• Algemene Toepasbaarheid: Hoewel gericht op hardware-software contracten, is de onderliggende theorie van relative bisimulatie ook toepasbaar op andere gebieden zoals veilige compilatie (secure compilation) en het verifiëren van Speculative Non-Interference (SNI).

Kortom, dit paper levert een fundamentele bijdrage aan het veld van hardware-veiligheid door een robuust, formeel raamwerk te bieden dat de kloof tussen abstracte contracten en concrete microarchitecturale implementaties overbrugt.