Vérification formelle pour les logiciels de défense critiques : méthodes, outils et assurance

Par Corvus Intelligence Engineering Team · À propos de l'équipe →

25 juin 2026 13 min de lecture

Tout programme de vérification logicielle finit par se heurter au même problème structurel : les tests sont bornés. Une suite de tests, aussi volumineuse soit-elle, n'exerce qu'un sous-ensemble fini d'entrées et de chemins d'exécution. Les combinaisons restantes, non testées, représentent une hypothèse implicite selon laquelle le comportement non testé est correct. Pour la plupart des logiciels commerciaux, cette hypothèse est acceptable ; le coût d'un défaut non découvert reste gérable. Pour la sûreté logicielle dans les systèmes de défense — code contrôlant des armes, des surfaces de contrôle de vol ou des fonctions critiques pour la vie humaine — un seul défaut sur un chemin non testé peut être catastrophique. La vérification formelle comble cette lacune non pas en effectuant davantage de tests, mais en remplaçant les preuves basées sur l'exécution par des preuves mathématiques.

Les méthodes formelles englobent une famille de techniques — model checking, démonstration de théorèmes et interprétation abstraite — qui raisonnent mathématiquement sur l'espace complet des comportements possibles d'un programme. Chacune offre des compromis différents entre expressivité, automatisation, passage à l'échelle et robustesse de la garantie produite. Cet article examine chaque technique dans le contexte du développement de logiciels de défense, explique comment elles s'intègrent dans la certification DO-178C DAL A et l'analyse de sécurité MIL-STD-882, et fournit une évaluation réaliste des situations où les méthodes formelles sont rentables et de celles où elles ne le sont pas.

Pourquoi les tests seuls ne peuvent pas garantir la sûreté

Les limites des tests utilisés comme unique stratégie de vérification ne tiennent pas principalement à la quantité de tests ; elles sont structurelles. Trois problèmes convergent pour rendre une assurance basée uniquement sur les tests insuffisante pour les systèmes critiques.

Le plafond de couverture. Les métriques de couverture structurelle — couverture des instructions, couverture des branches, Modified Condition/Decision Coverage (MC/DC) — mesurent la fraction des structures de code exercée par une suite de tests. DO-178C exige la couverture MC/DC pour les logiciels DAL A car elle garantit que chaque résultat de décision et chaque condition au sein de chaque décision influence de manière indépendante le résultat. Pourtant, même une couverture MC/DC à 100 % n'épuise pas l'espace d'entrées : une fonction avec cinq paramètres entiers de 32 bits possède 2¹⁶⁰ combinaisons d'entrées possibles. Une suite de tests démontrant 100 % de couverture MC/DC peut couvrir des dizaines ou des centaines de chemins d'exécution mais ne peut rien dire sur la correction des exécutions qui combinent des valeurs d'entrée spécifiques de manières non testées. Le plafond de couverture n'est pas un problème de qualité des tests — c'est un fait mathématique concernant les tests finis d'espaces infinis.

L'explosion combinatoire dans les systèmes concurrents. Les logiciels de défense critiques sont presque toujours concurrents : plusieurs tâches s'exécutent en parallèle, partagent de la mémoire, échangent des messages via des files et des sémaphores, et sont soumises à des interruptions pouvant préempter l'exécution à des points arbitraires. Le nombre d'entrelacement possibles de N tâches concurrentes avec K étapes chacune croît comme O(K^N). Un système avec trois tâches de dix étapes chacune possède plus d'un milliard d'entrelacement possibles. Les tests n'en exercent qu'une infime partie ; les métriques de couverture ne disent rien sur les entrelacement non testés. Les conditions de course, les inversions de priorité et les interblocages se cachent dans les entrelacement que les tests n'exercent pas par hasard.

Le rôle des méthodes formelles. La vérification formelle aborde ces problèmes en remplaçant l'énumération par la preuve. Au lieu de demander « le système s'est-il comporté correctement pour ces entrées ? », elle demande « est-il mathématiquement impossible que le système se comporte incorrectement pour n'importe quelle entrée ? ». La question est plus difficile et plus coûteuse à répondre, mais la réponse — lorsqu'elle est positive — est catégoriquement plus solide. C'est pourquoi l'industrie aéronautique, l'industrie nucléaire et le secteur de la défense imposent ou encouragent les méthodes formelles pour les niveaux d'assurance de conception les plus élevés : les tests établissent la confiance ; la vérification formelle établit la certitude dans les limites du modèle formel et de ses hypothèses.

La discipline connexe de l'analyse statique de code pour les logiciels de défense se situe entre les tests et la vérification formelle : les outils d'analyse statique examinent le code source sans l'exécuter, identifiant des classes de défauts que les tests ratent, mais généralement sans les garanties de solidité mathématique que les méthodes formelles fournissent.

Model checking : vérification exhaustive de l'espace d'états

Le model checking est la technique de vérification formelle la plus largement applicable aux logiciels de défense car elle est la plus automatisée. Étant donné un modèle formel d'un système et une propriété exprimée en logique temporelle, un model checker explore exhaustivement tous les états atteignables et confirme que la propriété est vérifiée dans chacun — ou produit un contre-exemple démontrant une violation.

