Combining model checking with simulation-based techniques for protocol verification

Technische Samenvatting: Het combineren van Model Checking met Simulatie-gebaseerde Technieken voor Protocolverificatie

Probleemstelling
Model checking is een rigoureuze techniek voor het verifiëren van eindige toestandsmachines, maar wordt frequent gehinderd door het state space explosion problem (toestandsruimte-explosieprobleem). Naarmate de systeemparameters toenemen (bijv. kanaalcapaciteiten of venstergroottes), groeit de bereikbare toestandsruimte exponentieel, waardoor uitputtende verificatie onhaalbaar wordt. Dit artikel adresseert deze beperking in de context van communicatieprotocollen, specifiek het Alternating Bit Protocol (ABP) en het Sliding Window Protocol (SWP). Terwijl eenvoudigere abstracties zoals het Simple Communication Protocol (SCP) direct geverifieerd kunnen worden, zorgt het verhogen van parameters in ABP en SWP ervoor dat de toestandsruimte de capaciteiten van standaard model checking-tools overstijgt, zelfs met moderne hardware.

Methodologie
De auteurs stellen een hybride verificatiemethodologie voor die model checking combineert met simulatie-relaties om de state space explosion te overwinnen. De kern van de theoretische fundering rust op het principe dat als een concrete toestandsmachine $M$ wordt gesimuleerd door een abstracte toestandsmachine $M_A$, en $M_A$ een invariant eigenschap voldoet, de overeenkomstige invariant ook geldt voor $M$.

De methodologie wordt operationeel gemaakt met de rewriting logic taal Maude en omvat twee primaire kaders:

1. Directe Simulatie Verificatie:
   Om een concreet protocol $M$ te verifiëren tegen een abstract protocol $M_A$:

   • Stap 1: Voer directe model checking uit op de abstracte machine $M_A$ om de invariant eigenschap ervan te verifiëren.
   • Stap 2: Conjectureer een simulatie-relatie kandidaat $r$ tussen $M$ en $M_A$. Bewijs dat de invariant van $M$ logisch afleidbaar is uit de invariant van $M_A$ onder de assumptie van $r$, gebruikmakend van statische case splitting en reductie.
   • Stap 3: Demonstreer dat $M$ inderdaad wordt gesimuleerd door $M_A$. Dit houdt in dat de simulatievoorwaarden (correspondentie van de begintoestand en behoud van transities) worden geverifieerd voor alle rewrite rules van $M$.
   • Implementatie: Stap 3 maakt gebruik van een procedure met drie commando's in Maude:
     • srew: Om opvolger-toestanden in $M$ te vinden met behulp van verse constanten om willekeurige waarden te representeren.
     • red: Om de simulatie-relatie tussen de concrete en abstracte toestanden te verifiëren.
     • search: Om te bevestigen dat de abstracte machine in nul of meer stappen een overeenkomstige toestand kan bereiken.
   • Om de betrouwbaarheid te waarborgen ondanks het gebruik van bovengroepen van bereikbare toestanden (vanwege de onbeslisbaarheid van bereikbaarheid), gebruiken de auteurs Lemma 1, die bewijst dat het verifiëren van de transitieconditie over deze bovengroepen voldoende is om de conditie over de werkelijke bereikbare toestanden te garanderen.

2. Compositie van Simulatie-relaties:
   Voor zeer complexe systemen waarbij een enkele abstractie onvoldoende is, stellen de auteurs een hiërarchische aanpak voor. Dit houdt in dat simulatie-relaties worden geketend (bijv. $SWP \to ABP \to SCP$).

   • De invariant van het meest concrete systeem wordt afgeleid van het tussenliggende systeem, dat op zijn beurt wordt afgeleid van het meest abstracte systeem.
   • Dit maakt de verificatie van systemen met enorme toestandsruimtes mogelijk door gebruik te maken van de geverifieerde invarianten van eenvoudigere, gelaagde abstracties.

