⚡ electrical engineering

ESBMC-Arduino: Closing the Deployment Gap for Formal Verification of Open-Hardware PLCs

Cet article présente ESBMC-Arduino, un cadre de vérification fidèle au matériel qui comble l'écart de déploiement pour les API en matériel ouvert en intégrant une couche d'abstraction matérielle déclarative et une modélisation saine des plages d'entrée afin d'éliminer les fausses alertes causées par des hypothèses d'entiers idéalisées tout en détectant les défauts réels dépendants de la largeur de mot dans les programmes IEC 61131-3 s'exécutant sur des microcontrôleurs à ressources limitées.

Auteurs originaux : Pierre Dantas, Lucas Cordeiro, Waldir Junior

Publié 2026-07-10

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Pierre Dantas, Lucas Cordeiro, Waldir Junior

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 construisez un robot pour gérer un réservoir d'eau. Vous écrivez les instructions dans un langage spécial appelé IEC 61131-3, qui est comme un livre de recettes universel pour les machines industrielles. Pendant des années, des ingénieurs ont utilisé des simulateurs de « super-robots » pour vérifier si ces recettes sont sûres. Ces simulateurs sont comme des sorciers capables de réfléchir avec des nombres infinis ; ils supposent que le robot peut garder n'importe quel nombre dans sa tête, de moins l'infini à plus l'infini, et que les capteurs peuvent rapporter n'importe quelle valeur imaginable.

Mais voici le rebondissement : le robot que vous construisez réellement n'est pas un sorcier. C'est un minuscule microcontrôleur bon marché (comme un Arduino) qui vit dans le monde réel. Cette petite puce a un cerveau très spécifique et limité. Elle ne peut contenir que des nombres allant jusqu'à 32 767. Si un calcul dépasse ce chiffre, le nombre ne devient pas simplement plus grand ; il se brise, revient brusquement au bas de l'échelle, et devient un nombre négatif. C'est comme un odomètre de voiture qui revient de 999 999 à 000 000.

Le Grand Décalage
L'article appelle cela le « écart de déploiement » (deployment gap). C'est la différence entre le monde des rêves du sorcier et la réalité étroite du robot.

Les auteurs ont découvert que lorsque les ingénieurs utilisaient les anciens simulateurs de « sorciers » pour vérifier leur code, ils obtenaient une quantité massive de fausses alertes. Sur les 123 programmes réels qu'ils ont testés, les anciens simulateurs ont hurlé « DANGER ! » 54 fois (un taux de fausses alarmes de 44 %). Mais en regardant de plus près, ils se sont rendu compte que ces « dangers » étaient impossibles. Les simulateurs imaginaient des lectures de capteurs comme -32 764. Dans le monde réel, un capteur connecté à ce robot ne peut lire que des nombres compris entre 0 et 1 023 (parce qu'il s'agit d'un capteur 10 bits). Une valeur de -32 764 est comme un thermomètre affichant « moins 32 764 degrés » — cela ne peut tout simplement pas arriver.

L'article soutient que de compter sur ces anciens simulateurs revient à utiliser un garde de sécurité qui crie « Intrusion ! » parce qu'il a vu un fantôme. Le garde est techniquement « correct » concernant le fantôme, mais inutile parce que les fantômes n'existent pas. Les auteurs excluent explicitement l'idée que l'on puisse simplement vérifier les erreurs mathématiques sans aussi vérifier ce que les capteurs peuvent réellement voir. Ils montrent que faire cela rend la vérification « non fiable » (unsound) en pratique.

La Solution Magique : Le Descripteur HAL
Pour correr cela, les auteurs ont construit un nouvel outil appelé ESBMC-Arduino. Considérez cet outil comme un filtre de « Vérification de la Réalité ».

Avant que le simulateur du sorcier n'examine le code, ce nouvel outil attache une petite note automatique à chaque capteur. Il dit : « Hé, souviens-toi, ce capteur ne peut donner que des nombres entre 0 et 1 023 ». Il rappelle également au simulateur : « Et souviens-toi, le cerveau du robot ne peut contenir que des nombres jusqu'à 32 767 ».

Lorsque le simulateur fonctionne avec ces règles, la magie opère :

Les 54 fausses alarmes disparaissent instantanément. Le fantôme de -32 764 a disparu car le simulateur sait désormais que ce nombre est impossible.
Les 32 programmes qui étaient déjà prouvés sûrs restent sûrs.
Plus important encore, l'outil n'a manqué aucun vrai bug. Il a découvert que les anciens simulateurs cachaient un type spécifique de danger réel : lorsqu'une lecture de capteur est multipliée par un grand nombre (comme transformer une valeur brute de capteur en pourcentage), le calcul peut déborder le cerveau minuscule du robot.

Le Vrai Danger (et sa rareté)
L'article a révélé que, bien que les « alarmes fantômes » fussent courantes, les vrais bugs causés par ce décalage étaient en fait assez rares dans le code public testé. Ils n'ont trouvé des défauts réels que dans des scénarios spécifiques où une lecture de capteur est multipliée par une constante élevée (comme 100) sur une carte 16 bits.

