Technische Samenvatting: iSMC – Een op BDD gebaseerde symbolische modelchecker met interactieve certificering

1. Probleemstelling

Modelchecking is een fundamentele techniek voor het verifiëren van de correctheid van hardware- en softwaresystemen. Het waarborgen van de betrouwbaarheid van de modelchecker zelf vormt echter een kritieke uitdaging. Traditionele certificeringsparadigma's vertrouwen op niet-interactieve protocollen: een bewijzer (de modelchecker) genereert een certificaat (bijvoorbeeld een vervullende toewijzing of een resolutiebewijs), en een verificateur controleert dit onafhankelijk.

Het artikel identificeert een fundamentele theoretische beperking in deze aanpak: voor veel problemen, waaronder algemene CTL-modelchecking, kunnen certificaten een exponentiële lengte in het slechtste geval hebben ten opzichte van de grootte van het voorbeeld. Bijgevolg vereist de verificateur exponentiële tijd om deze te controleren, waardoor het certificeringsproces onpraktisch wordt voor grote systemen, tenzij $NP = coNP$.

De auteurs stellen interactieve certificering voor, een paradigma gebaseerd op interactieve bewijssystemen (IP), waarbij een bewijzer en een verificateur deelnemen aan een meertrapsprotocol. De verificateur stelt adaptief vragen, waardoor hij fouten met hoge waarschijnlijkheid kan detecteren in polynomiale tijd, zelfs als de onderliggende berekening complex is. Hoewel interactieve bewijzen voor PSPACE-problemen (zoals CTL-modelchecking) theoretisch zijn vastgesteld (Shamirs $IP=PSPACE$), is het praktisch toepasbaar maken ervan voor symbolische modelchecking met behulp van Binary Decision Diagrams (BDD's) een open uitdaging gebleven.

2. Methodologie

Het artikel presenteert iSMC, de eerste zelf-certificerende modelchecker die interactieve certificering implementeert voor CTL-modelchecking met rechtvaardigheidseisen. Het systeem is gebouwd op drie kernmodules:

2.1 Architectuur

• Solver: Een symbolische, op BDD gebaseerde modelchecker die de verzameling bereikbare toestanden berekent die voldoen aan een CTL-specificatie. Hij werkt op afgevlakte booleaanse modellen (SMV-formaat) en gebruikt de clic BDD-bibliotheek.
• Prover: Draait op dezelfde machine als de Solver. Hij voert het modelcheckingsvoorbeeld uit en genereert een uitvoeringstrace bestaande uit de reeks BDD-bibliotheekoproepen en asserties die tijdens de berekening zijn gedaan.
• Verifier: Een lichtgewicht module die kan draaien op een client met beperkte middelen. Hij voert het modelcheckingsalgoritme niet opnieuw uit. In plaats daarvan engageert hij zich in een interactief protocol met de Prover om de uitvoeringstrace te verifiëren.

2.2 Het TraceCert-protocol

De kerninnovatie is TraceCert, een interactief bewijsprotocol aangepast van het QBF-certificeringswerk van Couillard et al. [11].

1. Trace naar Circuit: De uitvoeringstrace wordt omgezet in een Generalized Boolean Circuit (GBC). Elke instructie in de trace wordt een poort, en asserties (bijvoorbeeld "toestandsverzameling $C_1$ is niet equivalent aan $C_0$") worden equivalentieclaims.
2. Arithmetisering: Booleaanse functies worden gecodeerd als multivariate polynomen over een eindig veld $\mathbb{F}_p$. Dit stelt de verificateur in staat eigenschappen van de berekening te controleren door polynomen te evalueren op willekeurige punten, in plaats van het volledige circuit te traverseren.
3. Graadreductie: Om ervoor te zorgen dat de polynomen een lage graad hebben (noodzakelijk voor verificatie in polynomiale tijd), introduceert het protocol graadreductie-poorten ($\delta_x$) die exponenten reduceren tot 1 zonder de waarde van de functie op booleaanse invoer te veranderen.
4. Interactieve Ronden: Het protocol verloopt in ronden, waarbij het circuit wordt traversed. De Prover claimt de waarde van een poort; de Verificateur daagt de Prover uit met willekeurige toewijzingen aan de invoer van de poort. De Prover moet polynomen leveren die consistent zijn met de claim. Als de Prover liegt, is de kans om betrapt te worden begrensd door het lemma van Schwartz-Zippel.

2.3 Belangrijkste technische verbeteringen ten opzichte van eerdere werken

De auteurs breiden de technologie uit [11] (die zich richtte op QBF) uit om te voldoen aan de specifieke behoeften van CTL-modelchecking, waarbij drie grote knelpunten worden aangepakt:

1. Efficiënte hernoeming en equivalentie: Het oorspronkelijke protocol (CPCertify) behandelde equivalentie- en hernoemingspoorten inefficiënt ($O(n^2)$ en $O(n^k)$). TraceCert optimaliseert deze ronden respectievelijk tot $O(1)$ en $O(n)$.
2. Compatibiliteit met garbage collection: Standaard BDD-bibliotheken gebruiken globale berekeningcaches en garbage collection. De eerdere aanpak vereiste dat de Prover alle intermediaire BDD's opslaat, wat garbage collection verhinderde. De auteurs introduceren TraceCertRev, een variant van het protocol van onderop, die de Prover toestaat intermediaire resultaten te verwijderen (optredend als orakel) zonder de geldigheid te compromitteren, mits de Prover niet kwaadaardig samenzweert om eerdere uitdagingen te onthouden.
3. Globale berekeningcache: De vorige implementatie (blic) kon geen globale cache gebruiken omdat het uitgebreide BDD's (eBDD's) manipuleerde op een manier die incompatibel was met caching. De auteurs introduceren een nieuwe onveranderlijke eBDD-representatie met behulp van linkvelden om knooppunten van versie te voorzien, waardoor het gebruik van een globale unieke tabel mogelijk wordt en de prestaties aanzienlijk verbeteren.