Propriétés en logique temporelle pour les systèmes de défense. La Linear Temporal Logic (LTL) et la Computation Tree Logic (CTL) sont les deux principaux langages de propriétés utilisés en model checking. Les propriétés LTL expriment des contraintes sur les chemins d'exécution individuels. Une propriété de sûreté typique en défense : globalement, chaque fois que le système entre dans l'état armé, dans l'état suivant le verrou de sécurité doit être libéré et la confirmation de l'opérateur doit être présente. Les propriétés CTL raisonnent sur des arbres de calcul ramifiés — exprimant, par exemple, qu'un chemin de récupération existe toujours depuis tout état atteignable. Les applications en défense comprennent la vérification que les machines à états des protocoles de communication n'entrent jamais dans des états non définis, que la logique d'ordonnancement respecte toujours les délais pour tout ordonnancement valide des tâches, et que les séquences de verrouillage de sécurité ne peuvent pas être contournées par aucune combinaison d'entrées valides.

Outils : SPIN et NuSMV. SPIN est un model checker à états explicites principalement utilisé pour vérifier les logiciels concurrents et les protocoles de communication. Son langage d'entrée, Promela, modélise des processus concurrents communiquant par des canaux de messages ; les propriétés sont exprimées en LTL. SPIN vérifie par recherche en profondeur d'abord avec stockage d'états basé sur le hachage et produit des traces de contre-exemples pouvant être rejouées dans un simulateur. NuSMV est un model checker symbolique qui utilise les Binary Decision Diagrams (BDDs) et le bounded model checking avec des solveurs SAT pour représenter et explorer les ensembles d'états de manière symbolique — le rendant efficace pour les systèmes avec de grands espaces d'états où l'énumération explicite est infaisable. Pour les protocoles et machines à états des logiciels de défense, SPIN est généralement plus applicable ; pour la logique de contrôle embarqué modélisée au niveau transfert de registre, l'approche symbolique de NuSMV est souvent plus traitable.

Le problème d'explosion des états et CEGAR. L'espace d'états atteignable croît exponentiellement avec la taille du système. Counterexample-Guided Abstraction Refinement (CEGAR) est la technique pratique principale pour gérer cela. Le flux de travail commence par un modèle abstrait grossier suffisamment petit pour être vérifié mais pouvant introduire des comportements parasites absents du système concret. Si la propriété est vérifiée sur le modèle abstrait, elle l'est sur le système concret par solidité de l'abstraction. Si un contre-exemple est trouvé, il est vérifié contre le modèle concret : si le modèle concret présente également le contre-exemple, c'est un défaut réel ; sinon, l'abstraction est raffinée en ajoutant plus de détails dans la région où le contre-exemple parasite est apparu. CEGAR est itératif et peut converger sur un résultat de vérification sans jamais représenter explicitement l'espace d'états complet.

/* Fragment Promela SPIN : verrou de déclenchement d'arme */
mtype = { SAFE, ARMED, RELEASED };
mtype safety_state = SAFE;
mtype confirm_state = SAFE;
mtype release_state = SAFE;

active proctype safety_controller() {
  do
  :: safety_state == ARMED && confirm_state == RELEASED ->
       atomic { release_state = RELEASED; }
  :: else -> skip
  od
}

/* Propriété LTL : déclenchement uniquement quand les deux préconditions sont satisfaites */
ltl p1 { [] (release_state == RELEASED ->
              (safety_state == ARMED && confirm_state == RELEASED)) }

Lorsqu'un model checker détecte une violation de propriété, il produit une trace de contre-exemple — une séquence complète d'états du système depuis l'état initial jusqu'à l'état violant. Cette trace est directement exploitable : elle spécifie précisément quelle séquence d'événements conduit à l'état non sûr, permettant aux développeurs de reproduire la défaillance de manière déterministe et de concevoir un correctif. Les contre-exemples trouvés lors de vérifications documentées de protocoles C2 de défense ont révélé des contournements d'authentification possibles uniquement sous des combinaisons spécifiques de délai de message et de retransmission — des scénarios jamais exercés durant des mois de tests d'intégration.

Démonstration de théorèmes : preuves mathématiques vérifiées par machine

Là où le model checking épuise automatiquement un espace d'états borné, la démonstration de théorèmes construit une preuve mathématique d'une propriété qui s'applique sur un domaine non borné ou paramétré — en faisant la technique de choix lorsque la propriété à vérifier implique de l'arithmétique sur les réels, des structures de données non bornées, ou des algorithmes paramétrés qu'aucun espace d'états fini ne peut représenter.

Coq, Isabelle/HOL et PVS en défense. Coq est un assistant de preuve basé sur la théorie des types dépendants ; son mécanisme d'extraction peut générer du code exécutable certifié directement à partir d'une spécification dont la correction a été prouvée, créant une chaîne de la preuve au binaire en cours d'exécution. Il a été utilisé pour vérifier des algorithmes cryptographiques et des transformations de compilateurs. Isabelle/HOL fournit une logique d'ordre supérieur avec des tactiques puissantes pour l'automatisation ; son adoption industrielle comprend la preuve du microkernel seL4 — la plus grande preuve mécanisée de correction logicielle jamais réalisée — qui a démontré que le binaire exécutable implémente correctement sa spécification formelle. PVS, développé au SRI International, a été conçu spécifiquement pour la spécification logicielle et a été appliqué à des logiciels de vol de la NASA et à la logique de systèmes de sûreté nucléaire. Chacun a été utilisé dans des contextes de défense : Coq pour les preuves de protocoles et d'algorithmes, Isabelle pour les logiciels de systèmes d'exploitation et de plateforme, PVS pour le raisonnement au niveau spécification en avionique et systèmes spatiaux.