Par exemple, si un capteur lit 898 (une valeur normale et réelle), et que le code le multiplie par 100, le résultat est 89 800. C'est trop grand pour le cerveau 16 bits du robot (maximum 32 767). Le nombre boucle, devient un nombre négatif, et le robot pense que le réservoir d'eau est vide alors qu'il est en train de déborder. Le nouvel outil a détecté exactement ce scénario et a fourni aux ingénieurs un exemple physique réel de la lecture de capteur qui provoquerait le crash.

Ce que l'Article Ne Prétend Pas
Les auteurs sont très honnêtes sur ce qu'ils n'ont pas fait. Ils n'ont pas prouvé que chaque programme est désormais sûr. Sur les 123 programmes, 91 se sont retrouvés avec un verdict « inconnu ». Ce n'est pas parce que l'outil est défectueux, mais parce que le calcul pour prouver la sécurité de ces programmes spécifiques est trop difficile pour le moteur actuel. L'outil a réussi à éliminer le bruit (les fausses alarmes) et à conserver le signal (les vraies preuves), mais il n'a pas encore résolu les énigmes les plus difficiles.

De plus, ils n'ont pas testé cela sur des nombres à virgule flottante (des décimales comme 3,14) ou des simulations physiques complexes. Ils se sont concentrés strictement sur les nombres entiers et la logique booléenne (interrupteurs on/off).

L'Essentiel
Cet article démontre que pour vérifier les automates programmables industriels (PLC) à matériel ouvert (comme ceux utilisés dans les écoles et les petites usines), on ne peut pas se contenter de vérifier les mathématiques ; il faut aussi vérifier les limites du matériel. En ajoutant automatiquement une « Vérification de la Réalité » qui indique au simulateur ce que les capteurs peuvent réellement faire, ils ont transformé un outil bruyant et peu fiable en un outil digne de confiance. Ils n'ont pas trouvé un million de nouveaux bugs, mais ils ont empêché l'outil de crier au loup, rendant possible pour les ingénieurs de faire à nouveau confiance aux vérifications de sécurité.

Résumé Technique : ESBMC-ARDUINO

Problème : Le fossé de déploiement dans les API Open-Hardware
Les automates programmables industriels (API) en matériel ouvert (open-hardware), tels qu'OpenPLC tournant sur Arduino OPTA, CONTROLLINO et Industrial Shields M-Duino, ont démocratisé la programmation IEC 61131-3 pour les dispositcules de classe microcontrôleur à bas coût. Ces plateformes sont de plus en plus utilisées dans l'éducation, l'automatisation à petite échelle et comme substrat d'exécution pour la recherche en sécurité des systèmes de contrôle industriel (ICS). Cependant, un « fossé de déploiement » critique existe entre les modèles abstraits utilisés par les vérificateurs open-source existants (par exemple, ESBMC-PLC, PLCverif) et l'environnement d'exécution matériel réel.

Les vérificateurs actuels opèrent sur un modèle de cycle de balayage (scan-cycle) abstrait supposant des entiers idéalisés et non bornés et des entrées non contraintes. En revanche, les artefacts déployés fonctionnent sur des unités de microcontrôleurs (MCU) à ressources limitées avec des largeurs de mots machines spécifiques (par exemple, un int de 16 bits sur les cartes AVR 8 bits) et des convertisseurs analogique-numérique (CAN) à résolution finie (typiquement 10 bits, produisant des valeurs dans $[0, 1023]$ ). Cette divergence conduit à deux modes de défaillance :

