💻 computer science

SEAL: Symbolic Execution with Separation Logic (Competition Contribution)

SEAL est un analyseur statique prototype et modulaire pour la vérification de programmes comportant des structures de données liées non bornées, qui exploite la logique de séparation et le solveur SMT Astral pour obtenir des résultats compétitifs dans la catégorie LinkedLists tout en offrant une extensibilité significative pour le développement futur.

Auteurs originaux : Tomáš Brablec, Tomáš Dacík, Tomáš Vojnar

Publié 2026-02-09

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Tomáš Brablec, Tomáš Dacík, Tomáš Vojnar

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayiez de vérifier qu'une ville complexe et changeante de routes et de bâtiments est sûre à naviguer. Vous devez vous assurer que personne ne tombe d'un pont (un « déréférencement de pointeur NULL »), que personne ne tente de démolir un bâtiment qui n'existe déjà plus (une erreur de « utilisation après libération » ou use-after-free), et que personne ne renverse accidentellement deux fois le même bâtiment (une erreur de « double libération » ou double-free).

C'est exactement ce que fait SEAL, mais au lieu d'une ville, il analyse des programmes informatiques qui gèrent des listes de données complexes et changeantes (comme des listes chaînées).

Voici comment l'article explique SEAL, décomposé en concepts simples :

1. L'idée centrale : Un détective spécialisé

La plupart des outils qui vérifient ces programmes sont comme des détectives qui utilisent un carnet de règles spécifique et rigide pour chaque type de crime. SEAL est différent. Il utilise un « moteur logique » à usage général appelé ASTRAL.

Considérez ASTRAL comme un super traducteur très intelligent. Quand SEAL voit un puzzle complexe sur la façon dont les données sont connectées en mémoire, il traduit ce puzzle dans un langage qu'un solveur informatique standard et puissant (appelé solveur SMT) comprend parfaitement. Cela rend SEAL très flexible. C'est comme avoir un détective capable de changer de langue pour parler à n'importe quel expert, plutôt que d'être coincé avec un seul dialecte.

2. Le défi : Fini vs Infini

Les programmes que SEAL vérifie impliquent souvent des listes chaînées — des chaînes de données où un élément pointe vers le suivant.

Le problème : Certaines listes sont courtes et fixes (comme une chaîne de 3 maillons). D'autres sont non bornées, ce qui signifie qu'elles pourraient avoir 10 maillons, ou 10 000, ou être infinies.
La difficulté : Essayer de vérifier chaque longueur possible d'une chaîne infinie est impossible pour un ordinateur. Cela prendrait une éternité.
L'astuce de SEAL : SEAL utilise une technique appelée abstraction. Imaginez que vous regardez un train très long. Au lieu de compter chaque wagon, SEAL dit : « D'accord, c'est un "long train" ». Il remplace les détails désordonnés du milieu de la chaîne par une étiquette unique et propre (un « prédicat »). Cela lui permet de raisonner sur l'ensemble de la chaîne sans se perdre dans les détails.

3. Comment ça marche : L'analyseur de "forme"

SEAL est un « analyseur de forme ». Il ne regarde pas seulement les nombres ; il regarde la forme de la mémoire.

Tas symboliques (Symbolic Heaps) : Il crée une carte de la mémoire en utilisant des « tas symboliques ». Considérez cela comme un plan qui dit : « Voici un bloc de mémoire, et il est connecté à ce autre bloc ».
Le point fixe de la boucle (Loop Fixpoint) : Lorsqu'un programme s'exécute dans une boucle (répétant la même action), SEAL vérifie si la « forme » de la mémoire s'est stabilisée. Si la forme dans le tour actuel semble « suffisamment sûre » par rapport au tour précédent, il arrête la vérification et déclare la boucle sûre.

4. Forces et faiblesses actuelles

L'article admet que SEAL est encore un prototype (une version précoce), mais il présente des statistiques impressionnantes :

Les bonnes nouvelles (Forces) :

Le club des « Non bornés » : Dans une compétition récente, il y avait 20 outils essayant de vérifier des programmes avec des listes infinies. Seuls quatre outils ont réussi. SEAL en faisait partie.
Potentiel futur : Parce que SEAL utilise ce « traducteur » flexible (ASTRAL), il est plus facile de lui apprendre de nouvelles formes. Les auteurs pensent qu'ils pourront éventuellement lui apprendre à gérer des structures complexes comme les arbres ou les skip-lists (qui sont comme des autoroutes à plusieurs niveaux pour les données) que d'autres outils peinent à manipuler.