Génération d'obligations de preuve. Les flux de travail modernes de méthodes formelles génèrent automatiquement des obligations de preuve à partir de code source annoté, réduisant la charge de l'écriture de spécifications de zéro. Des outils tels que Frama-C avec son plugin WP (Weakest Precondition) analysent le code source C annoté avec des contrats ACSL (ANSI/ISO C Specification Language) et génèrent des obligations de preuve pouvant être déchargées par des prouveurs automatisés (Alt-Ergo, CVC4, Z3) ou par des prouveurs de théorèmes interactifs lorsque l'automatisation échoue. Le langage SPARK pour Ada offre un flux de travail intégré similaire : le code SPARK est écrit avec des contrats de pré/postconditions, et GNATprove génère et tente de décharger automatiquement les obligations de preuve, ne faisant appel à la preuve interactive que pour les obligations que l'automatisation ne peut pas traiter. Cette approche hybride — maximisant l'automatisation tout en réservant la preuve guidée par l'homme pour les cas difficiles — est le modèle pratique pour les programmes de défense qui ne peuvent pas doter une équipe de théoriciens de la preuve.

Le compromis lié à la courbe d'apprentissage. L'écart entre la valeur que la démonstration de théorèmes peut apporter et l'investissement organisationnel requis constitue le défi central de l'adoption de cette technique. Écrire des spécifications en Coq ou Isabelle nécessite une maîtrise de la logique d'ordre supérieur et de la théorie des types que la formation standard en génie logiciel ne dispense pas. Le développement de preuves se mesure en mois-ingénieurs pour des composants non triviaux. Les programmes qui sous-estiment cet investissement dépassent systématiquement les délais. La voie réaliste consiste à acheter des travaux de démonstration de théorèmes auprès d'organisations qui disposent déjà de cette capacité, et à en limiter le périmètre aux composants pour lesquels aucune autre technique n'est adéquate — typiquement les algorithmes sur lesquels repose l'argumentaire de sûreté.

Interprétation abstraite et analyse statique fiable

L'interprétation abstraite occupe un terrain pratique intermédiaire entre l'analyse statique conventionnelle (qui produit généralement des résultats non fiables — elle peut manquer des erreurs) et la démonstration de théorèmes (qui est fiable mais nécessite un effort manuel). Un outil d'interprétation abstraite calcule une sur-approximation fiable : s'il ne signale aucune erreur, le programme concret est garanti ne pas avoir d'erreur de cette classe. S'il signale une erreur potentielle, le programme peut ou non avoir l'erreur — le rapport est une alarme conservatrice qui doit être examinée.

