ESBMC-Arduino: Formale Verifikation für Open-Hardware-SPSen ohne Fehlalarme

ESBMC-Arduino: Closing the Deployment Gap for Formal Verification

OpenPLC, Arduino OPTA, CONTROLLINO und Industrial Shields M-Duino bringen IEC 61131-3 auf kostengünstige Mikrocontroller, die in realen Automatisierungs- und ICS-Sicherheitsforschungen eingesetzt werden. Bisherige Open-Source-Verifier wie ESBMC-PLC prüfen Sicherheitseigenschaften über ein abstraktes Scan-Cycle-Modell mit idealisierten unbegrenzten ganzen Zahlen. Die Hardware läuft jedoch auf ressourcenbeschränkten MCUs mit 16-Bit-Wörtern und liest Sensoren über einen ADC mit endlicher Auflösung. Diese Diskrepanz macht naive breitenabhängige Verifikation unsound: Bei 123 realen Programmen erzeugt die Prüfung auf 16-Bit-Überlauf ohne Hardware-Eingabemodell 44% Fehlalarme (54/123) und findet keine echten Defekte, da sie Sensorwerte erkundet, die kein ADC erzeugen kann. Die Autoren präsentieren hardwaretreue Verifikation für IEC 61131-3 auf Open Hardware: eine deklarative Hardware-Abstraktionsschicht (HAL) mit Deskriptoren für Breite, ADC/PWM-Auflösung und I/O-Bindung sowie eine sounde Senkung, die Arithmetik auf Zielbreite interpretiert und Eingaben auf hardware-realistische Bereiche beschränkt. Die Instanziierung für Arduino (ArduinoTool) leitet HAL-Parameter aus offiziellen Cores ab und setzt das Eingabebereichsmodell im ESBMC-Ladder-Diagramm-Frontend um. Auf dem Korpus eliminiert der HAL-Annotator alle 54 Fehlalarme, während Robustheitsbeweise erhalten bleiben; ein kontrollierter Korpus zeigt die seltenen breitenabhängigen Defekte, die mit realisierbaren Witnesses erkannt werden.