💻 computer science

Sufficient Incorrectness Logic: SIL and Separation SIL

Ce document introduit la logique d'incorrectitude suffisante (Sufficient Incorrectness Logic, SIL), une nouvelle logique de programme par sous-approximation conçue pour identifier précisément l'ensemble des états initiaux menant à des erreurs, et l'étend à la logique de séparation pour gérer les pointeurs et l'allocation dynamique tout en offrant des garanties plus fortes et des postconditions plus concises que les approches existantes.

Auteurs originaux : Flavio Ascari, Roberto Bruni, Roberta Gori, Francesco Logozzo

Publié 2026-01-23

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Flavio Ascari, Roberto Bruni, Roberta Gori, Francesco Logozzo

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 êtes un détective tentant de résoudre un mystère dans une usine immense et chaotique. L'usine est un programme informatique, et votre travail est de comprendre pourquoi les choses tournent mal (des bugs) ou de prouver que tout fonctionne parfaitement.

Pendant des décennies, la méthode standard pour faire cela a été la Logique de Hoare. Voyez cela comme un « Inspecteur de Sécurité ». L'inspecteur examine une machine et dit : « Si vous commencez avec n'importe laquelle de ces entrées sûres, vous n'obtiendrez jamais une sortie défectueuse. » C'est très strict. Cela garantit la sécurité, mais cela donne souvent l'impression de crier au loup. Cela peut dire : « Cette entrée pourrait casser la machine », même si ce n'est pas le cas, juste par mesure de prudence. Cela crée des « fausses alertes » qui agacent les programmeurs.

Puis, il y a quelques années, des chercheurs ont introduit la Logique d'Incorrectness (IL). C'est plutôt comme un « Chasseur de Bugs ». Au lieu d'essayer de prouver que tout est sûr, l'IL essaie de prouver qu'un bug spécifique peut se produire. Elle dit : « Si vous commencez avec certaines de ces entrées, vous trouverez définitivement une sortie défectueuse. » C'est excellent pour trouver de vrais bugs sans fausses alertes, mais cela possède un angle mort : elle vous indique qu'un bug existe, mais ne vous dit pas toujours exactement quelles conditions initiales l'ont causé. C'est comme trouver un engrenage cassé sans savoir quel outil spécifique l'a fait tomber.

Le Nouveau Héros : La Logique d'Incorrectness Suffisante (SIL)

Cette publication présente un nouvel outil de détection appelé Logique d'Incorrectness Suffisante (SIL).

L'idée centrale :
Alors que l'ancien « Chasseur de Bugs » (IL) regarde vers l'avant et dit : « Voici un bug que vous pouvez trouver », la SIL regarde vers l'arrière. Elle demande : « Si nous voyons ce résultat défectueux spécifique, quels sont tous les points de départ possibles qui auraient pu le causer ? »

