使用ESBMC-PLC+检测IEC 61131-3 PLC程序中的梯形逻辑炸弹：一种带有触发综合的形式化验证方法

# 使用ESBMC-PLC+检测IEC 61131-3 PLC程序中的梯形逻辑炸弹：一种带触发综合的形式化验证方法
来源：https://arxiv.org/html/2607.08417
Pierre Dantas 计算机科学系 曼彻斯特大学 曼彻斯特，英国 pierre\.dantas@manchester\.ac\.uk ORCID: 0000\-0001\-6390\-9340 & Lucas Cordeiro 11footnotemark:1 计算机科学系 曼彻斯特大学 曼彻斯特，英国 lucas\.cordeiro@manchester\.ac\.uk ORCID: 0000\-0002\-6235\-4272 & Waldir Junior 11footnotemark:1 电气工程系 亚马逊联邦大学（UFAM） 马瑙斯，AM，巴西 waldirjr@ufam\.edu\.br ORCID: 0000\-0003\-3095\-0042 作者对本研究贡献相同。通讯作者：pierre\.dantas@manchester\.ac\.uk。

（2026年7月）

###### 摘要

梯形逻辑炸弹（LLB）是一种插入到可编程逻辑控制器（PLC）程序中的恶意控制逻辑，它处于潜伏状态，直到某个*触发条件*激活一个*有效载荷*，从而操纵执行器、伪造传感器读数或拒绝操作员控制。我们对真实的LLB数据集进行了一项结构性观察：恶意逻辑隐藏在*功能块体内部*，而现有的梯形图（LD）验证器会将其从中级表示（IR）中丢弃，使得证明者无法区分恶意程序和良性程序。我们提出了ESBMC-LLB方法，该方法*使用ESBMC-PLC+*（一个现有的IEC 61131-3验证器）作为其验证引擎，并增加了一个建模层，将功能块内部的逻辑暴露给证明者，并将LLB检测重新定义为形式化验证：*扫描看门狗*将拒绝控制（非终止）型有效载荷暴露为可检查的安全违规，而*输出接线*将执行器伪造型有效载荷暴露为可检查的安全违规。k-归纳法可以生成跨所有扫描周期的*炸弹缺失无界证明*，而边界模型检查器则返回一个反例，该反例*就是引爆触发条件*——这是签名检测、异常检测和控制流图（CFG）分类检测器无法提供的两个保证。在公开的Iacobelli等人\[12 (https://arxiv.org/html/2607.08417#bib.bib12)\]数据集上，ESBMC-LLB检测到了所有30个炸弹并恢复了每一个触发条件；因为它基于程序语义而非语法模式进行推理，所以它还能检测到可逃避CFG分类启发式方法的自适应触发条件（计算型、不透明算术型、多扫描型）。我们进一步报告了语义模型检查器在最新真实模拟基准（PLC-Defuser的SWaT语料库）上的首次评估：我们的模拟建模扩展使整个语料库首次可解析，并且在存档的v1.0.0版本上，检测到149/150个炸弹（99%），零误报，并恢复了每个触发条件；在一个增加了*非线性*非终止型炸弹的较新语料库版本上，检测率下降到49%，因为可满足性模理论（SMT）后端超时。我们得出结论，语义模型检查和CFG分类是*互补的*——前者提供无界炸弹缺失证明和自适应触发鲁棒性，处理布尔/整数和线性模拟逻辑，后者在非线性模拟非终止方面领先——我们精确描述了各自胜出的场景。

*关键词* 梯形逻辑炸弹·PLC·IEC 61131-3·工业控制系统安全·ESBMC·BMC·k-归纳法·SMT·触发综合·形式化验证·LD·PLCopen XML

## 1 引言

可编程逻辑控制器（PLC）运行安全关键型工业控制系统（ICS）的控制逻辑：水处理、电力、化工和制造工厂。能够通过工程工作站、被篡改的项目文件或供应链获得对PLC写入权限的攻击者，可以插入一个*梯形逻辑炸弹（LLB）*：一段控制逻辑片段，在*触发条件*激活之前保持潜伏，然后执行一个*有效载荷*来破坏物理过程\[10 (https://arxiv.org/html/2607.08417#bib.bib26)\]。与IT恶意软件不同，LLB是普通的梯形图或结构化文本（ST）代码；它能够通过调试测试和短时间仿真，因为其触发条件被设计为在正常运行期间保持非活跃状态。Govil等人\[10 (https://arxiv.org/html/2607.08417#bib.bib26)\]引入了这一概念以及LLB触发条件和有效载荷的分类；后续工作提出了基于形式化验证的检测架构\[12 (https://arxiv.org/html/2607.08417#bib.bib12)\]和工业部署\[3 (https://arxiv.org/html/2607.08417#bib.bib14)\]。

本文使这种联系具体而完整。我们基于ESBMC-PLC+\[6 (https://arxiv.org/html/2607.08417#bib.bib20)\]构建——这是一个统一的IEC 61131-3验证器，通过单一的高效基于SMT的上下文边界模型检查器（ESBMC）后端（带有k-归纳法）接受文本形式的梯形图（LD）、图形化的LD和ST/结构化控制语言（SCL）——并观察到，为*安全性*验证构建的机制，在无需后端修改的情况下，就是一个*LLB检测器*。我们将由此产生的方法称为ESBMC-LLB：

- • LLB有效载荷必然将程序驱动到违反安全或完整性属性的状态。因此，检测炸弹归结为检查该属性。
- • k-归纳法将该属性作为*无界*证明进行处理：SAFE判定表明*没有*可达的扫描周期状态引爆所建模类别的炸弹——这是签名扫描仪无法提供的保证。
- • 当存在炸弹时，边界模型检查（BMC）返回一个反例跟踪。该跟踪*就是触发条件*：准备和引爆有效载荷所需的确切输入/周期序列。因此，检测自动产生触发综合。

一种隐蔽且被广泛引用的LLB类别是计数器/定时器定时炸弹（“经过N个周期后引爆”）\[10 (https://arxiv.org/html/2607.08417#bib.bib26)\]：这是一种整数状态模式，基于二元决策图（BDD）的无界证明器已知会遭受状态空间爆炸，而ESBMC-LLB所基于的可满足性模理论（SMT）位向量引擎则符号化地处理宽整数状态\[6 (https://arxiv.org/html/2607.08417#bib.bib20)\]。我们利用这一特性来恢复计数器/定时器的引爆触发条件；我们在此*不*重新测量后端性能，并且我们预先指出（§6.8 (https://arxiv.org/html/2607.08417#S6.SS8)），这一优势*并不*扩展到*非线性*整数状态（例如，更新i := i\*i的非终止循环），这对SMT后端来说仍然困难，而这正是控制流图（CFG）分类检测器保持优势的地方。

### 1.1 贡献

1. 1. 一个将功能块（FB）内部的炸弹暴露给ESBMC-PLC+的建模层（§6.2 (https://arxiv.org/html/2607.08417#S6.SS2)）：我们展示参考数据集中的LLB隐藏在*LD功能块体内部*，现有的LD验证器会将其从中级表示（IR）中丢弃；我们的建模层翻译每个功能块体并将其馈送给ESBMC-PLC+（其验证引擎保持不变使用），使炸弹逻辑对证明者可达。
2. 2. 两种带触发综合的检测机制：*扫描看门狗*，将触发条件门控的非终止（拒绝控制）型炸弹转化为可达的安全违规；*输出接线*，将值/执行器伪造型炸弹转化为安全属性违规；在两者中，BMC反例恢复引爆触发条件，而k-归纳法可无界地证明炸弹缺失。
3. 3. 自适应对手鲁棒性（§6.6 (https://arxiv.org/html/2607.08417#S6.SS6)）：因为ESBMC-LLB评估程序语义而非语法模式，它可以检测到为逃避基于CFG的触发分类而设计的触发条件（计算型、不透明算术型、多扫描型）——这类检测器在结构上会遗漏此类触发。
4. 4. 一个诚实的评估，包括实际正面交锋和负面结果（§6 (https://arxiv.org/html/2607.08417#S6)）：在公开的Iacobelli等人\[12 (https://arxiv.org/html/2607.08417#bib.bib12)\]数据集上检测率达到30/30，在一个310程序的布尔/整数语料库上达到100%召回率且零误报（中位数70ms），并且没有回归（13/13）。我们进一步展示了语义模型检查器在PLC-Defuser的真实SWaT基准上的首次运行：我们的模拟建模扩展使语料库可解析，在存档的v1.0.0版本上，检测到149/150个炸弹（99%）且零误报，而在一个增加了*非线性*非终止型炸弹的较新语料库版本上，检测率下降到49%，因为SMT后端超时。
5. 5. 对语义与CFG权衡的描述（§7 (https://arxiv.org/html/2607.08417#S7)）：语义模型检查在自适应触发条件和布尔/整数逻辑的无界保证方面领先；CFG分类在非线性模拟非终止方面领先。两者是*互补的*，而非竞争关系。

## 2 背景与相关工作

### 2.1 PLC扫描周期与ESBMC-PLC+

PLC执行周期性的*扫描*：采样输入，执行控制程序一次，写入输出，然后重复执行，并配有看门狗定时器，若执行时间超过固定预算则中止该周期。ESBMC-PLC+\[6 (https://arxiv.org/html/2607.08417#bib.bib20)\]将此扫描周期编码为一个while(true)循环，其中输入被非确定性重新采样（*开放世界*传感器模型），输出和定时器/计数器状态为持久变量，YAML指定的安全/完整性属性被注入为__ESBMC_assert()语句。由此产生的模型由ESBMC\[9 (https://arxiv.org/html/2607.08417#bib.bib17),18 (https://arxiv.org/html/2607.08417#bib.bib18)\]后端处理：k-归纳法证明一个属性对于*所有*扫描计数都成立（无界保证）。相比之下，增量式BMC展开循环以找到违反跟踪（图1 (https://arxiv.org/html/2607.08417#S2.F1)）。我们不加修改地使用此编码，只在其前面添加一个建模层（§6.2 (https://arxiv.org/html/2607.08417#S6.SS2)）。

采样输入 → 执行程序一次 → 写入输出 → 看门狗：若执行超过预算则中止 → PLC扫描周期
while(true) { in = nondet(); /* 输出、定时器/ */ /* 计数器持久 */ step(); __ESBMC_assert(p); } → ESBMC-PLC+编码 → 开放世界传感器模型·持久状态·YAML属性 → ESBMC后端 → SAFE：对所有扫描计数成立（k-归纳法） → VIOLATION++跟踪（增量式BMC）

图1: PLC扫描周期及其ESBMC-PLC+编码。PLC重复采样输入，执行程序一次，写入输出，并配有看门狗中止超预算的执行。ESBMC-PLC+将该周期编码为一个while(true)循环：输入被非确定性重新采样（开放世界传感器模型），输出和定时器/计数器状态在迭代间持久，YAML安全/完整性属性成为__ESBMC_assert()语句。k-归纳法证明一个属性对所有扫描计数成立（无界），而增量式BMC展开循环以返回违反跟踪。我们的建模层（§6.2 (https://arxiv.org/html/2607.08417#S6.SS2)）位于此编码之前，该编码被保持不变使用。

### 2.2 梯形逻辑炸弹

Govil等人\[10 (https://arxiv.org/html/2607.08417#bib.bib26)\]将LLB定义为由其*触发条件*（激活条件）和其*有效载荷*（恶意效果）组成，并展示了操纵执行器、伪造传感器/HMI值和拒绝控制的炸弹。我们在§5 (https://arxiv.org/html/2607.08417#S5)中复现此分类。这一威胁并非假设：Stuxnet蠕虫通过注入在检查期间保持潜伏、仅在精确过程状态下方引爆的恶意PLC逻辑来破坏离心机控制器\[13 (https://arxiv.org/html/2607.08417#bib.bib1)\]；LLB将这种潜伏模式推广到任意触发条件/有效载荷对，其潜伏性正是能够击败调试测试和短期仿真的关键。

### 2.3 相关检测工作

表1 (https://arxiv.org/html/2607.08417#S2.T1)按方法对先前工作进行分组，并定位ESBMC-LLB：在布尔/整数LD上，它能够匹敌专用检测器，同时独特地添加了无界炸弹缺失证明和自适应触发鲁棒性；而在非线性模拟控制方面，PLC-Defuser领先——因此两者是互补的。

表1：ESBMC-LLB在PLC恶意/不安全逻辑检测器中的定位。“声音存在性证明” = 认证*所有*扫描周期内不存在（所建模类别的）炸弹；“触发综合” = 恢复具体的引爆条件；“整数触发器规模” = 在整数比较/计数器触发器上的表现；“自适应鲁棒性” = 检测为逃避语法/CFG分类而设计的触发条件。†\dagger ESBMC-LLB处理线性/平坦整数算术（SMT-BV）；PLC-Defuser的CFG分类在结构上定位触发条件，无需SMT即可处理非线性算术。
对PLC代码进行形式化验证/模型检查是直接可比的研究方向。Iacobelli等人\[12 (https://arxiv.org/html/2607.08417#bib.bib12)\]（ICPS’24）是最接近的竞争者：一个用于LLB检测的形式化验证架构，在包含30个合法和30个恶意PLCopen LD程序的公开数据集上进行评估，其中炸弹使用EQ/LT/LE/GE/GT比较块作为触发条件，线圈/赋值作为有效载荷。我们使用*他们的*数据集进行我们的正面交锋（§6.4 (https://arxiv.org/html/2607.08417#S6.SS4)）。*可信安全验证器（TSV）*\[17 (https://arxiv.org/html/2607.08417#bib.bib2)\]对PLC字节码针对安全属性进行线路内模型检查，但是有界的且非无规范。*SymPLC*\[11 (https://arxiv.org/html/2607.08417#bib.bib3)\]通过相同的MATIEC\[21 (https://arxiv.org/html/2607.08417#bib.bib22)\]到C路径对IEC 61131-3应用符号执行，但使用KLEE——提供覆盖驱动的测试生成，而非无界证明。*PLCverif*\[22 (https://arxiv.org/html/2607.08417#bib.bib7)\]基于用于ANSI-C程序的边界模型检查（CBMC）或BDD有界（nuXmv\[5 (https://arxiv.org/html/2607.08417#bib.bib19)\]）且为西门子特定。这些工具都无法提供炸弹*缺失*的无界证明、自动触发综合或整数触发器上的鲁棒性——这正是ESBMC-LLB领先的三个维度。

通用的IEC 61131-3验证：一个广泛的研究方向形式化IEC 61131-3语义并验证PLC代码的功能正确性和安全性，而非恶意逻辑：可执行的ST语义\[24 (https://arxiv.org/html/2607.08417#bib.bib10),14 (https://arxiv.org/html/2607.08417#bib.bib11),15 (https://arxiv.org/html/2607.08417#bib.bib16)\]，带归纳代码综合的形式化验证\[25 (https://arxiv.org/html/2607.08417#bib.bib6)\]，协作验证\[23 (https://arxiv.org/html/2607.08417#bib.bib8)\]，梯形逻辑故障影响分析\[7 (https://arxiv.org/html/2607.08417#bib.bib9)\]，耦合FRET和PLCverif的基于监视器的验证\[8 (https://arxiv.org/html/2607.08417#bib.bib13)\]，以及在安全关键工厂上的验证即服务部署\[16 (https://arxiv.org/html/2607.08417#bib.bib15)\]。这些工具验证一个*预期行为的规范*；没有一个将LLB检测重新定义为带触发综合的无界炸弹缺失证明，而这是ESBMC-LLB所填补的空白。

不变量挖掘/安全审查：*VetPLC*\[26 (https://arxiv.org/html/2607.08417#bib.bib4)\]（CCS’19）挖掘时间不变量以审查PLC代码，而*SAIN*\[1 (https://arxiv.org/html/2607.08417#bib.bib5)\]（USENIX’24）细化状态感知不变量；两者针对不同的问题（发现规范/异常），是互补的而非直接的竞争者。

运行时证明和过程级机器学习（ML）异常检测（例如在SWaT测试床上）在另一层（网络/传感器轨迹，而非控制逻辑）上运行，并在执行时检测攻击，而非离线认证程序。我们定性地将其定位为与ESBMC-LLB互补，但不声称与之直接竞争。