Belangrijkste Bijdragen
Het artikel presenteert twee hoofdbijdragen:

1. Een methodologie die model checking combineert met simulatie-relaties om systemen te verifiëren waarbij directe model checking faalt door state space explosion.
2. Een methodologie voor de compositie van simulatie-relaties, wat hiërarchische verificatie mogelijk maakt door meerdere lagen van abstractie te koppelen om nog grotere en complexere modellen te hanteren.

Resultaten en Casestudy's
De auteurs hebben hun aanpak geëvalueerd met drie protocollen: SCP, ABP en SWP.

• Casestudy I (ABP):

  • Uitdaging: Directe model checking van ABP met maxIndex = 64 en maxQueueLength = 32 resulteerde in een timeout (>3.600 seconden) vanwege state space explosion.
  • Oplossing: De auteurs stelden een simulatie-relatie vast van ABP naar het eenvoudigere SCP.
  • Resultaat: Het gehele verificatieproces (het controleren van SCP, het afleiden van de invariant en het verifiëren van de simulatie) werd voltooid in minder dan 1 seconde per stap. Dit bevestigde dat ABP aan zijn invariant eigenschap voldoet zonder uitputtende toestandsverkenning.

• Casestudy II (SWP):

  • Uitdaging: SWP introduceert vensterbeheer en sequentienummers, wat een toestandsruimte creëert die aanzienlijk groter is dan die van ABP, waardoor directe verificatie onmogelijk wordt.
  • Oplossing: De auteurs gebruikten de compositie van simulatie-relaties: $SWP \to ABP \to SCP$. Ze verifieerden de simulatie van SWP naar ABP en combineerden dit met de eerder geverifieerde ABP-naar-SCP relatie.
  • Resultaat: De hiërarchische aanpak verifieerde succesvol de invariant eigenschap van SWP (het garanderen dat berichten in volgorde worden ontvangen zonder verlies of duplicatie) met parameters (windowSize = 16, maxQueueLength = 32) die onhaalbaar zouden zijn voor directe controle.

Betekenis en Claims
Het artikel beweert dat deze aanpak de state space explosion effectief mitigeert door de computationele last te verschuiven van uitputtende toestandsdoorloop naar symbolische verificatie op kleinere, abstracte modellen. Belangrijke aspecten van de betekenis zijn:

• Schaalbaarheid: De methode maakt de formele verificatie van protocollen met grote parameters (zoals venstergroottes en wachtrijlengtes) mogelijk die buiten het bereik van directe model checking liggen.
• Herbruikbaarheid: Bestaande formele specificaties kunnen worden hergebruikt als abstracte modellen voor nieuwe, complexere doelwitten, wat de verificatieinspanning aanzienlijk vermindert.
• Automatisering en Rigor: Hoewel het construeren van de abstracte modellen en simulatie-relaties handmatige domeinkennis vereist, wordt de geldigheid van deze relaties semi-automatisch geverifieerd met standaard Maude-commando's. De auteurs hebben een ondersteunende tool ontwikkeld om case splitting en commando-executie te automatiseren, wat menselijke fouten minimaliseert.
• Onderscheid van Bestaand Werk: In tegen tegenstelling tot Counterexample-Guided Abstraction Refinement (CEGAR), dat reactief is en modellen verfijnt op basis van spookachtige tegenvoorbeelden, is deze aanpak proactief door gebruik te maken van domeinkennis om strategische abstracties te construeren. Dit biedt verbeterde transparantie en interpreteerbaarheid, aangezien de simulatie-relaties een menselijk begrijpelijke mapping behouden tussen concrete en abstracte gedragingen.

De auteurs concluderen dat door de simulatietheorie te operationaliseren in een gestandaardiseerde sequentie van Maude-commando's, zij de kloof hebben overbrugd tussen abstracte theoretische relaties en uitvoerbare verificatieworkflows, waarmee zij een praktisch en efficiënt pad bieden voor het verifiëren van complexe gedistribueerde systemen.