La réponse est non. La vraie question est ce qu’elle peut prouver à la place.

L’analyse statique ne peut pas prouver qu’un avion ne s’écrasera pas. Elle peut prouver que la boucle de contrôle de votre altimètre ne divisera jamais par zéro, ne dépassera jamais les limites d’un tableau et ne provoquera jamais de débordement d’un accumulateur en virgule fixe. Cette distinction est importante, car l’une est une affirmation sur la physique, l’aérodynamique et l’aluminium sous contrainte, et l’autre est une affirmation sur du code que vous pouvez vérifier avant même que l’avion ne quitte le sol.

C’est la promesse de l’interprétation abstraite. Pas l’omniscience. Juste une preuve rigoureuse que certaines catégories spécifiques de défaillances logicielles catastrophiques sont impossibles dans toute exécution possible.

Pourquoi tester un million de scénarios vous laisse toujours dans le doute

Un système de contrôle de vol typique contient des centaines de milliers de lignes de C. L’espace des entrées est le produit cartésien des lectures des capteurs, des commandes du pilote, des conditions environnementales et des variables d’état internes. Vous pourriez faire tourner le système dans un simulateur jusqu’à la mort thermique de l’univers sans pour autant couvrir tous les chemins d’exécution.

Les tests trouvent des bogues. Ils ne prouvent pas leur absence. Chaque test réussi est un point de donnée. Ce n’est pas une garantie.

L’interprétation abstraite renverse l’approche. Au lieu d’exécuter le programme avec des entrées spécifiques, elle l’exécute sur des domaines abstraits qui représentent des ensembles de valeurs possibles. Si l’analyse abstraite dit qu’un état d’erreur particulier est inaccessible, alors cette erreur est inaccessible pour chaque entrée concrète. La preuve est exhaustive, car elle couvre l’intégralité de l’espace des entrées en un seul passage.

Les valeurs concrètes sont trop coûteuses. Utilisez des formes à la place.

Considérons une simple variable x. Dans une exécution concrète, x pourrait valoir 42. Dans une interprétation abstraite, x pourrait être « n’importe quel entier entre 0 et 255 ». Cela s’appelle une abstraction par intervalles.

L’analyseur trace ces intervalles à travers chaque opération. Si x est [0, 100] et y est [1, 10], alors x / y est [0, 100]. L’analyseur sait que la division est sûre, car l’intervalle du diviseur ne comprend pas zéro.

Mais si y était [-5, 5], l’analyseur signalerait une division par zéro potentielle. Il ne sait pas si l’exécution concrète atteint effectivement zéro. Il sait que zéro se trouve à l’intérieur de la plage possible. Cela suffit pour déclencher une alerte.

L’idée clé, due à Patrick et Radhia Cousot en 1976, est que le domaine abstrait doit être une sur-approximation saine de la sémantique concrète. Chaque comportement concret doit être représentable dans l’abstraction. Si l’abstraction est sûre, le programme concret est sûr. Si l’abstraction alerte, le programme concret pourrait aller bien. Mais il se peut aussi que non.

Construire un analyseur par intervalles jouet en Python

Voici un domaine abstrait par intervalles fonctionnel. Il est naïf, mais il illustre les mécanismes.

from dataclasses import dataclass
from typing import Optional