Défauts manqués : Un programme peut être prouvé sûr dans le modèle abstrait mais non sûr sur le dispositif en raison d'un dépassement d'entier (integer overflow) causé par des largeurs de mots étroites (par exemple, un calcul de mise à l'échelle qui boucle sur une carte 16 bits).
Fausses alarmes (Faux positifs) : Plus critique encore, une vérification sensible à la largeur qui prend en compte la largeur du mot mais ignore les limites d'entrée matérielles explore des valeurs de capteurs qu'aucun CAN physique ne peut produire (par exemple, des valeurs négatives ou dépassant 1023). Cela génère des rapports de dépassement spécieux. L'évaluation sur un corpus de 123 programmes tiers réels a montré qu'une vérification naïve de dépassement 16 bits produit un taux de fausses alarmes de 44 % (54/123) tout en trouvant zéro défaut réel.

Méthodologie : Vérification fidèle au matériel
Le document propose une méthode pour combler ce fossé en construisant un « modèle de déploiement » ( $M_{dev}$ ) qui représente fidèlement le matériel cible. Le cœur de cette approche est un descripteur de couche d'abstraction matérielle (HAL) et un processus de réduction fidèle (sound lowering).

Descripteur HAL ( $H$ ) : Un tuple déclaratif $H = \langle w, b_{adc}, b_{pwm}, \mu \rangle$ $H = ⟨ w, b_{a d c}, b_{pw m}, μ ⟩$ qui capture :
- $w$ : La largeur du mot machine (par exemple, 16 bits pour AVR, 32 bits pour ARM).
- $b_{adc}$ et $b_{pwm}$ : La résolution des convertisseurs analogique-numérique et des sorties à modulation de largeur d'impulsion (PWM).
- $\mu$ : Une carte de liaison E/S dérivée automatiquement du schéma d'adressage direct IEC 61131-3 (par exemple, les adresses %IW sont mappées vers des entrées analogiques avec des plages ADC spécifiques).
Réduction fidèle (Faithful Lowering) : La méthode transforme le programme API ( $P$ $P$ ) en un modèle de déploiement ( $M_{dev}(P, H)$ $M_{d e v} (P, H)$ ) en :
- Interprétant l'arithmétique à la largeur de mot cible $w$ (reproduisant exactement le bouclage par complément à deux).
- Injectant des contraintes assume immédiatement après l'échantillonnage des entrées pour restreindre les variables à leurs plages réalisables par le matériel (par exemple, $0 \leq adc \leq 1023$ ).
- Sur-approximant les blocs de fonctions non linéaires (par exemple, PID) avec des sorties non déterministes pour maintenir la tractabilité.
Moteur de vérification : La méthode réutilise le backend ESBMC (Bounded Model Checking basé sur le SMT et $k$ -induction) sans modification. La réduction se produit dans le frontend de diagramme à contacts (Ladder Diagram - LD), en ajoutant un crochet léger (environ 40 lignes) qui impose les limites d'entrée et définit la largeur de mot de l'architecture.

Principales contributions

Méthode de vérification fidèle au matériel : Une approche formelle qui transfère la discipline de modèle cible de la programmation C embarquée critique pour la sécurité (établie par des outils comme Frama-C et Astrée) au domaine des API. Contra% aux outils de ces derniers, qui nécessitent des contrats d'entrée manuels, cette méthode dérive automatiquement les limites d'entrée à partir du schéma d'adressage standard IEC 61131-3 et des descripteurs de cartes.
Instanciation ESBMC-Arduino : Une implémentation concrète pour les cibles de classe Arduino, extrayant les paramètres HAL des cœurs officiels Arduino. Elle supporte les cibles 16 bits (AVR) et 32 bits (ARM).
Évaluation empirique : Une évaluation rigoureuse sur 123 programmes réels et un corpus contrôlé de 20 motifs.

Résultats

Élimination des fausses alarmes : Sur le corpus de 123 programmes, l'activation de l'annotateur HAL a éliminé toutes les 54 fausses alarmes (réduisant le compte d'insécurité de 54 à 0) tout en préservant chaque preuve de robustesse (32 programmes sont restés prouvés sûrs).
Détection de défauts réels : Un corpus contrôlé a démontré que la méthode détecte des défauts réels dépendants de la largeur (par exemple, un dépassement lors de la mise à l'échelle ADC-vers-pourcentage sur des cartes 16 bits) avec des témoins physiquement réalisables.
Validation croisée entre outils : Le phénomène des « fausses alarmes » a été reproduit à l'aide d'outils indépendants (CBMC et Frama-C/EVA) sur des miroirs C de la logique, confirmant que le problème est inhérent à la vérification naïve sensible à la largeur sans modélisation d'entrée, et non spécifique à ESBMC.
Performance : La surcharge de l'annotateur HAL est négligeable ; les temps de vérification restent inférieurs à une seconde par programme.
Limites : Bien que les fausses alarmes soient éliminées, 91 programmes du corpus réel ont renvoyé des verdicts « inconnu » en raison de l'incomplétude de la $k$ -induction sur les blocs de fonctions possédant un état interne. Il s'agit d'une limitation de la capacité du prouveur à fermer les étapes inductives, et non du modèle d'entrée.

Signification
L'article soutient que la valeur principale de ce travail n'est pas le nombre de bugs découverts (qui sont rares dans les corpus publics spécifiques étudiés, dominés par la logique booléenne et de temporisation), mais la restauration de la sûreté (soundness). Les auteurs démontrent qu'une vérification naïve sensible à la largeur est inutilisable pour l'assurance en raison d'un taux de fausses alarmes de 44 % qui étouffe les découvertes réelles. En dérivant automatiquement les plages d'entrée réalisables par le matériel, la méthode convertit un outil peu fiable en un outil qui ne délivre que des rapports réalisables, permettant aux ingénieurs de faire confiance aux résultats de vérification pour les API en matériel ouvert. L'approche est présentée comme une stratégie d'adoption réaliste et à faible coût (un descripteur à 4 champs et un crochet de 40 lignes) qui s'intègre à l'infrastructure de vérification mature plutôt que de proposer une solution repartant de zéro.

Articles similaires