非标自动化产线中PLC程序漏洞挖掘与形式化验证方法

非标自动化产线的PLC程序通常由不同工程师编写，缺乏统一规范，易含逻辑漏洞，如互锁冲突、状态机死锁及时序违规。本文提出一种结合模型检测与符号执行的PLC漏洞挖掘框架。首先将梯形图/ST代码转换为时间自动机模型，定义安全性、活性及互斥性属性；然后使用UPPAAL进行形式化验证，对违反属性生成反例路径；同时引入符号执行引擎检测数据流异常。该方法在三个非标产线案例中发现了7处真实漏洞（包括2处联锁失效），比传统测试效率提升5倍。

1. 引言

可编程逻辑控制器（PLC）是非标自动化产线的核心控制单元。由于非标产线的程序常为一次性开发、缺乏充足的仿真测试，且逻辑复杂（包含大量手动/自动切换、互锁、计时器配合），极易引入隐蔽漏洞。传统测试方法依赖人工构造测试用例，覆盖不全，尤其难以发现并发状态下的竞态条件或长时间序列中的死锁。

形式化方法能够穷尽搜索状态空间，已被证明在安全关键系统中有效，但在PLC领域应用受限于：PLC程序的多任务扫描周期特性、I/O物理时序约束以及工程师对形式化语言的不熟悉。本文提出一种面向非标产线特点的PLC漏洞挖掘流程，将梯形图自动转化为形式模型，并给出适合工业实践的反例可视化方法。

2. PLC程序建模与属性定义

2.1 从梯形图到时间自动机

梯形图本质上由一系列串联/并联的触点与线圈组成，对应布尔逻辑和定时器/计数器。本文定义转换规则：

• 每个梯级（rung）转换为一个布尔赋值语句。
• 定时器（TON/TOF）转换为带有连续时间变量的自动机，时钟速率与PLC扫描周期同步。
• 多任务组织块（OB）间通过共享全局变量交互，对应自动机间的通道同步。

以UPPAAL的输入语言描述时间自动机网络，每个自动机状态表示一组变量的赋值集合。

2.2 待验证属性

针对非标产线，定义以下典型属性：

• 安全性：“两个互锁的气缸不得同时伸出”，即 G¬(CylA_ext∧CylB_ext)G¬(CylA​_ext∧CylB​_ext)。
• 活性：“请求进料后10秒内必须启动输送带”，即 G(Request→F≤10sConveyor_on)G(Request→F≤10s​Conveyor_on)。
• 无死锁：从任意可达状态，至少有一个迁移可执行。
• 无界变量：计时器或计数器不会溢出。

这些属性以CTL或TCTL公式表达。

3. 漏洞挖掘方法

3.1 模型检测核心流程

1. 解析PLC源代码（支持西门子SCL、三菱梯形图）。
2. 构建抽象语法树，去除与逻辑无关的注释和I/O别名。
3. 生成时间自动机模型，限定状态空间爆炸：采用抽象解释技术将连续模拟量离散为区间。
4. 调用UPPAAL验证引擎。若属性违反，输出反例路径（一系列状态迁移序列）。
5. 将反例路径映射回原PLC程序中的梯级和变量，并突出显示。

3.2 符号执行补充验证

模型检测受限于状态空间，对于包含复杂算术运算的PLC程序（如PID调节、配方计算），采用符号执行引擎（基于KLEE修改PLC语义）生成路径约束，求解是否存在除以零、有符号溢出等数值漏洞。

3.3 漏洞分类与严重性评级

按漏洞影响分级：

• 致命：可导致机械碰撞或人身伤害。
• 严重：产线停机或产品报废。
• 一般：性能下降或短暂异常。

4. 案例研究

4.1 案例一：非标压装产线互锁漏洞

程序意图：压装头与换料滑台互锁。形式化验证发现属性 G¬(Press_down∧Slide_in)G¬(Press_down∧Slide_in) 被违反。反例显示当急停复位后一个扫描周期内两者同时动作为真。根因是急停后复位信号在两个梯级中同时置位。修复后避免了一次潜在设备损坏。

4.2 案例二：涂胶机状态机死锁

涂胶程序包含8个状态（待机、清洗、定量、涂胶等）。模型检测显示从“清洗超时自动返回”状态无法迁移至“待机”，因为超时标志被错误清零。死锁漏洞导致设备在清洗后永久等待。传统测试运行6小时未触发，形式化验证10分钟内发现。

4.3 案例三：多任务竞态条件

两个中断OB同时修改同一计数器，符号执行发现存在路径使计数器值非预期，导致胶量不足。共挖掘7个真实漏洞，传统单元测试仅发现2个。

5. 方法有效性评估

6. 结论

本文提出的基于时间自动机和符号执行的PLC漏洞挖掘方法，能够系统性地检测非标产线PLC程序中的逻辑与时序漏洞。工业案例验证了其高效性和实用性。未来将开发集成于TIA Portal的插件，降低工程师使用门槛。