3. Belangrijkste bijdragen

1. iSMC-systeem: De eerste implementatie van een zelf-certificerende modelchecker met interactieve certificering voor willekeurige CTL-eigenschappen met rechtvaardigheidseisen.
2. TraceCert-protocol: Een nieuw interactief bewijsprotocol dat efficiënt omgaat met variabele hernoeming en equivalentieasserties die veel voorkomen in modelchecking-traces, waardoor de complexiteit van specifieke poortronden wordt verminderd.
3. Geoptimaliseerde eBDD-implementatie: Een nieuw algoritme (ApplyEBDD) en datastructuur die het gebruik van globale berekeningcaches en garbage collection mogelijk maken, waardoor de inefficiënties van de vorige blic-bibliotheek worden overwonnen.
4. TraceCertRev: Een protocolvariant die garbage collection tijdens certificering toestaat, waardoor het systeem levensvatbaar wordt voor grootschalige modelchecking waar geheugen een beperkende factor is.

4. Experimentele resultaten

De auteurs hebben iSMC geëvalueerd op 53 benchmarks uit de HWMCC'25 liveness-track.

• Solver-prestaties: In vergelijking met de volwassen tool NuSMV is de Solver van iSMC gemiddeld 5,84 keer trager. De auteurs schrijven dit voornamelijk toe aan het ontbreken van ondersteuning voor relationele producten (een BDD-optimalisatie) in het huidige prototype, aangezien het interactief certificeren daarvan een open probleem blijft.
• Overhead van de Prover: De Prover draait in tijd $O(S)$, waarbij $S$ de tijd van de Solver is. De constante factor is ongeveer 2,00, wat betekent dat de certificeringsoverhead ongeveer het dubbele is van de oplostijd.
• Efficiëntie van de Verificateur: De Verificateur is zeer efficiënt. Voor een time-out van 15 minuten op de Prover duurde de Verificateur nooit meer dan 3,6 seconden (gemiddelde snelheidswinst van 33,4x ten opzichte van de Prover). De runtime van de Verificateur schaalt lineair met de lengte van de uitvoeringstrace, niet met de berekeningstijd.
• Impact van optimalisaties: De verbeteringen (TraceCert, clic-bibliotheek, globale cache) resulteerden in een gemiddelde snelheidswinst van 2,26x in de executietijd en een reductie van 16,12x in het geheugengebruik in vergelijking met de basisimplementatie die CPCertify en blic gebruikte.

5. Betekenis en claims

Het artikel beweert dat iSMC een belangrijke stap voorwaarts is naar praktische interactieve certificering voor modelchecking.

• Vertrouwen in onbetrouwbare servers: Het systeem maakt een scenario mogelijk waarbij een client met beperkte middelen modelchecking kan delegeren aan een krachtige maar onbetrouwbare server. De server (Solver + Prover) voert de zware berekening uit, terwijl de client (Verifier) het resultaat met hoge waarschijnlijkheid in polynomiale tijd certificeert.
• Polynomiale verificatie: In tegenstelling tot niet-interactieve certificeringsmethoden die exponentiële tijd vereisen voor algemene CTL-eigenschappen, draait de Verificateur van iSMC in polynomiale tijd ten opzichte van het aantal variabelen en de lengte van de trace.
• Schaalbaarheid: De auteurs tonen aan dat met hun optimalisaties de overhead van interactieve certificering beheersbaar is en dat het geheugengebruik aanzienlijk is verminderd, waardoor de aanpak haalbaar wordt voor niet-triviale benchmarks.

De auteurs blijven bescheiden en merken op dat iSMC een eerste prototype is. Zij erkennen dat de Solver momenteel trager is dan state-of-the-art tools zoals NuSMV door ontbrekende optimalisaties (relationele producten) en dat de huidige implementatie gericht is op CTL, hoewel het onderliggende kader theoretisch kan worden uitgebreid tot de volledige modale $\mu$-calculus.