Astrée. Astrée (développé à l'ENS Paris/INRIA et commercialisé par AbsInt) est l'outil d'interprétation abstraite le plus éminent dans les contextes de défense et d'aérospatiale. Il analyse le code source C pour les classes d'erreurs d'exécution suivantes : débordement entier par excès et par défaut (signé et non signé), division par zéro, déréférencement de pointeur nul, accès tableau hors limites, décalages de bits invalides et lectures de variables non initialisées. Il a été utilisé pour prouver l'absence d'erreurs d'exécution dans le logiciel de vol primaire de l'Airbus A380 — environ 132 000 lignes de C avec zéro alarme non résolue après analyse. Pour les logiciels embarqués de défense, Astrée est appliqué au niveau module ; chaque module doit atteindre zéro alarme réelle avant d'être considéré comme formellement vérifié pour l'absence d'erreurs d'exécution.

Polyspace de MathWorks. Polyspace Bug Finder et Polyspace Code Prover offrent des capacités similaires d'interprétation abstraite, avec une intégration plus étroite dans la chaîne d'outils MathWorks (développement basé sur des modèles MATLAB/Simulink) courante dans les systèmes embarqués de défense. Code Prover utilise l'interprétation abstraite basée sur les intervalles pour prouver — et non simplement détecter — l'absence de certaines classes d'erreurs et classe chaque vérification comme Prouvée (aucune erreur possible), Non prouvée (impossible à déterminer) ou Erreur (défaut confirmé). Astrée et Polyspace fournissent tous les deux des kits de qualification d'outils DO-330, réduisant la charge d'artefacts de programme pour le crédit réglementaire.

Classe d'erreur	Astrée	Polyspace Code Prover	Fiabilité
Débordement entier par excès / défaut	Oui	Oui	Fiable (aucun manqué)
Déréférencement de pointeur nul	Oui	Oui	Fiable (aucun manqué)
Division par zéro	Oui	Oui	Fiable (aucun manqué)
Accès tableau hors limites	Oui	Oui	Fiable (aucun manqué)
Lectures de variables non initialisées	Oui	Oui	Fiable (aucun manqué)

Gestion des faux positifs. Les outils fiables signalent de manière conservatrice : dans le doute, ils déclenchent une alarme. Dans les grandes bases de code C avec de l'arithmétique de pointeurs complexe, des stubs d'environnement pour des interfaces matérielles non modélisées, ou des extensions de compilateurs spécifiques à la plateforme, les taux de faux positifs peuvent être élevés — 30 à 70 % lors d'une première exécution n'est pas inhabituel. La discipline consiste à annoter chaque faux positif avec une justification lisible par machine que l'outil accepte comme suppression, de sorte que l'alarme supprimée ne réapparaisse pas lors des exécutions ultérieures. Chaque suppression est une affirmation — « cette alarme ne peut pas se produire à l'exécution car [raison] » — et les affirmations doivent être examinées lors des inspections de code dans le cadre de l'argumentaire de sûreté. Le journal de suppressions est lui-même un artefact de sûreté ; un module avec un nombre élevé de suppressions mérite une attention particulière.

Application des méthodes formelles aux logiciels DO-178C DAL A

DO-178C, la principale norme de certification pour les logiciels embarqués aéronautiques et la norme le plus souvent appliquée par analogie à d'autres plateformes de défense critiques, comprend un supplément sur les méthodes formelles — DO-333 (Formal Methods Supplement to DO-178C and DO-278A) — qui définit comment les activités d'analyse formelle peuvent satisfaire les objectifs de vérification DO-178C.

Supplément versus remplacement des tests. Une idée fausse courante est que la vérification formelle élimine le besoin de tests dans le cadre de DO-178C. DO-333 ne le soutient pas. Les méthodes formelles sont un supplément : elles peuvent fournir un crédit pour des objectifs de vérification spécifiques que les tests satisferaient sinon, réduisant le périmètre des tests, mais elles ne remplacent pas l'ensemble des exigences de tests. L'application typique consiste à utiliser l'analyse formelle pour satisfaire les objectifs de couverture structurelle — une preuve d'interprétation abstraite fiable qu'aucune erreur d'exécution n'est atteignable dans un module fournit une assurance équivalente à l'exécution de chaque branche de ce module et peut être réclamée comme crédit de couverture — tandis que les tests conventionnels continuent de satisfaire les objectifs de tests basés sur les exigences. L'effet net est une réduction de la taille de la suite de tests pour les modules DAL A avec une profondeur d'assurance accrue pour les propriétés que l'analyse formelle cible.

Documentation PSAC et SAS. Le Plan for Software Aspects of Certification (PSAC) doit décrire l'approche des méthodes formelles dès le début du programme : quelles méthodes formelles sont utilisées, quels objectifs DO-178C elles adressent, quels outils sont utilisés et comment les outils seront qualifiés. Cet artefact de planification est examiné par l'autorité de certification avant le début des travaux de vérification formelle — présenter une revendication de méthodes formelles au certificateur uniquement après achèvement est un échec de processus qui peut invalider le crédit. Le Software Accomplishment Summary (SAS) documente les activités de vérification formelle comme complétées et fournit une traçabilité de chaque résultat formel vers l'objectif DO-178C qu'il satisfait. Les preuves de vérification formelle — sorties d'exécution d'outils, fichiers de propriétés, fichiers de modèles, enregistrements de disposition des alarmes — sont conservées dans le système de gestion de configuration comme partie des données du cycle de vie de certification.

Qualification des outils. DO-330 définit les exigences de qualification pour les outils logiciels utilisés dans le développement de logiciels embarqués aéronautiques. Les outils dont la sortie est utilisée sans vérification indépendante dans le dossier de conformité nécessitent une qualification proportionnelle au DAL et au rôle de l'outil. Les outils d'interprétation abstraite utilisés pour satisfaire les objectifs de vérification DAL A nécessitent une qualification TQL-1 — le niveau le plus rigoureux. Des outils commerciaux comme Astrée et Polyspace fournissent des kits de support à la qualification qui comprennent les exigences opérationnelles de l'outil, les procédures de test de qualification et les résultats des tests de qualification. La responsabilité du programme est d'établir que le kit s'applique à son contexte d'utilisation : le compilateur spécifique, le système d'exploitation et le sous-ensemble du langage utilisés. Les outils open source sans kits de qualification existants obligent le programme à générer tous les artefacts de qualification de zéro — un coût de programme substantiel qui doit être inclus dans le plan de projet dès le premier jour.

Principe clé DO-178C / DO-333 : Le crédit accordé aux méthodes formelles dans le dossier de conformité est obtenu par la qualité de l'argumentaire de traçabilité — démontrant que la propriété formelle vérifiée correspond exactement à l'exigence de sûreté qu'elle est censée satisfaire. Une propriété formellement vérifiée qui ne capture qu'approximativement l'exigence ne fournit aucun crédit réglementaire et peut affaiblir plutôt que renforcer l'argumentaire de sûreté.

Élimination des dangers MIL-STD-882 et vérification formelle

MIL-STD-882E (System Safety) définit la hiérarchie préférée des contrôles de dangers par ordre décroissant d'efficacité : éliminer le danger, réduire la probabilité d'occurrence, ajouter la détection ou l'avertissement, et accepter le risque résiduel avec une justification documentée. La vérification formelle contribue directement aux deux premiers niveaux et fournit l'argumentaire de sûreté le plus défendable lorsqu'elle le fait.

Élimination des dangers par preuve d'impossibilité. Lorsqu'une preuve de model checking démontre qu'une propriété temporelle est vérifiée pour tous les états atteignables — par exemple, que le circuit de mise à feu ne peut jamais être alimenté lorsque l'indicateur de verrouillage de sécurité est activé — elle constitue une affirmation d'élimination du danger pour le chemin causal logiciel de ce danger. L'entrée du journal des dangers pour le danger correspondant peut être mise à jour pour refléter que le chemin causal logiciel a été éliminé par preuve formelle, et l'évaluation du risque résiduel ne reflète que les chemins causaux matériels qui demeurent non traités. C'est catégoriquement plus solide que l'argument de réduction du risque issu des tests, qui peut seulement établir que le danger n'a pas été déclenché lors des runs de test.

Crédit de réduction de probabilité issu de l'analyse fiable. Là où l'élimination n'est pas réalisable — parce que le danger dépend de conditions extérieures au contrôle du logiciel — l'analyse formelle fournit une borne sur la contribution du logiciel à la probabilité de défaillance. Une preuve d'interprétation abstraite qu'un débordement entier ne peut pas se produire dans l'algorithme de navigation borne le taux de corruption silencieuse des données à zéro pour cette classe d'erreur, réduisant directement le terme de taux de défaillance logicielle dans l'évaluation probabiliste des risques. Cette borne est plus défendable qu'une estimation du taux de défaillance dérivée des tests car la borne formelle est exacte dans les hypothèses du modèle, alors que l'estimation dérivée des tests est un intervalle de confiance sur un échantillon fini.

Traçabilité des preuves formelles vers les causes de dangers. L'argumentaire de sûreté n'est complet que lorsque chaque résultat formel est explicitement tracé vers la cause du danger qu'il adresse. La chaîne de traçabilité est : propriété formelle → exigence logicielle → cause de danger logicielle → entrée dans l'analyse des dangers du système. Cette chaîne doit être documentée dans le document d'analyse de sûreté logicielle et référencée dans le dossier de preuves de vérification formelle. Une preuve formelle qui existe sans cette traçabilité est un actif d'assurance qualité mais pas un argumentaire de sûreté — elle démontre une activité de vérification sans démontrer d'impact sur la sûreté.

Relier les résultats de la vérification formelle à la discipline plus large du DevSecOps pour les pipelines de défense signifie que les exécutions d'analyse formelle peuvent être intégrées dans le pipeline d'intégration continue comme des portes automatisées — bloquant l'intégration de tout module qui introduit de nouvelles alarmes non résolues — plutôt qu'être exécutées uniquement comme activités de certification en fin de cycle.

Intégration pratique dans un projet de logiciel de défense

Le défi central de l'introduction de la vérification formelle dans un projet de logiciel de défense n'est pas technique — les outils existent et les techniques sont matures. C'est l'allocation des ressources : les méthodes formelles nécessitent un investissement qui doit être justifié par rapport aux priorités concurrentes du programme, et l'investissement est frontal tandis que les bénéfices sont réalisés tardivement.

Où investir : algorithmes critiques versus couches d'intégration. Le retour sur investissement de la vérification formelle est le plus élevé là où le composant est mathématiquement précis, suffisamment petit pour être modélisé de manière traitable et porte un danger de haute sévérité. Les algorithmes de loi de commande, la logique d'ordonnancement, le séquençage des verrous de sécurité et les implémentations de primitives cryptographiques sont les cibles canoniques. À l'inverse, les grands composants de la couche d'intégration, le code d'interface utilisateur, les couches de marshalling de données et la logique de gestion de configuration ont des interfaces complexes et une faible précision mathématique — l'effort d'écriture de spécifications avoisine l'effort d'implémentation, et le modèle formel doit être maintenu en parallèle avec le code. Une règle empirique défendable : appliquer les méthodes formelles là où le comportement du composant peut être spécifié en moins de pages qu'il ne peut être implémenté, et là où la propriété spécifiée correspond directement à une cause de danger dans l'analyse des dangers du système.

Exigences en compétences d'équipe. Les outils d'interprétation abstraite sont le point d'entrée à la barrière la plus basse et doivent être introduits en premier. Les ingénieurs ayant un background embarqué C/C++ peuvent opérer Astrée ou Polyspace de manière productive après quelques jours de formation ; la compétence principale est le tri des alarmes — distinguer les défauts réels des faux positifs. Le model checking nécessite des ingénieurs capables d'écrire des modèles Promela ou SMV et d'exprimer des propriétés en LTL/CTL ; cette compétence prend des semaines voire des mois à développer, n'est pas largement enseignée et doit être prise en compte dans les plans d'embauche ou de formation dès le début du programme. La démonstration de théorèmes nécessite une expertise en logique formelle et en théorie des preuves que la plupart des programmes devront contracter auprès d'organisations spécialisées plutôt que développer en interne. Planifier les effectifs en méthodes formelles comme une réflexion après coup — « on verra qui fera la vérification formelle quand on en aura besoin » — est la cause unique la plus courante de non-exécution des plans de méthodes formelles.

Attentes réalistes coût-bénéfice. Une attente réaliste pour un programme introduisant l'interprétation abstraite dans les modules DAL A est une réduction de 15 à 30 % des cas de test requis pour la couverture structurelle, compensée par environ 5 à 10 % d'effort ingénieur supplémentaire pour le tri des alarmes et la documentation des suppressions lors du premier cycle de programme. Dès le deuxième cycle, la familiarité avec les patterns d'alarmes de l'outil pour la base de code spécifique réduit la charge de tri, et le bénéfice net s'améliore. Le model checking pour les machines à états ajoute 10 à 20 % de coût à la phase de conception des composants spécifiques ciblés mais élimine toute une classe de défauts — violations de machines à états, erreurs de protocole — qui seraient autrement trouvés lors des tests d'intégration ou sur le terrain. La démonstration de théorèmes est la technique la plus coûteuse et la plus valorisante et doit être évaluée composant par composant avec une documentation explicite coût-bénéfice avant tout engagement.

Interprétation abstraite (Astrée, Polyspace) : barrière la plus basse, outillage mature, kits DO-330 disponibles — appliquer à tous les modules C/C++ DAL A
Model checking (SPIN, NuSMV) : appliquer aux machines à états, protocoles et logique de transition de modes là où l'espace d'états est traitable
Démonstration de théorèmes (Coq, Isabelle/HOL, PVS, SPARK/GNATprove) : réserver aux algorithmes où la correction mathématique est un argumentaire de sûreté primaire et aucune autre technique n'est adéquate
Qualification des outils : planifier le TQL DO-330 dans le PSAC ; utiliser les kits de qualification commerciaux si disponibles ; budgétiser explicitement la qualification des outils open source
Traçabilité MIL-STD-882 : tracer chaque résultat formel vers une cause de danger avant de revendiquer un crédit de sûreté — une vérification non traçable n'est pas un argumentaire de sûreté

Les programmes qui intègrent avec succès la vérification formelle la traitent comme une discipline d'ingénierie de premier ordre avec du personnel dédié, une qualification planifiée des outils, une traçabilité explicite des exigences et un périmètre réaliste limité aux composants où les méthodes formelles modifient la classification de sûreté d'un danger. Les programmes qui traitent la vérification formelle comme une case à cocher de conformité à ajouter en fin de développement constatent systématiquement que l'analyse formelle ne soutient pas la revendication de conformité car le code n'a pas été conçu en pensant à l'analyse formelle. La conception et le modèle formel doivent être codéveloppés — la discipline de spécification qu'exigent les méthodes formelles est aussi précieuse que la preuve elle-même.

Intégrer la vérification formelle dans votre programme de logiciel de défense

Corvus Intelligence applique les méthodes formelles — interprétation abstraite, model checking et démonstration de théorèmes — aux programmes de logiciels de défense critiques opérant sous DO-178C et MIL-STD-882. Si votre programme nécessite une assurance DAL A ou doit renforcer un argumentaire de sûreté logicielle, nous sommes disponibles pour discuter de vos exigences de vérification.

Développement logiciel de défense → Réserver un briefing

Cette analyse a été préparée par les ingénieurs de Corvus Intelligence qui conçoivent et vérifient des logiciels critiques pour des organisations de défense et gouvernementales. En savoir plus sur notre équipe →

Questions fréquentes

Qu'est-ce que la vérification formelle et en quoi diffère-t-elle des tests logiciels ?

La vérification formelle utilise des techniques de preuve mathématique pour démontrer qu'un système logiciel satisfait une spécification précisément énoncée, tandis que les tests exécutent le programme sur un ensemble fini d'entrées et observent les sorties. La différence fondamentale est la complétude : les tests peuvent montrer la présence d'erreurs mais ne peuvent pas prouver leur absence, car aucune suite de tests finie ne couvre toutes les entrées et tous les états possibles. La vérification formelle raisonne sur l'espace complet des comportements possibles — lorsqu'elle réussit, elle fournit une garantie valable pour chaque exécution, pas seulement pour celles qui ont été exercées. En pratique, cela signifie que les méthodes formelles complètent les tests plutôt qu'ils ne les remplacent : elles sont appliquées aux propriétés les plus critiques là où le coût des erreurs non découvertes est le plus élevé et où la couverture par tests est structurellement impossible à atteindre. Pour les logiciels de défense critiques, même un seul chemin non exercé contenant un mode de défaillance peut constituer un risque de sûreté inacceptable — c'est exactement la lacune que les méthodes formelles comblent.

Qu'est-ce que le model checking et quels types de propriétés peut-il vérifier ?

Le model checking est une technique de vérification formelle qui explore exhaustivement tous les états atteignables d'un modèle à états finis d'un système, vérifiant à chaque état si une propriété donnée exprimée en logique temporelle est vérifiée. Les propriétés LTL expriment des exigences sur des séquences d'états dans le temps — par exemple, « chaque fois que l'indicateur d'armement d'arme est activé, le verrou de sécurité doit avoir été libéré dans l'état précédent ». Les propriétés CTL raisonnent sur les futurs ramifiés — « il est toujours possible d'atteindre un état sûr depuis tout état atteignable ». Les applications typiques en défense comprennent la vérification des machines à états des protocoles de communication, la vérification que tous les chemins à travers un graphe de flux de contrôle satisfont un invariant de sûreté donné, et la confirmation qu'aucune séquence d'entrées valides ne peut conduire le système dans une configuration interdite. Les model checkers comme SPIN et NuSMV produisent une trace de contre-exemple lorsqu'une propriété échoue, faisant de CEGAR un flux de travail itératif pratique.

Qu'est-ce que le problème d'explosion des états en model checking ?

Le problème d'explosion des états est la croissance exponentielle de l'espace d'états qui doit être exploré à mesure que le nombre de composants concurrents ou de variables de données augmente. Un système avec N variables booléennes a 2^N états possibles ; un système avec N threads concurrents ayant chacun K états a K^N états combinés. En pratique, même de petits systèmes embarqués peuvent produire des espaces d'états avec des milliards d'états atteignables qui épuisent la mémoire disponible avant la fin de l'exploration. Les model checkers modernes y remédient via les Binary Decision Diagrams (BDDs) qui représentent les ensembles d'états symboliquement, CEGAR qui raffine les abstractions uniquement là où des contre-exemples parasites apparaissent, la réduction d'ordre partiel qui élimine les entrelacement d'événements concurrents équivalents, et le bounded model checking qui utilise des solveurs SAT pour vérifier les propriétés jusqu'à une longueur de chemin fixe — suffisant pour la plupart des propriétés de sûreté. Pour les logiciels de défense, limiter le périmètre du model checking à des sous-systèmes critiques spécifiques maintient l'espace d'états traitable tout en concentrant l'effort de vérification là où c'est le plus important.

Que sont les démonstrateurs de théorèmes et lesquels sont utilisés en vérification de logiciels de défense ?

Les démonstrateurs de théorèmes sont des outils qui aident les ingénieurs à construire des preuves mathématiques vérifiées par machine de propriétés logicielles. Contrairement aux model checkers, les démonstrateurs de théorèmes ne sont pas limités par la taille de l'espace d'états et peuvent raisonner sur des domaines infinis — comprenant les nombres réels, les entiers non bornés et les algorithmes paramétrés. Les trois démonstrateurs les plus souvent rencontrés en vérification formelle de défense et aérospatiale sont Coq, Isabelle/HOL et PVS. Le mécanisme d'extraction de Coq peut générer du code exécutable certifié directement à partir de spécifications vérifiées. Isabelle/HOL a connu une utilisation industrielle majeure, notamment dans la preuve du microkernel seL4. PVS a été conçu spécifiquement pour la spécification logicielle et a été appliqué aux logiciels de vol de la NASA et à la logique de systèmes de sûreté nucléaire. Les trois nécessitent une expertise spécialisée substantielle et un investissement initial significatif dans l'écriture de spécifications, ce qui explique pourquoi les programmes les réservent généralement aux algorithmes de plus haute criticité pour lesquels aucune autre technique ne fournit une assurance adéquate.

Qu'est-ce que l'interprétation abstraite et comment Astrée l'utilise-t-il ?

L'interprétation abstraite est un cadre mathématique pour calculer des sur-approximations fiables de la sémantique des programmes. Au lieu de suivre les valeurs exactes qu'une variable pourrait prendre, un interpréteur abstrait suit une abstraction — comme l'intervalle dans lequel la variable est garantie de se trouver. Si le calcul abstrait se termine sans détecter d'erreur dans aucun état abstrait, l'outil garantit que le programme concret est également exempt de cette classe d'erreur. Astrée applique l'interprétation abstraite pour prouver l'absence d'erreurs d'exécution dans les programmes C — débordement entier, division par zéro, déréférencement de pointeur nul, accès tableau hors limites et lectures non initialisées. Il a été utilisé pour vérifier le logiciel de vol primaire de l'Airbus A380 avec zéro alarme non résolue. Pour les logiciels embarqués de défense, Astrée et MathWorks Polyspace Code Prover sont appliqués pour prouver que les modules critiques ne lèveront jamais d'exception d'exécution sous aucune entrée, satisfaisant les exigences clés pour DO-178C DAL A et l'élimination des dangers logiciels MIL-STD-882.

Comment DO-178C intègre-t-il les méthodes formelles ?

DO-178C inclut un supplément sur les méthodes formelles — DO-333 (Formal Methods Supplement to DO-178C and DO-278A) — qui définit comment les activités d'analyse formelle peuvent satisfaire les objectifs de vérification DO-178C. Sous DO-333, une méthode formelle peut fournir un crédit pour les exigences de couverture structurelle : une preuve qu'une propriété est vérifiée pour tous les états atteignables fournit une assurance équivalente à la couverture MC/DC des chemins de code correspondants, à condition que la méthode formelle soit fiable et que la propriété soit démontrée comme impliquant l'exigence de sûreté. Le supplément exige que le modèle formel représente fidèlement l'implémentation, que toutes les hypothèses soient explicitement énoncées et justifiées, et que les outils utilisés soient qualifiés conformément à DO-330. Les méthodes formelles complètent plutôt que remplacent les tests sous DO-178C — elles réduisent la charge de tests pour des objectifs spécifiques tout en augmentant la profondeur d'assurance pour les propriétés formellement analysées. Le PSAC doit décrire l'approche des méthodes formelles dès le début du programme.

Comment MIL-STD-882 relie-t-il la vérification formelle au crédit de réduction des dangers ?

MIL-STD-882E définit une matrice de risques basée sur la sévérité des dangers et la probabilité d'occurrence, avec une hiérarchie de mitigation préférée : éliminer le danger, réduire la probabilité, ajouter détection et avertissement, puis accepter le risque résiduel. La vérification formelle contribue aux deux premiers niveaux. Une preuve de model checking que la logique de déclenchement d'arme ne peut jamais être activée sans la libération du verrou de sécurité et la confirmation de l'opérateur dans le bon ordre constitue une élimination du danger pour le chemin causal logiciel de ce danger. Là où l'élimination n'est pas réalisable, une preuve fiable d'interprétation abstraite délimitant le taux de défaillance induite par le logiciel fournit des preuves pour le crédit de réduction de probabilité revendiqué dans l'analyse des dangers. L'étape de documentation clé est de tracer chaque résultat formel vers une cause de danger spécifique dans l'analyse des dangers du système — cette traçabilité convertit une activité de vérification en argumentaire de sûreté reconnu.

Quel est le compromis réaliste coût-bénéfice de la vérification formelle dans un programme de défense ?

La vérification formelle comporte des coûts initiaux significatifs : construction de modèles formels, rédaction de spécifications, formation des ingénieurs et qualification des outils pour un crédit réglementaire. Les bénéfices sont élevés mais inégalement répartis : les méthodes formelles offrent une forte valeur pour les petits composants mathématiquement précis — algorithmes d'ordonnancement, machines à états, logique de verrouillage de sécurité — et une faible valeur pour le code d'intégration de grande taille où la spécification serait aussi complexe que l'implémentation. Attentes réalistes : l'interprétation abstraite ajoute 5 à 10 % d'effort ingénieur en contrepartie d'une réduction de 15 à 30 % des cas de test requis ; le model checking ajoute 10 à 20 % de coût à la phase de conception pour les machines à états ciblées mais élimine toute une classe de défauts trouvés sinon en tests d'intégration ; la démonstration de théorèmes porte le coût le plus élevé et doit être évaluée composant par composant avec une justification explicite avant engagement. Les programmes qui appliquent les méthodes formelles de manière sélective aux bons composants récupèrent leur investissement ; ceux qui les appliquent indistinctement dépassent les délais et le budget.

Quelle qualification d'outils est requise lors de l'utilisation d'outils d'analyse formelle pour un crédit DO-178C ?

DO-178C §12.2 exige que les outils logiciels soient qualifiés lorsque leur sortie est utilisée sans vérification indépendante. DO-330 définit les niveaux de qualification des outils (TQL-1 à TQL-5) en fonction du rôle de l'outil et du niveau d'assurance de développement. Un outil d'analyse formelle utilisé pour satisfaire un objectif de vérification DO-178C DAL A tombe au niveau TQL-1 ou TQL-2, nécessitant les artefacts de qualification les plus rigoureux : exigences opérationnelles de l'outil, plan de qualification de l'outil, résumé d'accomplissement de la qualification et preuves de résultats corrects pour le cas d'utilisation pertinent. Les outils commerciaux comme Astrée et Polyspace fournissent des kits de qualification préexistants qui réduisent la charge du programme à démontrer que le kit s'applique à leur contexte d'utilisation spécifique et à leur configuration de compilateur. Les outils open source nécessitent généralement une qualification complète de zéro — un coût de programme substantiel qui doit être inclus dans le plan de projet dès le début.

Quelles compétences d'équipe sont nécessaires pour introduire la vérification formelle dans une équipe de logiciels de défense ?

Les outils d'interprétation abstraite comme Astrée et Polyspace sont le point d'entrée à la barrière la plus basse et peuvent être opérés par des ingénieurs ayant un background C/C++ après quelques jours de formation — la compétence principale est le tri des alarmes : distinguer les défauts réels des faux positifs dus à l'imprécision de l'abstraction. Le model checking avec SPIN ou NuSMV nécessite des ingénieurs capables d'écrire des spécifications en Promela ou SMV et d'exprimer des propriétés en LTL/CTL — une compétence qui prend des semaines voire des mois à développer et qui n'est pas enseignée dans les cursus standards. La démonstration de théorèmes avec Coq, Isabelle/HOL ou PVS nécessite une expertise approfondie en logique formelle et en théorie des preuves — des compétences que la plupart des programmes devront recruter ou sous-traiter auprès d'organisations spécialisées. La voie de dotation en personnel la plus pratique est d'introduire d'abord l'interprétation abstraite, de former des ingénieurs spécifiquement en model checking pour la vérification des machines à états, et de réserver la démonstration de théorèmes pour des travaux contractés par des spécialistes sur les composants de plus haute criticité.