Résumé technique : iSMC – Un vérificateur de modèles symbolique basé sur les BDD avec certification interactive

1. Énoncé du problème

La vérification de modèles est une technique fondamentale pour vérifier la correction des systèmes matériels et logiciels. Cependant, garantir la fiabilité du vérificateur de modèles lui-même constitue un défi critique. Les paradigmes de certification traditionnels reposent sur des protocoles non interactifs : un prouveur (le vérificateur de modèles) génère un certificat (par exemple, une affectation satisfaisante ou une preuve par résolution), et un vérificateur le vérifie indépendamment.

L'article identifie une limitation théorique fondamentale dans cette approche : pour de nombreux problèmes, y compris la vérification de modèles CTL générale, les certificats peuvent avoir une longueur exponentielle dans le pire des cas par rapport à la taille de l'instance. Par conséquent, le vérificateur nécessite un temps exponentiel pour les vérifier, rendant le processus de certification peu pratique pour les grands systèmes, sauf si $NP = coNP$.

Les auteurs proposent la certification interactive, un paradigme basé sur les systèmes de preuve interactive (IP), où un prouveur et un vérificateur engagent un protocole multi-tours. Le vérificateur pose des questions de manière adaptative, lui permettant de détecter des erreurs avec une forte probabilité en temps polynomial, même si le calcul sous-jacent est complexe. Bien que les preuves interactives pour les problèmes PSPACE (comme la vérification de modèles CTL) soient théoriquement établies ($IP=PSPACE$ de Shamir), les rendre pratiques pour la vérification de modèles symbolique utilisant les Diagrammes de Décision Binaire (BDD) est resté un défi ouvert.

2. Méthodologie

L'article présente iSMC, le premier vérificateur de modèles auto-certifiant qui implémente la certification interactive pour la vérification de modèles CTL avec des exigences de justice. Le système est construit sur trois modules principaux :

2.1 Architecture

• Résolveur : Un vérificateur de modèles symbolique basé sur les BDD qui calcule l'ensemble des états atteignables satisfaisant une spécification CTL. Il opère sur des modèles booléens aplatis (format SMV) et utilise la bibliothèque BDD clic.
• Prouveur : S'exécute sur la même machine que le Résolveur. Il exécute l'instance de vérification de modèles et génère une trace d'exécution composée de la séquence des appels à la bibliothèque BDD et des affirmations faites pendant le calcul.
• Vérificateur : Un module léger qui peut s'exécuter sur un client aux ressources limitées. Il ne réexécute pas l'algorithme de vérification de modèles. Au lieu de cela, il engage un protocole interactif avec le Prouveur pour vérifier la trace d'exécution.

2.2 Le protocole TraceCert

L'innovation centrale est TraceCert, un protocole de preuve interactive adapté du travail de certification QBF de Couillard et al. [11].

1. Trace vers Circuit : La trace d'exécution est transformée en un Circuit Booléen Généralisé (GBC). Chaque instruction de la trace devient une porte, et les affirmations (par exemple, « l'ensemble d'états $C_1$ n'est pas équivalent à $C_0$ ») deviennent des revendications d'équivalence.
2. Arithmétisation : Les fonctions booléennes sont encodées comme des polynômes multivariés sur un corps fini $\mathbb{F}_p$. Cela permet au vérificateur de vérifier les propriétés du calcul en évaluant des polynômes à des points aléatoires plutôt qu'en parcourant l'ensemble du circuit.
3. Réduction de degré : Pour garantir que les polynômes ont un faible degré (nécessaire pour une vérification en temps polynomial), le protocole introduit des portes de réduction de degré ($\delta_x$) qui réduisent les exposants à 1 sans changer la valeur de la fonction sur les entrées booléennes.
4. Tours interactifs : Le protocole procède par tours, parcourant le circuit. Le Prouveur revendique la valeur d'une porte ; le Vérificateur défie le Prouveur avec des affectations aléatoires aux entrées de la porte. Le Prouveur doit fournir des polynômes cohérents avec la revendication. Si le Prouveur ment, la probabilité d'être pris est bornée par le lemme de Schwartz-Zippel.

2.3 Améliorations techniques clés par rapport aux travaux antérieurs

Les auteurs étendent la technologie de [11] (qui se concentrait sur les QBF) pour répondre aux besoins spécifiques de la vérification de modèles CTL, en traitant trois goulots d'étranglement majeurs :

