⚡ electrical engineering

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

Questo articolo introduce ESBMC-Arduino, un framework di verifica fedele all'hardware che colma il divario di implementazione per i PLC open-hardware integrando uno strato di astrazione hardware dichiarativo e una modellazione sonora degli intervalli di input per eliminare i falsi allarmi causati da assunzioni di interi idealizzati, rilevando al contempo difetti reali dipendenti dalla larghezza nei programmi IEC 61131-3 in esecuzione su microcontrollori con risorse limitate.

Autori originali: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Pubblicato 2026-07-10

📖 5 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina di costruire un robot per gestire un serbatoio d'acqua. Scrivi le istruzioni in un linguaggio speciale chiamato IEC 61131-3, che è come un libro di ricette universale per macchine industriali. Per anni, gli ingegneri hanno usato dei simulatori "super-robot" per controllare se queste ricette sono sicure. Questi simulatori sono come maghi che possono pensare con numeri infiniti; assumono che il robot possa contenere qualsiasi numero nella sua testa, da meno infinito a più infinito, e che i sensori possano riportare qualsiasi valore immaginabile.

Ma ecco il colpo di scena: il vero robot che costruisci non è un mago. È un piccolo, economico microcontrollore (come un Arduino) che vive nel mondo reale. Questo piccolo chip ha un cervello molto specifico e limitato. Può contenere solo numeri fino a 32.767. Se un calcolo va oltre, il numero non diventa semplicemente più grande; si rompe, torna indietro verso il basso e si trasforma in un numero negativo. È come il contachilometri di un'auto che torna da 999.999 a 000.000.

Il Grande Disconnesso
Il documento chiama questo fenomeno il "deployment gap" (divario di implementazione). È la differenza tra il mondo dei sogni del mago e la realtà ristretta del robot.

Gli autori hanno scoperto che quando gli ingegneri usavano i vecchi simulatori "magici" per controllare il loro codice per la sicurezza, ottenevano un enorme numero di falsi allarmi. Su 123 programmi reali testati, i vecchi simulatori urlavano "PERICOLO!" 54 volte (un tasso di falsi allarmi del 44%). Ma guardando più da vicino, si sono resi conto che questi "pericoli" erano impossibili. I simulatori immaginavano letture dei sensori come -32.764. Nel mondo reale, un sensore collegato a questo robot può leggere solo numeri compresi tra 0 e 1.023 (perché è un sensore a 10 bit). Un valore di -32.764 è come un termometro che segna "meno 32.764 gradi": semplicemente non può accadere.

Il documento sostiene che fare affidamento su questi vecchi simulatori è come un guardia giurata che urla "Intruso!" perché ha visto un fantasma. La guardia è tecnicamente "corretta" riguardo al fantasma, ma inutile perché i fantasmi non esistono. Gli autori escludono esplicitamente l'idea che si possa semplicemente controllare gli errori matematici senza controllare anche cosa i sensori possono effettivamente vedere. Dimostrano che fare questo rende la verifica "insound" (inaffidabile) nella pratica.

La Soluzione Magica: Il Descrittore HAL
Per risolvere il problema, gli autori hanno costruito un nuovo strumento chiamato ESBMC-Arduino. Pensa a questo strumento come a un filtro di "Controllo della Realtà".

Prima che il simulatore magico analizzi il codice, questo nuovo strumento attacca una piccola nota automatica a ogni sensore. Dice: "Ehi, ricorda, questo sensore può dare solo numeri compresi tra 0 e 1.023". Inoltre, ricorda al simulatore: "E ricorda, il cervello del robot può contenere solo numeri fino a 32.767".

Quando il simulatore viene eseguito con queste regole, la magia avviene:

I 54 falsi allarmi scompaiono istantaneamente. Il fantasma di -32.764 è sparito perché il simulatore ora sa che quel numero è impossibile.
I 32 programmi che erano già stati provati sicuri rimangono sicuri.
Cosa più importante, lo strumento non ha mancato alcun bug reale. Ha scoperto che i vecchi simulatori stavano nascondendo un tipo specifico di pericolo reale: quando la lettura di un sensore viene moltiplicata per un numero grande (come trasformare il valore grezzo di un sensore in una percentuale), la matematica può causare un overflow nel minuscolo cervello del robot.

Il Vero Pericolo (e quanto è raro)
Il documento ha scoperto che, sebbene i "falsi allarmi da fantasma" fossero comuni, i veri bug causati da questo divario erano in realtà piuttosto rari nel codice pubblico testato. Hanno trovato difetti genuini solo in scenari specifici in cui la lettura di un sensore veniva moltiplicata per una costante grande (come 100) su una scheda a 16 bit.