@dataclass(frozen=True)
class Interval:
    lo: int
    hi: int

    def __post_init__(self):
        if self.lo > self.hi:
            raise ValueError("Empty interval")

    def add(self, other: "Interval") -> "Interval":
        return Interval(self.lo + other.lo, self.hi + other.hi)

    def div(self, other: "Interval") -> Optional["Interval"]:
        if other.lo <= 0 <= other.hi:
            return None  # Potential division by zero
        # Simplified: assumes positive divisor for demo
        return Interval(self.lo // other.hi, self.hi // other.lo)

    def intersect(self, other: "Interval") -> Optional["Interval"]:
        lo = max(self.lo, other.lo)
        hi = min(self.hi, other.hi)
        if lo > hi:
            return None
        return Interval(lo, hi)

    def __repr__(self):
        return f"[{self.lo}, {self.hi}]"


def analyze_division(a: Interval, b: Interval) -> None:
    result = a.div(b)
    if result is None:
        print(f"ALERT: {a} / {b} may divide by zero")
    else:
        print(f"SAFE: {a} / {b} = {result}")

Exécutons quelques cas :

analyze_division(Interval(10, 20), Interval(2, 5))   # SAFE
analyze_division(Interval(10, 20), Interval(-1, 1))  # ALERT
analyze_division(Interval(10, 20), Interval(0, 5))   # ALERT

Le premier cas est sûr, car chaque diviseur est positif. Le deuxième est signalé, car zéro se trouve dans [-1, 1]. Le troisième est signalé, car zéro se trouve dans [0, 5].

Remarquez ce qui s’est passé dans le troisième cas. Le programme concret pourrait ne jamais s’exécuter réellement avec b = 0. L’analyseur ne le sait pas. Il est conservateur par conception. C’est le compromis fondamental.

Le coût des faux positifs

Un analyseur statique sain ne manque jamais un bogue. Si un plantage est possible, il le signalera. Mais il signalera aussi des plantages qui sont impossibles. Ces faux positifs sont le prix de la correction.

En pratique, ce coût est élevé. Une analyse par intervalles naïve d’une boucle comme for (i = 0; i < n; i++) concluera souvent que i est [0, +∞], même si n est borné. L’analyseur perd en précision aux points de fusion, où deux chemins d’exécution se rejoignent et leurs états abstraits doivent être combinés.

Les outils réels utilisent des domaines plus sophistiqués. Les polyèdres, les octogones et les abstractions par prédicats traquent les relations entre les variables. x < y est invisible pour les intervalles, mais un domaine polyédral s’en souvient. Ces domaines sont plus précis. Ils sont aussi plus coûteux. Le domaine polyédral a une complexité exponentielle dans le pire des cas. Pour un système de contrôle de vol de 300 000 lignes de C, une implémentation naïve ne terminerait pas avant la retraite de l’appareil.

Ce qu’Astrée a réellement prouvé sur l’A380

Astrée est l’analyseur statique qui a rendu l’interprétation abstraite célèbre dans l’aéronautique. En 2003, Astrée a été exécuté sur le logiciel de contrôle de vol principal de l’Airbus A380. Il a prouvé l’absence de toute erreur d’exécution. Aucune division par zéro. Aucun accès de tableau hors limites. Aucun débordement arithmétique. Aucun code inaccessible dans les chemins critiques.

Il n’a pas prouvé que l’avion ne s’écraserait pas. Il n’a pas prouvé que les lois de commande étaient correctes. Il n’a pas prouvé que le calcul de l’angle d’attaque correspondait à la physique de l’appareil. Ce sont des problèmes différents, résolus avec des outils différents.

Astrée a prouvé que le logiciel ne s’auto-détruirait pas. C’est une affirmation plus étroite qu’elle n’y paraît, et plus précieuse que la plupart des gens ne le réalisent. L’auto-destruction logicielle est une cause fréquente d’accidents aériens. Prouver qu’elle ne peut pas se produire vaut l’effort consenti.

L’outil a accompli cela en combinant plusieurs astuces spécifiques au domaine. Il utilise un domaine non relationnel pour la vitesse et un domaine relationnel pour la précision. Il gère l’arithmétique en virgule flottante avec un modèle qui prend en compte les erreurs d’arrondi. Il comprend le sous-ensemble spécifique de C utilisé en avionique et traite tout comportement indéfini comme une erreur. Il a fallu des années d’ajustement pour que le taux de faux positifs soit suffisamment bas pour que les ingénieurs fassent confiance aux résultats.

La correction est un choix, pas une valeur par défaut

Tous les analyseurs statiques ne visent pas la correction. Des outils comme Coverity, CodeQL et Infer privilégient la découverte de bogues réels plutôt que la preuve d’absence. Ils sous-approximent l’espace des états. Ils pourraient manquer une division par zéro, mais celles qu’ils trouvent sont généralement réelles.

C’est un choix d’ingénierie légitime. Pour une application web, un détecteur de bogues précis à 90 % qui s’exécute en minutes est préférable à un analyseur sain qui vous noie sous les faux positifs. Pour un système de contrôle de vol, c’est l’inverse qui est vrai. Vous voulez la preuve, même si vous devez filtrer le bruit.

L’interprétation abstraite est la technologie qui rend la preuve possible. Ce n’est pas la seule méthode formelle. Les model-checkers comme SPIN et TLA+ vérifient les machines à états. Les démonstrateurs de théorèmes comme Coq et Isabelle vérifient la correction fonctionnelle. L’interprétation abstraite occupe une position privilégiée : elle est entièrement automatique, elle passe à l’échelle sur de grandes codebases, et elle offre des garanties mathématiques sur le comportement à l’exécution.

Où l’interprétation abstraite atteint ses limites

La méthode a des limites strictes. Elle ne peut pas raisonner sur la mémoire allouée via une arithmétique de pointeurs complexe. Elle ne peut pas vérifier qu’un algorithme calcule la bonne valeur, seulement qu’il ne plante pas en le calculant. Elle peine avec la concurrence, la dispatch dynamique et le code qui s’appuie délibérément sur un comportement indéfini.

Elle exige également que le code soit écrit dans un style vérifiable. Le logiciel de vol de l’A380 évite la récursion, limite l’allocation dynamique de mémoire et garde le flux de contrôle simple. Ces restrictions ne sont pas des limitations de l’analyseur. Ce sont des préconditions pour la preuve. On ne peut pas prouver des propriétés d’un code trop chaotique pour être modélisé.

Commencez par les intervalles sur une fonction réelle

Vous n’avez pas besoin d’Astrée pour appliquer ces idées. Choisissez une fonction pure unique dans votre base de code. Identifiez une variable qui doit rester dans certaines limites. Écrivez un simple script de propagation par intervalles. Suivez la variable à travers chaque branche et chaque opération.

Si l’intervalle au point d’utilisation se trouve dans la plage sûre, vous disposez d’une preuve manuelle de sûreté pour cette variable. Si ce n’est pas le cas, vous avez identifié soit un bogue, soit un endroit où votre raisonnement était incomplet. Dans les deux cas, vous avez appris quelque chose qu’un test unitaire aurait pu ne pas détecter.

L’interprétation abstraite ne prouvera pas que votre avion ne s’écrasera pas. Rien ne le peut. Mais elle peut prouver que votre logiciel n’en sera pas la cause.

FAQ

Qu’est-ce que l’interprétation abstraite ?

L’interprétation abstraite est une méthode formelle d’analyse statique de programmes où les valeurs concrètes du programme sont remplacées par des représentations abstraites, telles que des intervalles ou des formes. L’analyseur simule l’exécution du programme sur ces valeurs abstraites. Si une erreur est inaccessible dans le domaine abstrait, elle est inaccessible dans le programme concret pour toutes les entrées possibles.

L’interprétation abstraite peut-elle trouver tous les bogues ?

Non. L’interprétation abstraite prouve l’absence d’erreurs d’exécution spécifiques, telles que les divisions par zéro, les débordements de tampon et les débordements arithmétiques. Elle ne peut pas vérifier qu’un algorithme produit le bon résultat, seulement qu’il ne plante pas. Elle ne peut pas non plus raisonner sur des propriétés extérieures au code, telles que les défaillances matérielles ou le comportement du système physique.

Quelle est la différence entre une analyse statique saine et une analyse statique non saine ?

Un analyseur sain sur-approxime l’ensemble des comportements possibles du programme. Il ne manquera jamais un bogue du type qu’il est conçu pour détecter, mais il peut signaler des faux positifs. Un analyseur non sain sous-approxime. Il peut manquer des bogues, mais ceux qu’il signale sont plus susceptibles d’être réels. La correction est essentielle pour les systèmes critiques pour la sécurité. L’analyse non saine est souvent préférée pour un retour d’information plus rapide dans le développement logiciel général.

L’interprétation abstraite est-elle réservée aux logiciels critiques pour la sécurité ?

Non, bien que ce soit là qu’elle est le plus utilisée. Les idées derrière l’interprétation abstraite apparaissent dans de nombreux compilateurs et optimiseurs. L’analyse de plages de LLVM, par exemple, utilise des abstractions par intervalles pour éliminer les vérifications de limites redondantes. Vous pouvez appliquer le même raisonnement par intervalles à tout code où prouver les limites compte, du micrologiciel embarqué aux noyaux numériques haute performance.