1. Renommage et équivalence efficaces : Le protocole original (CPCertify) gérait les portes d'équivalence et de renommage de manière inefficace ($O(n^2)$ et $O(n^k)$). TraceCert optimise ces tours à $O(1)$ et $O(n)$ respectivement.
2. Compatibilité avec la collecte de déchets : Les bibliothèques BDD standard utilisent des caches de calcul globaux et la collecte de déchets. L'approche précédente obligeait le Prouveur à stocker tous les BDD intermédiaires, empêchant la collecte de déchets. Les auteurs introduisent TraceCertRev, une variante ascendante du protocole qui permet au Prouveur de rejeter les résultats intermédiaires (agissant comme une oracle) sans compromettre la justesse, à condition que le Prouveur ne comploter pas malicieusement pour se souvenir des défis passés.
3. Cache de calcul global : L'implémentation précédente (blic) ne pouvait pas utiliser un cache global car elle manipulait des BDD étendus (eBDD) d'une manière incompatible avec la mise en cache. Les auteurs introduisent une représentation eBDD immuable novatrice utilisant des champs de liaison pour versionner les nœuds, permettant l'utilisation d'une table unique globale et améliorant considérablement les performances.

3. Contributions clés

1. Système iSMC : La première implémentation d'un vérificateur de modèles auto-certifiant avec certification interactive pour des propriétés CTL arbitraires avec des exigences de justice.
2. Protocole TraceCert : Un nouveau protocole de preuve interactive qui gère efficacement le renommage de variables et les affirmations d'équivalence courantes dans les traces de vérification de modèles, réduisant la complexité de tours de portes spécifiques.
3. Implémentation eBDD optimisée : Un nouvel algorithme (ApplyEBDD) et une nouvelle structure de données qui permettent l'utilisation de caches de calcul globaux et de la collecte de déchets, surmontant les inefficacités de l'ancienne bibliothèque blic.
4. TraceCertRev : Une variante de protocole qui permet la collecte de déchets pendant la certification, rendant le système viable pour la vérification de modèles à grande échelle où la mémoire est une contrainte.

4. Résultats expérimentaux

Les auteurs ont évalué iSMC sur 53 benchmarks du track de vivacité HWMCC'25.

• Performance du Résolveur : Comparé à l'outil mature NuSMV, le Résolveur de iSMC est en moyenne 5,84 fois plus lent. Les auteurs attribuent cela principalement au manque de support pour les produits relationnels (une optimisation BDD) dans le prototype actuel, car les certifier de manière interactive reste un problème ouvert.
• Surcharge du Prouveur : Le Prouveur s'exécute en temps $O(S)$, où $S$ est le temps du Résolveur. Le facteur constant est d'environ 2,00, ce qui signifie que la surcharge de certification est environ le double du temps de résolution.
• Efficacité du Vérificateur : Le Vérificateur est très efficace. Pour un délai d'attente de 15 minutes sur le Prouveur, le Vérificateur n'a jamais pris plus de 3,6 secondes (accélération moyenne de 33,4x par rapport au Prouveur). Le temps d'exécution du Vérificateur évolue linéairement avec la longueur de la trace d'exécution, et non avec le temps de calcul.
• Impact des optimisations : Les améliorations (TraceCert, bibliothèque clic, cache global) ont entraîné une accélération moyenne de 2,26x du temps d'exécution et une réduction de 16,12x de l'utilisation de la mémoire par rapport à l'implémentation de base utilisant CPCertify et blic.

5. Importance et revendications

L'article revendique que iSMC représente une étape significative vers la certification interactive pratique pour la vérification de modèles.

• Confiance dans des serveurs non fiables : Le système permet un scénario où un client aux ressources limitées peut déléguer la vérification de modèles à un serveur puissant mais non fiable. Le serveur (Résolveur + Prouveur) effectue le calcul lourd, tandis que le client (Vérificateur) certifie le résultat avec une forte probabilité en temps polynomial.
• Vérification polynomiale : Contrairement aux méthodes de certification non interactive qui nécessitent un temps exponentiel pour les propriétés CTL générales, le Vérificateur de iSMC s'exécute en temps polynomial par rapport au nombre de variables et à la longueur de la trace.
• Évolutivité : Les auteurs démontrent que grâce à leurs optimisations, la surcharge de la certification interactive est gérable et l'empreinte mémoire est considérablement réduite, rendant l'approche réalisable pour des benchmarks non triviaux.

Les auteurs restent modestes, notant que iSMC est un premier prototype. Ils reconnaissent que le Résolveur est actuellement plus lent que les outils de pointe comme NuSMV en raison de l'absence d'optimisations (produits relationnels) et que l'implémentation actuelle cible le CTL, bien que le cadre sous-jacent puisse théoriquement s'étendre au calcul modal $\mu$ complet.