Per esempio, se un sensore legge 898 (che è un valore normale e reale) e il codice lo moltiplica per 100, il risultato è 89.800. Questo è troppo grande per il cervello a 16 bit del robot (massimo 32.767). Il numero torna indietro, diventa un numero negativo, e il robot pensa che il serbatoio d'acqua sia vuoto quando in realtà è in pieno straripamento. Il nuovo strumento ha catturato esattamente questo scenario e ha fornito agli ingegneri un esempio fisico e reale della lettura del sensore che avrebbe causato il crash.

Cosa il Documento Non Rivendica
Gli autori sono molto onesti su ciò che non hanno fatto. Non hanno dimostrato che ogni programma è ora sicuro. Dei 123 programmi, 91 sono finiti con un verdetto di "sconosciuto". Questo non è dovuto al fatto che lo strumento è rotto, ma perché la matematica per provare la sicurezza di quei programmi specifici è troppo difficile per l'attuale motore di calcolo. Lo strumento ha rimosso con successo il rumore (i falsi allarmi) e ha mantenuto il segnale (le prove reali), ma non è riuscito a risolvere ancora tutti i puzzle più difficili.

Inoltre, non hanno testato questo su numeri in virgola mobile (decimali come 3,14) o simulazioni fisiche complesse. Si sono concentrati esclusivamente su numeri interi e logica booleana (interruttori on/off).

In Sintesi
Il documento dimostra che per verificare i PLC open-hardware (come quelli usati nelle scuole e nelle piccole fabbriche), non puoi solo controllare la matematica; devi controllare i limiti dell'hardware. Aggiungendo automaticamente un "Controllo della Realtà" che dice al simulatore cosa possono effettivamente fare i sensori, hanno trasformato uno strumento rumoroso e inaffidabile in uno affidabile. Non hanno trovato un milione di nuovi bug, ma hanno impedito allo strumento di dare il falso allarme, rendendo possibile per gli ingegneri fidarsi di nuovo dei controlli di sicurezza.

Sintesi Tecnica: ESBMC-ARDUINO

Problema: Il divario di implementazione nei PLC Open-Hardware
I Programmabili Logici Industriali (PLC) open-hardware, come OpenPLC in esecuzione su Arduino OPTA, CONTROLLINO e Industrial Shields M-Duino, hanno democratizzato la programmazione IEC 61131-3 per dispositivi di classe microcontrollore a basso costo. Queste piattaforme sono sempre più utilizzate nell'istruzione, nell'automazione su piccola scala e come substrato di runtime per la ricerca sulla sicurezza dei sistemi di controllo industriale (ICS). Tuttavia, esiste un critico "divario di implementazione" tra i modelli astratti utilizzati dai verificatori open-source esistenti (ad esempio, ESBMC-PLC, PLCverif) e l'effettivo ambiente di esecuzione hardware.