Les mauvaises nouvelles (Faiblesses) :

Vocabulaire limité : SEAL ne comprend actuellement qu'un sous-ensemble restreint du langage C. Il ne peut pas encore gérer les mathématiques complexes avec des nombres ou de nombreux types de pointeurs.
Jeu de devinettes : Parfois, SEAL doit deviner quel type de structure de données un morceau de code est en train de construire. S'il se trompe de supposition (par exemple, en pensant qu'une structure complexe est juste une liste simple), il peut rater un bug ou donner une réponse du type « je ne sais pas ».
Faux positifs : Parce qu'il utilise des abstractions (simplification des détails), il peut parfois penser qu'un programme est dangereux alors qu'il est en fait correct. L'article note qu'ils pourraient corriger cela en relançant la vérification sans simplification, mais cela prend plus de temps.

5. L'essentiel

SEAL est un nouvel outil modulaire conçu pour prouver que les programmes gérant des chaînes de données complexes et infinies sont sûrs. Bien qu'il ne soit pas encore parfait et qu'il ne comprenne pas toutes les fonctionnalités du langage C, sa conception unique — utilisant un traducteur général pour résoudre des puzzles logiques — en fait l'un des rares outils capables de gérer les problèmes de sécurité de la mémoire les plus difficiles. Les auteurs espèrent qu'en gardant le système flexible, ils pourront l'améliorer encore davantage lors de futures compétitions.

Résumé Technique : SEAL – Exécution Symbolique avec Logique de Séparation

Énoncé du Problème

La vérification de programmes manipulant des structures de données liées non bornées demeure un défi important en analyse statique. Bien que de nombreux outils s'appuient sur la vérification de modèles bornés ou sur des heuristiques spécialisées, ces approches peinent souvent face à la complexité du raisonnement sur des longueurs de listes arbitraires et des formes de mémoire complexes. De plus, les analyseurs existants basés sur la logique de séparation (SL) couplent fréquemment l'analyse à des solveurs dédiés et non modulaires, ce qui limite leur extensibilité et leur capacité à s'intégrer avec d'autres théories logiques.

Méthodologie

SEAL est un analyseur statique conçu pour la vérification de programmes manipulant des structures de données liées non bornées. Il emploie une interprétation abstraite par voie ascendante (forward abstract interpretation) sur des formules de logique de séparation (SL). La méthodologie centrale se distingue par une architecture modulaire qui découple proprement le moteur d'analyse du moteur de raisonnement logique.

Composants Principaux

Domaine Abstrait (Tas Symboliques) :
- SEAL représente les états de mémoire abstraits comme des tas symboliques, qui sont des formules SL de la forme $\exists x_1, \dots, x_m. \phi_1 * \dots * \phi_n$ .
- Les formules atomiques ( $\phi_i$ $ϕ_{i}$ ) incluent :
  - Formules pures : Décrivant les égalités (ou inégalités) de pointeurs ou les contraintes sur les valeurs non-pointeurs.
  - Atomes de pointeurs (points-to atoms) : Décrivant des cellules de tas uniques.
  - Prédicats inductifs : Décrivant des séquences de pointeurs non bornées (ex: listes).
  - Mémoire libre : Un prédicat spécial qui représente explicitement la mémoire libérée qui reste atteignable.
