ESBMC-PLC+形式化检测PLC梯级逻辑炸弹并合成触发器
速览
梯级逻辑炸弹(LLB)是隐藏在PLC程序功能块体内的恶意控制逻辑，现有梯级图验证器会忽略功能块逻辑。ESBMC-LLB通过建模层暴露功能块逻辑，将炸弹检测转化为形式化验证问题：扫描看门狗暴露非终止载荷，输出接线暴露篡改载荷。在Iacobelli 2024数据集上检测全部30个炸弹并恢复每个触发器；在PLC-Defuser的SWaT语料库上实现99%检测率，零误报。该方法与CFG-triage互补，提供无界证明和自适应触发器鲁棒性。
AI 深度解读
背景
可编程逻辑控制器（PLC）是工业自动化系统的核心组件，按照 IEC 61131-3 标准编写的梯形逻辑程序负责控制物理过程（如阀门、电机、传感器）。近年来，针对 PLC 的恶意攻击日益增多，其中一类特殊的威胁称为“梯形逻辑炸弹”（Ladder Logic Bomb, LLB）：一段看似正常的控制逻辑在特定触发条件满足时释放破坏性载荷，例如操纵执行器、篡改传感器读数或拒绝操作员控制。
现有梯形图验证工具在构建中间表示（IR）时会丢弃功能块（function block）内部的逻辑细节，而真实恶意逻辑恰恰常藏匿在功能块内部——这导致炸弹在形式化验证过程中“隐形”。传统基于签名、异常检测或控制流图（CFG）分类的方法虽然能识别部分已知模式，但无法提供无界的正确性证明，也无法恢复出触发条件（trigger）。为此，本文提出了 ESBMC-LLB，一种将炸弹检测转化为形式验证问题的新方法。
核心内容
ESBMC-LLB 以 ESBMC-PLC+ 作为验证引擎，并在其基础上增加了一个建模层。该建模层能完整暴露功能块的内部逻辑，使得原本被隐藏的恶意代码进入验证范围。具体而言，验证通过两种安全机制来捕获不同类型的炸弹：
- 扫描看门狗（scan-watchdog）：用于暴露非终止（non-termination）载荷。如果某个函数块中的循环或递归导致扫描超时，看门狗将其标记为违反安全属性。
- 输出接线（output wiring）：用于暴露执行器伪造（actuator-forgery）载荷。当输出被恶意改写为与输入计算不一致的值时，视为安全违例。
验证过程采用双轨策略：
- k-induction：通过归纳证明，保证在所有扫描周期中都不存在炸弹（无界证明）。
- 有界模型检查（BMC）：返回反例，该反例即是炸弹的精准触发条件（trigger）。这一能力是签名检测、异常检测和 CFG 分类方法所不具备的。
实验在两个公开数据集上进行：
- Iacobelli 2024 数据集：包含 30 个炸弹。ESBMC-LLB 检测出全部 30 个，并恢复了每个炸弹的触发器，包括自适应触发器（自适应触发器通过计算、不透明算术、多扫描等方式逃避 CFG 分类）。
- PLC-Defuser 的 SWaT 语料库：本文首次在此语料库上进行语义模型检查评估。团队开发了模拟扩展，使全部语料库可被解析。在 v1.0.0 版本中，检测出 149/150 个炸弹（99%），零误报，并恢复每个触发器；但在后续版本中，由于引入了非线性非终止炸弹，SMT 求解器超时，检测率降至 49%。
结论指出，语义模型检查（semantic model checking）与 CFG 分类是互补的：前者提供无界证明、自适应触发器的鲁棒性，并处理布尔/整数及线性模拟逻辑；后者在非线性模拟非终止场景中更具优势。文章明确了各自擅长的领域。
关键要点
- 现有梯形图验证工具因丢弃功能块内部逻辑，使得隐藏其中的 LLB 完全不可见；ESBMC-LLB 通过建模层暴露这一盲区。
- 将炸弹检测形式化为两个安全属性：扫描看门狗捕获非终止载荷，输出接线捕获执行器伪造载荷；k-induction 给出无界证明，BMC 返回精确触发器。
- 在 Iacobelli 2024 数据集上实现 100% 检测率（30/30），且恢复所有触发条件，包括自适应触发器（计算型、不透明算术型、多扫描型）。
- 在 SWaT 语料库 v1.0.0 上达到 99% 检测率（149/150）、零误报，并完全恢复触发器；这是该语料库首次经过语义模型检查评估。
- 面对非线性非终止炸弹时，SMT 求解器超时导致检测率下降至 49%，说明当前方法在处理非线性模拟逻辑时存在局限。
- 语义模型检查与 CFG 分类是互补工具：前者适合布尔/整数及线性模拟场景，后者在非线性模拟非终止场景中表现更优。
意义与影响
ESBMC-LLB 首次证明了形式验证方法能够有效检测藏匿在 PLC 功能块内部的恶意逻辑，并恢复其触发条件。这一进展弥补了现有轻型检测方法（如签名匹配、异常分析、CFG 分类）缺乏无界证明和触发器恢复能力的根本缺陷。对于工业控制系统安全领域，该工作提供了：
- 一种可证明安全的验证框架，能够给出“所有扫描周期内无炸弹”的保证。
- 一种自动化生成触发器的方法，可辅助安全分析师理解攻击的行为路径。
- 对自适应触发器的鲁棒性，使得攻击者无法通过简单的触发条件变化绕过检测。
同时，实验揭示了非线性模拟逻辑下 SMT 的求解瓶颈，为未来研究方向指明了道路——例如结合符号执行与数值求解器处理非线性约束，或设计混合验证策略，在 CFG 分类与模型检查间动态切换。总体而言，ESBMC-LLB 为 IEC 61131-3 PLC 程序的安全性分析开辟了基于语义模型检查的新途径，并有望成为工业安全验证工具链的重要组成部分。