Gli attuali verificatori operano su un modello di ciclo di scansione astratto che assume interi idealizzati e illimitati e input non vincolati. Al contrario, gli artefatti implementati girano su Unità Microcontrollore (MCU) con risorse limitate, dotate di specifiche larghezze di parola macchina (ad esempio, int a 16 bit su schede AVR a 8 bit) e convertitori analogico-digitali (ADC) a risoluzione finita (tipicamente a 10 bit, che restituiscono valori nell'intervallo $[0, 1023]$ ). Questa discrepanza porta a due modalità di guasto:

Difetti Mancati: Un programma può essere dimostrato sicuro nel modello astratto ma insicuro sul dispositivo a causa di un overflow di interi causato da larghezze di parola ristrette (ad esempio, un calcolo di scala che va in wrap-up su una scheda a 16 bit).
Falsi Allarmi (Falsi Positivi): Più criticamente, una verifica consapevole della larghezza (width-aware) ingenua, che tiene conto della larghezza della parola ma ignora i limiti degli input hardware, esplora valori dei sensori che nessun ADC fisico può produrre (ad esempio, valori negativi o valori superiori a 1023). Ciò produce segnalazioni di overflow spurie. La valutazione su un corpus di 123 programmi reali di terze parti ha mostrato che un controllo ingenuo dell'overflow a 16 bit genera un tasso di falsi allarmi del 44% (54/123) pur trovando zero difetti reali.

Metodologia: Verifica fedele all'hardware
Il documento propone un metodo per colmare questo divario costruendo un "modello di implementazione" ( $M_{dev}$ ) che rappresenti fedelmente l'hardware target. Il nucleo di questo approccio è un descrittore dello strato di astrazione hardware (HAL) e un processo di riduzione (lowering) sonora.

Descrittore HAL ( $H$ ): Una tupla dichiarativa $H = \langle w, b_{adc}, b_{pwm}, \mu \rangle$ $H = ⟨ w, b_{a d c}, b_{pw m}, μ ⟩$ che cattura:
- $w$ : La larghezza della parola macchina (ad esempio, 16 bit per AVR, 32 bit per ARM).
- $b_{adc}$ e $b_{pwm}$ : La risoluzione dei convertitori analogico-digitali e delle uscite Pulse-Width Modulation.
- $\mu$ : Una mappa di binding I/O derivata automaticamente dallo schema di indirizzamento diretto IEC 61131-3 (ad esempio, gli indirizzi %IW mappano su ingressi analogici con specifici intervalli ADC).
Riduzione Fedele (Faithful Lowering): Il metodo trasforma il programma PLC ( $P$ $P$ ) in un modello di implementazione ( $M_{dev}(P, H)$ $M_{d e v} (P, H)$ ) tramite:
- L'interpretazione dell'aritmetica alla larghezza di parola target $w$ (riproducendo esattamente il wrap-around del complemento a due).
- L'iniezione di vincoli assume immediatamente dopo il campionamento dell'input per restringere le variabili ai loro intervalli realizzabili dall'hardware (ad esempio, $0 \leq adc \leq 1023$ ).
- La sovra-approssimazione di blocchi funzionali non lineari (ad esempio, PID) con output non deterministici per mantenere la trattabilità.
Motore di Verifica: Il metodo riutilizza il backend ESBMC (Bounded Model Checking basato su SMT e $k$ -induzione) senza modifiche. La riduzione avviene nel frontend Ladder Diagram (LD), aggiungendo un hook leggero (circa 40 righe) che impone i limiti di input e imposta la larghezza di parola dell'architettura.

Contributi Chiave

Metodo di Verifica Fedele all'Hardware: Un approccio formale che trasferisce la disciplina del target-model della programmazione C embedded a sicurezza critica (stabilita da strumenti come Frama-C e Astrée) al dominio PLC. A differenza di tali strumenti, questo metodo deriva automaticamente i limiti di input dallo schema di indirizzamento standard IEC 61131-3 e dai descrittori della scheda.
Istanza ESBMC-Arduino: Un'implementazione concreta per target di classe Arduino, che trae i parametri HAL dai core ufficiali di Arduino. Supporta sia target a 16 bit (AVR) che a 32 bit (ARM).
Valutazione Empirica: Una valutazione rigorosa su 123 programmi reali e un corpus controllato di 20 pattern.

Risultati

Eliminazione dei Falsi Allarmi: Sul corpus di 123 programmi, l'attivazione dell'annotatore HAL ha eliminato tutti i 54 falsi allarmi (riducendo il conteggio degli insicuri da 54 a 0) preservando ogni prova di robustezza (32 programmi sono rimasti provati sicuri).
Rilevamento di Difetti Reali: Un corpus controllato ha dimostrato che il metodo rileva difetti genuini dipendenti dalla larghezza (ad esempio, overflow nella scalatura da ADC a percentuale su schede a 16 bit) con testimoni fisicamente realizzabili.
Validazione Cross-Tool: Il fenomeno degli "allarmi fantasma" è stato riprodotto utilizzando strumenti indipendenti (CBMC e Frama-C/EVA) su specchi C della logica, confermando che il problema è inerente alla verifica naive consapevole della larghezza senza modellazione dell'input, non specifico per ESBMC.
Prestazioni: L'overhead dell'annotatore HAL è trascurabile; i tempi di verifica rimangono sotto il secondo per programma.
Limitazioni: Sebbene i falsi allarmi siano stati eliminati, 91 programmi nel corpus reale hanno restituito verdetti "unknown" a causa dell'incompletezza della $k$ -induzione su blocchi funzionali con stato interno. Questa è una limitazione della capacità del prover per chiudere i passi induttivi, non del modello di input.

Significatività
Il documento sostiene che il valore primario di questo lavoro non risiede nel numero di bug scoperti (che sono rari nei specifici corpora pubblici analizzati, dominati da logica Booleana e di timer), ma nel ripristino della correttezza (soundness). Gli autori dimostrano che la verifica naive consapevole della larghezza è inutilizzabile per l'assurance a causa di un tasso di falsi allarmi del 44% che annega i risultati genuini. Derivando automaticamente gli intervalli di input realizzabili dall'hardware, il metodo converte uno strumento inaffidabile in uno che emette solo report realizzabili, consentendo agli ingegneri di fidarsi dei risultati di verifica per i PLC open-hardware. L'approccio è presentato come una strategia di adozione realistica e a basso costo (un descrittore a 4 campi e un hook di 40 righe) che si integra con l'infrastruttura di verifica matura invece di richiedere una proposta da zero.

Sintesi Tecnica: ESBMC-ARDUINO

Articoli simili