L'analogie du « Traçage vers l'arrière » :
Imaginez une scène de crime où un vase est brisé sur le sol (l'erreur).

La Logique de Hoare essaie de prouver que si vous entrez dans la pièce, vous ne casserez pas le vase.
La Logique d'Incorrectness (IL) dit : « Si vous lancez une pierre depuis quelque part dans cette pièce, le vase se cassera. » Elle prouve que la casse est possible.
La SIL dit : « Le vase est brisé. Par conséquent, la personne qui l'a cassé devait se trouver dans cette zone spécifique de la pièce. »

La SIL ne se contente pas de trouver le bug ; elle cartographie les conditions initiales exactes (les causes « suffisantes ») qui garantissent que l'erreur se produira. Elle dit au programmeur : « Si votre code commence dans n'importe lequel de ces états, vous allez garanti planter. » C'est incroyablement utile car cela donne un objectif précis pour le débogage. Les développeurs n'ont pas à deviner ; ils savent exactement quelles entrées tester pour reproduire le bug.

Comment cela fonctionne (L'astuce du « Vers l'arrière »)

La plupart des logiques fonctionnent comme la lecture d'un livre : vous commencez à la page 1 (le début du code) et vous avancez vers la page 100 (la fin du code).

Logique vers l'avant (Forward Logic) : « Si je commence ici, où puis-je arriver ? »
SIL (Logique vers l'arrière) : « Si j'arrive ici (dans un crash), d'où dois-je être parti ? »

L'article prouve que la SIL est mathématiquement saine (elle ne ment jamais) et complète (elle peut trouver toutes les réponses qu'elle recherche) pour un ensemble spécifique de règles. Elle est conçue pour être le partenaire parfait pour trouver la source des erreurs, et non seulement les erreurs elles-mêmes.

Gérer la mémoire : La Separation SIL

Les ordinateurs doivent aussi gérer la mémoire (comme un entrepôt avec des étagères). Parfois, des bugs surviennent parce qu'un programme tente d'utiliser une étagère qui a déjà été vidée ou qui n'existe pas.

Les auteurs ont créé une version spéciale de la SIL appelée Separation SIL.

La métaphore : Imaginez que l'entrepôt est immense et désordonné. La logique standard essaie de regarder l'entrepôt entier à la fois pour trouver un article manquant. C'est lent et déroutant.
La Logique de Séparation (Separation Logic) (le fondement de la Separation SIL) dit : « Regardons seulement l'étagère spécifique où l'article manque et ignorons le reste de l'entrepôt. »
La Separation SIL combine cette capacité de « zoom » avec le « traçage vers l'arrière ». Elle peut regarder une erreur de mémoire spécifique (comme un pointeur vers une étagère supprimée) et la remonter jusqu'à la ligne de code exacte et l'entrée qui a causé la suppression.

L'article affirme que pour certains types de programmes (ceux sans boucles complexes), la Separation SIL est non seulement correcte mais aussi « complète », ce qui signifie qu'elle peut trouver l'explication la plus simple et la plus directe de pourquoi une erreur de mémoire s'est produite.

Pourquoi cela importe (selon l'article)

Les auteurs soutiennent que la SIL comble une lacune que d'autres outils ignorent :

Il ne s'agit pas seulement de trouver des bugs : Il s'agit de trouver la cause.
Elle aide au débogage : En identifiant précisément le « état initial suffisant », elle aide les programmeurs à restreindre leurs tests. Au lieu de tester un million d'entrées aléatoires, ils peuvent se concentrer sur les entrées spécifiques que la SIL indique comme celles qui feront définitivement planter le code.
Elle est différente des autres : L'article fournit une « taxonomie » (un arbre généalogique) montrant comment la SIL est liée, mais distincte, de la Logique de Hoare, de la Logique d'Incorrectness et d'autres méthodes. Il montre que si certains outils sont bons pour prouver la sécurité, et d'autres pour trouver des bugs, la SIL est unique pour expliquer pourquoi les bugs se produisent.

En résumé, l'article présente la SIL comme une nouvelle lentille puissante pour observer le code. Au lieu de simplement dire « Ceci est cassé » ou « Ceci est sûr », elle dit : « Si vous commencez ici, vous allez garanti le casser », offrant ainsi aux programmeurs une carte claire pour réparer le problème.

Résumé Technique : Logique d'Incorrectness Suffisante (SIL) et Separation SIL

1. Énoncé du Problème

Les méthodes formelles pour la vérification de programmes se sont historiquement appuyées sur des techniques de sur-approximation (ex: la logique de Hoare, l'interprétation abstraite) pour garantir l'absence d'erreurs. Bien que saines, ces méthodes produisent inévitablement des fausses alertes (erreurs spécieuses), ce qui peut entraver l'adoption par les programmeurs. À l'inverse, les méthodes de sous-approximation (ex: la logique d'incorrectness, le model checking borné) sont conçues pour la recherche de bugs et sont exemptes de fausses alertes, car elles ne signalent que des états d'erreur atteignables. Cependant, les logiques de sous-approximation existantes, telles que la logique d'incorrectness (IL), se concentrent principalement sur la preuve de l'existence d'une erreur atteignable à partir d'une précondition. Elles ne caractérisent pas nécessairement le l'ensemble des états initiaux menant à de telles erreurs.

Le papier identifie une lacune dans le raisonnement sur les sources de l'incorrectness. Les programmeurs ont besoin de savoir non seulement qu'un bug existe, mais spécifiquement quels états d'entrée causent ce bug, afin de délimiter efficacement le débogage et les tests. Bien que les "triplés de Lisbonne" (sous-approximations vers l'arrière) aient été précédemment discutés dans le contexte de la logique d'outcome (OL), un système de preuve dédié, minimal et complet spécifiquement pour inférer des préconditions suffisantes pour les erreurs faisait défaut.

2. Méthodologie

Les auteurs introduisent la Logique d'Incorrectness Suffisante (SIL), une nouvelle logique de programme basée sur des triplés conçue pour une sous-approximation vers l'arrière (backward under-approximation).

2.1 Concept Central : Les Triplés SIL

Un triplé SIL est noté $\langle\langle P \rangle\rangle r \langle\langle Q \rangle\rangle$ .

Sémantique : Le triplé est valide si et seulement si la sémantique de collecte vers l'arrière du programme $r$ appliquée à l'ensemble des états d'erreur $Q$ contient l'ensemble des états initiaux $P$ . Formellement : $J \leftarrow r K (Q) \supseteq P$ .
Interprétation : "Tous les états d'entrée satisfaisant $P$ ont au moins une exécution de $r$ menant à un état satisfaisant $Q$ ."
Distinction avec l'IL : Alors que l'IL ( $[P] r [Q]$ ) garantit que certain état dans $Q$ est atteignable à partir de certain état dans $P$ , la SIL garantit que chaque état dans $P$ peut atteindre une erreur dans $Q$ . Cela fait de $P$ une condition suffisante pour l'incorrectness.

2.2 Système de Preuve

Le papier définit un ensemble minimal de règles de preuve pour la SIL (Figure 7) qui sont à la fois saines et complètes pour les commandes régulières (incluant le non-déterminisme et les boucles).

Sémantique vers l'arrière : Les règles sont dérivées de la sémantique vers l'arrière des commandes (ex: l'assignation utilise la substitution vers l'arrière).
Règle de Conséquence : La règle $\langle\langle \text{cons} \rangle\rangle$ permet de renforcer la précondition et d'affaiblir la postcondition, facilitant ainsi la sous-approximation.
Gestion des Boucles : La logique inclut des règles pour l'itération ( $\langle\langle \text{iter} \rangle\rangle$ ) et des règles additionnelles comme $\langle\langle \text{iter0} \rangle\rangle$ (sauter la boucle) et $\langle\langle \text{unroll} \rangle\rangle$ (dérouler une fois) pour supporter l'analyse pratique sans nécessager d'invariants de boucle pour la terminaison.
Disjonction : Contrairement à la logique de Hoare, la SIL permet d'abandonner des disjonctions dans les préconditions (via $\langle\langle \text{choice} \rangle\rangle$ et $\langle\langle \text{disj} \rangle\rangle$ ), ce qui est crucial pour la scalabilité en sous-approximation.

2.3 Separation SIL

Pour gérer les pointeurs et l'allocation de mémoire dynamique, les auteurs instancient la SIL avec des formules de logique de séparation, créant la Separation SIL.

Langage d'Assertion : Combine la logique de séparation standard (séparation de tas, pointeur vers) avec l'assertion $x \not\mapsto$ (indiquant un pointeur désalloué), adaptée de l'Incorrectness Separation Logic (ISL).
Règles : Inclut des règles vers l'arrière pour les opérations sur le tas (alloc, free, load, store) et une règle de cadre ( $\langle\langle \text{frame} \rangle\rangle$ ) pour permettre un raisonnement local sur les erreurs de mémoire.
Complétude : Le système est prouvé sain. Pour les programmes sans boucle, il est démontré qu'il est relativement complet (en supposant un oracle pour l'implication entre assertions).

