ESBMC-Arduino: 形式検証の展開ギャップを埋める

ESBMC-Arduino: Closing the Deployment Gap for Formal Verification

OpenPLC、Arduino OPTA、CONTROLLINO、Industrial Shields M-DuinoなどのオープンハードウェアPLCは、IEC 61131-3を低コストのマイコンに導入し、産業用制御システムのセキュリティ研究に利用されています。しかし、既存の検証ツールは理想化された抽象モデルに依存しており、実際のハードウェアの制約（16ビット幅、ADCの分解能など）を無視していました。その結果、123の実プログラムで44%の誤警報が発生し、真の欠陥を検出できないことが判明。本研究では、ハードウェアの仕様を記述する抽象化レイヤー（HAL）と、それをESBMCに統合するArduinoToolを提案し、誤警報をすべて排除しつつ、幅依存の欠陥を検出可能にしました。