- Le domaine suit les valeurs entières précises dans une plage configurable (par défaut $[-5, 5]$ ). Les états aux emplacements du programme sont représentés comme des disjonctions (ensembles) de tas symboliques.
Abstraction et Élargissement (Widening) :
- Pour gérer les boucles et les espaces d'états infinis, SEAL effectue un élargissement en généralisant les formes de mémoire. Cela implique de trouver des prédicats spatiaux compatibles (points-to ou listes) et de les joindre en un prédicat de liste unique, à condition que l'emplacement de liaison ne soit pas ciblé par des pointeurs externes ou des variables du programme.
- Le système suit les longueurs minimales de listes jusqu'à une limite fixe pour garantir l'acyclicité lors de l'abstraction.
- Devinette de Prédicats (Predicate Guessing) : Actuellement, SEAL devine le prédicat inductif attendu pour les structures C avant l'analyse basé sur le nombre de champs (ex: un champ auto-référentiel $\to$ SLL ; deux $\to$ DLL). Cette heuristique peut mener à une mauvaise classification (ex: une structure destinée à être une liste imbriquée classée comme une liste doublement chaînée).
Le Solveur ASTRAL :
- Contrairement à la plupart des outils SL qui utilisent des heuristiques dédiées pour la satisfaisabilité et l'implication, SEAL repose sur ASTRAL, un solveur de logique de séparation à usage général.
- ASTRAL traduit les formules SL en théories SMT (spécifiquement les vecteurs de bits et les tableaux) en utilisant une borne sur le déploiement des prédicats.
- Les formules traduites sont transmises au solveur SMT BITWUZLA.
- ASTRAL supporte les prédicats inductifs définis par l'utilisateur, permettant à SEAL de définir ses propres prédicats sans support natif du solveur pour ceux-ci.
Mécanique de l'Analyse :
- Points Fixes de Boucle : Un point fixe est atteint lorsque l'implication entre l'état de l'itération actuelle de la boucle ( $S$ ) et l'état de l'itération précédente ( $T$ ) est valide. Cela est approximé en vérifiant que pour chaque tas dans $S$ , il existe un tas dans $T$ qu'il implique.
- Analyse Interprocédurale : Les appels de fonctions sont optimisés à l'aide de résumés (paires précondition/postcondition).
- Simplification : Le système applique des simplifications syntaxiques, telles que la réduction des classes d'équivalence et la suppression des variables hors de portée.

Contributions Clés

Architecture Modulaire : En séparant le moteur d'interprétation abstraite du moteur de raisonnement logique via ASTRAL, SEAL atteint un design destiné à être plus facile à étendre et à combiner avec le raisonnement dans d'autres théories.
Résolution à Usage Général : L'intégration d'ASTRAL permet à SEAL de tirer parti des solveurs SMT pour l'implication et la satisfaisabilité en SL, évitant ainsi le besoin de solveurs personnalisés et dédiés pour chaque variante spécifique de la logique.
Vérification de Listes Non Bornées : L'outil est capable de vérifier des programmes manipulant des listes liées non bornées, une catégorie où beaucoup d'outils concurrents échouent.

Résultats Expérimentaux

SEAL a participé à la catégorie MemSafety-LinkedLists de la compétition SV-COMP.

Performance Globale : Sur l'ensemble complet de 134 programmes, SEAL en a vérifié 55 comme "Vrai" (correct) et en a trouvé 4 "Faux" (bugs), avec 75 n'ayant donné aucun résultat.
Sous-ensemble de Listes Non Bornées : Sur le sous-ensemble de 69 programmes nécessitant un raisonnement sur des structures de données non bornées, SEAL a vérifié 14 programmes comme corrects et a trouvé 2 bugs.
Comparaison :
- SEAL a surpassé 2LS (qui n'a vérifié que 3 programmes non bornés).
- SEAL a vérifié moins de programmes que PREDATORHP (46) et CPACHECKER (40), qui utilisent tous deux des graphes de mémoire symbolique (SMG).
- SEAL était l'un des quatre seuls analyseurs capables de vérifier des programmes avec des listes non bornées dans cette catégorie.

Signification et Revendications

L'article positionne SEAL comme un prototype prometteur avec un accent spécifique sur l'extensibilité plutôt que sur la domination immédiate en termes de performance brute.

Potentiel Futur : Les auteurs affirment que la conception modulaire de l'outil et sa dépendance à ASTRAL fournissent une base solide pour supporter des structures de données complexes qui ne peuvent pas être facilement représentées par des SMG, telles que les skip-lists et les arbres.
Limitations : En tant que prototype précoce, SEAL ne supporte actuellement qu'un sous-ensemble du langage C (arithmétique de pointeurs limitée, suivi d'entiers spécifique) et repose sur une devinette de prédicats heuristique, ce qui peut mener à des faux positifs ou à l'incapacité de rapporter des violations lorsque les informations entières sont manquantes.
Feuille de Route : Les auteurs ont l'intention d'améliorer la sélection des prédicats pendant l'analyse, de synthétiser des prédicats inductifs à partir d'exemples, et potentiellement d'intégrer SEAL en tant que domaine abstrait au sein du framework Frama-C EVA pour gérer des valeurs non-pointeurs plus complexes.

En résumé, SEAL démontre qu'une approche basée sur le SMT et à usage général pour la résolution de la logique de séparation est une alternative viable et extensible aux heuristiques spécialisées, offrant une voie pour vérifier des structures de données liées complexes et non bornées dans de futures compétitions.