Interactive Safety Verification of Distributed Protocols by Inductive Proof Decomposition

Probleemstelling

De automatische verificatie van de veiligheid (safety) van grote, gedistribueerde en concurrerende systemen blijft een uitdaging. Hoewel er de afgelopen jaren veel geavanceerde technieken zijn ontwikkeld (zoals IC3/PDR en syntax-gestuurde synthese), zijn hun prestaties vaak onvoorspelbaar en hun faalmodi ondoorzichtig voor industriële toepassingen.

• De "All-or-Nothing" beperking: Bestaande geautomatiseerde tools werken vaak volgens een "alles-of-niets"-principe. Als ze een probleem oplossen, is geen menselijke tussenkomst nodig; als ze falen, bieden ze weinig tot geen hulp bij het ontwikkelen van een handmatige bewijsvoering of het geven van richtlijnen aan de gebruiker.
• Complexiteit van Inductieve Invarianten: Het ontwikkelen van inductieve invarianten (asserties over de systeemtoestand die bij elke transitie behouden blijven) vereist normaal gesproken een enorme menselijke inspanning. De gebruiker moet vaak werken met een monolithische lijst van lemma's en tegenvoorbeelden (Counterexamples to Induction, CTI's) analyseren in een lineaire, globale context, wat bij complexe protocollen (zoals Raft) onoverzichtelijk wordt.
• Gebrek aan Interactiviteit: Er is weinig focus op interactieve verificatie: hoe kan een mens effectief samenwerken met een tool wanneer deze faalt? Bestaande frameworks zoals Ivy richten zich vaak op beslisbaarheid of heuristieken, maar missen een gestructureerde aanpak voor het beheren van de bewijsstructuur en het lokaliseren van redeneringen.

Methodologie: Inductieve Bewijsdecompositie

De auteurs presenteren een nieuwe methodologie genaamd Inductive Proof Decomposition. Deze methode combineert menselijke inspanning met machine-gidsing door inductieve invarianten te ontwikkelen via een composionele, interactieve aanpak.

De kern van de methode bestaat uit drie pijlers:

1. Inductieve Bewijsgraf (Inductive Proof Graph):

   • Dit is een nieuw formeel datamodel dat de logische afhankelijkheden tussen lemma's en de acties van een protocol visualiseert.
   • De graf bestaat uit lemma-nodes (toestandspredicaten) en actie-nodes (logische transities van het protocol).
   • In plaats van één grote inductieve invariant te zoeken, bouwt de gebruiker de graf op door achteruit te werken vanaf het doel (de veiligheidsproperty).
   • De graf maakt expliciet welke lemma's nodig zijn om specifieke acties inductief te bewijzen.

2. Lokale Redenering en Tegenvoorbeelden:

   • In tegenstelling tot traditionele methoden waar CTI's globaal worden geanalyseerd, worden in deze methode CTI's gelokaliseerd naar specifieke actie-nodes in de graf.
   • De gebruiker focust op één knoop (lemma + actie) tegelijk. Als een knoop niet "gedischarged" (bewezen) is, levert de tool een tegenvoorbeeld voor die specifieke knoop.
   • De gebruiker ontwikkelt dan een nieuw lemma om dit specifieke tegenvoorbeeld uit te sluiten, wat de knoop in de graf valid maakt.

3. Lokale Variabele Slicing (Variable Slicing):

   • Een cruciale innovatie is de techniek om irrelevante protocoltoestanden te verbergen.
   • Voor elke actie-node wordt een "slice" van variabelen berekend die relevant is voor dat specifieke bewijsstap (variabelen in de preconditie van de actie, de definitie van het lemma, en de afhankelijkheden van de updates).
   • Dit reduceert de complexiteit van de tegenvoorbeelden aanzienlijk, zodat de gebruiker zich kan focussen op een klein subset van variabelen in plaats van het volledige systeem.

Belangrijkste Bijdragen

1. Definitie van Inductieve Bewijsgrafen: Een formeel kader dat de logische afhankelijkheden tussen conjuncten van een inductieve invariant en de acties van een gedistribueerd protocol structureert.
2. Methodologie voor Interactieve Verificatie: Een procedure voor het stapsgewijs opbouwen van deze grafen, geleid door gelokaliseerde tegenvoorbeelden en slicing, wat de menselijke cognitieve last verlaagt.
3. Implementatie (Scimitar): Een interactief verificatietool dat een grafische interface biedt voor het bouwen van deze grafen. Het integreert modelcheckers (TLC en Apalache) voor het genereren van tegenvoorbeelden en het valideren van bewijzen.
4. Validatie op Complexe Protocollen: Toepassing en evaluatie op meerdere protocollen, waaronder een industriële specificatie van Raft (AsyncRaft), wat verder gaat dan wat huidige geautomatiseerde tools aankan.

Resultaten

De auteurs hebben hun techniek getest op vijf gedistribueerde protocollen, variërend van eenvoudig tot zeer complex:

• Protocollen: SimpleConsensus, TwoPhase, AbstractRaft, Bakery, en AsyncRaft (een gedetailleerde, industriële specificatie van Raft met asynchrone berichtuitwisseling).
• Efficiëntie: Voor AsyncRaft, een protocol met een complexiteit die veel groter is dan wat eerdere geautomatiseerde methoden aankan, werd de inductieve invariant ontwikkeld in ongeveer 3 menselijke weken. Dit is aanzienlijk sneller dan vergelijkbare inspanningen in de literatuur (vaak 1-2 maanden).
• Slicing Effectiviteit: De variabele slices reduceerden de hoeveelheid informatie die de gebruiker moest analyseren aanzienlijk. Bij SimpleConsensus bedroeg de mediaan van de slice-grootte slechts 33% van de totale variabelen; bij AsyncRaft was dit 42%.
• Inzicht in Structuur: De gegenereerde bewijsgrafen leverden extra inzicht op in de structuur van het protocol. Bijvoorbeeld, de graf maakte complexe inductie-cycli (zoals die rondom log-matching in Raft) zichtbaar, wat moeilijk te zien is in een monolithische invariant.

Betekenis en Conclusie

Dit artikel biedt een doorbraak in de verificatie van complexe gedistribueerde systemen door de kloof tussen volledig geautomatiseerde verificatie (die vaak faalt bij grote systemen) en volledig handmatige bewijsvoering (die extreem tijdrovend is) te overbruggen.

• Schalbaarheid: De methodologie maakt het mogelijk om veiligheidsbewijzen te construeren voor protocollen die te complex zijn voor bestaande state-of-the-art tools.
• Mens-Machine Samenwerking: Het stelt de menselijke verifieur in staat om gefocust te werken op kleine, beheersbare sub-problemen in plaats van een overweldigend monolithisch probleem.
• Interpretbaarheid: De resulterende "Inductive Proof Graph" dient niet alleen als bewijs, maar ook als een documentatie van de logische structuur van het protocol, wat waardevol is voor ontwerp en onderhoud.

Kortom, de paper introduceert een pragmatische en krachtige aanpak waarbij de menselijke intuïtie wordt versterkt door geautomatiseerde slicing en gerichte feedback, waardoor verificatie van industriële schaal systemen haalbaar wordt.