3. Contributions Clés

Introduction de la SIL : Une nouvelle logique pour les triplés d'incorrectness suffisante qui identifie les sources des erreurs (états initiaux) plutôt que la simple existence de bugs.
Taxonomie Formelle : Le papier construit une taxonomie des logiques basées sur des triplés (Figure 3) selon deux axes :
- Direction de la Sémantique : Vers l'avant (Logique de Hoare, IL) vs Vers l'arrière (SIL, Conditions Nécessaires).
- Type d'Approximation : Sur-approximation (Logique de Hoare, Conditions Nécessaires) vs Sous-approximation (IL, SIL).
- Cette taxonomie clarifie que la SIL est la combinaison unique de la sémantique vers l'arrière et de la sous-approximation.
Analyse Comparative :
- SIL vs IL : L'IL trouve qu'une erreur est atteignable ; la SIL trouve quels entrées la causent. Elles ne sont pas logiquement équivalentes.
- SIL vs Logique de Hoare (HL) : Pour les programmes déterministes et terminants, la SIL et la HL coïncident (en interprétant la postcondition comme des états d'erreur). Pour les programmes non-déterministes, elles divergent.
- SIL vs Conditions Nécessaires (NC) : Les auteurs prouvent que la NC est isomorphe à la HL (via la double négation) mais n'est pas comparable à l'IL ou à la SIL dans le cas général.
- SIL vs Logique d'Outcome (OL) : Bien que l'OL puisse exprimer des triplés SIL (spécifiquement le motif "Lisbonne"), les auteurs soutiennent que le système de preuve de la SIL est plus direct et naturel pour inférer des préconditions à partir de spécifications d'erreurs, notamment concernant la gestion des disjonctions et le raisonnement vers l'arrière.
Separation SIL : Une instanciation saine et relativement complète pour les erreurs de mémoire, démontrant que la sous-approximation vers l'arrière peut produire des postconditions plus concises et des garanties plus fortes que l'ISL dans certains cas (ex: fournir des témoins réels pour les tests).

4. Résultats

Correction et Complétude : L'ensemble minimal de règles SIL est prouvé sain et complet pour les commandes régulières.
Complétude Relative : La Separation SIL est prouvée relativement complète pour les programmes sans boucle.
Pertinence Industrielle : Le papier soutient que la SIL fournit une justification formelle a posteriori des stratégies d'analyse vers l'arrière utilisées par les outils industriels chez Meta (Zoncolan, Mariana Trench, Pysa), qui infèrent des préconditions d'incorrectness suffisante pour détecter des bugs de sécurité.
Exemples de Dérivation : Le papier fournit des dérivations détaillées (ex: pour un programme client impliquant free et alloc) montrant comment la Separation SIL peut dériver des préconditions garantissant qu'une erreur se produit, offrant un chemin plus direct vers le débogage que les logiques orientées vers l'avant.

5. Signification et Revendications

Le papier affirme que la SIL comble une lacune théorique critique en fournissant un cadre d'under-approximation orienté vers l'arrière. Sa signification réside dans :

Précision pour le Débogage : En identifiant l'ensemble exact des états d'entrée qui mènent aux erreurs, la SIL supporte un "raisonnement vers l'arrière" plus naturel pour les développeurs cherchant à comprendre pourquoi un bug survient, comparé aux sous-approximations vers l'avant qui montrent seulement qu'un bug est atteignable.
Unification Théorique : Elle clarifie le paysage des logiques de programmes, montrant que si une dualité existe entre la logique de Hoare et les Conditions Nécessaires, aucune dualité aussi simple n'existe entre la logique d'Incorrectness et la logique d'Incorrectness Suffisante.
Utilité Pratique : Les auteurs soutiennent que la Separation SIL peut produire des postconditions plus concises et des garanties plus fortes que l'Incorrectness Separation Logic (ISL) pour les tests et le débogage, car elle assure que chaque état dans la précondition mène à l'erreur, fournissant des témoins concrets.

Le papier conclut qu'aucune logique n'est intrinsèquement "meilleure" ; plutôt, chaque logique (HL, IL, NC, SIL) sert un but spécifique. La SIL est positionnée spécifiquement comme l'outil de choix lorsque l'objectif est de localiser les sources d'incorrectness pour guider les efforts de débogage et de test.