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

 非标自动化产线中的PLC控制程序频繁迭代，且常由不同工程师编写，极易引入逻辑冲突、死锁、边界超限等软件漏洞，严重威胁生产安全。本文提出一套结合静态分析与模型检验的混合式漏洞挖掘与形式化验证方法。首先，将梯形图（LD）或结构化文本（ST）代码转化为中间表示（IR），并构建控制流图（CFG）与数据依赖图（DDG）；然后，基于时序逻辑（LTL）定义典型漏洞模式（如互斥违背、看门狗超时）；最后，采用符号模型检验工具（如nuXmv）对系统状态空间进行形式化验证。在某非标电池模组装配线中，该方法成功挖掘出3处隐藏极深的逻辑死锁和5个数值溢出漏洞，验证时间较穷举测试降低90%。

1. 引言

PLC（可编程逻辑控制器）是非标自动化产线的核心控制器件。非标项目“短平快”的特点使得PLC程序往往缺乏系统的代码审查和全面的测试，遗留大量逻辑漏洞。这些漏洞在运行时可能表现为：传感器故障处理不完善导致机器人意外运动、状态机死锁造成产线停机、定时器竞争引发多缸同时动作等。传统基于经验的功能测试覆盖率极低。形式化验证方法通过数学证明程序是否满足既定规约，能实现完备验证。但直接对PLC原生代码进行形式化面临状态空间爆炸、PLC特有语义难以表达等问题。本文旨在构建一个面向PLC程序的自动化漏洞挖掘与验证工具链。

2. PLC漏洞模式分析与建模

2.1 典型漏洞分类
基于对20条非标产线故障报告的分析，归纳出四类高频漏洞：

• 逻辑冲突：同一线圈在不同网络中被重复赋值（双线圈问题）。
• 时序死锁：两个互锁的状态机同时等待对方释放资源。
• 边界异常：计数器的设定值大于预设最大阈值，导致溢出。
• 实时性违例：扫描周期内无法完成预期逻辑，导致看门狗复位。

2.2 中间表示转换
将西门子、三菱等主流PLC的梯形图/ST代码统一转换为一种名为“PLC-IR”的中间表示。PLC-IR保留了PLC的周期扫描语义、边沿触发、定时器/计数器函数块特性。转换规则包括：将梯形图的触点和线圈转换为布尔逻辑门网络；将结构化文本转换为静态单赋值（SSA）形式。

3. 混合式漏洞挖掘方法

3.1 静态模式匹配
预定义漏洞特征库。例如，双线圈漏洞的检测：遍历所有输出线圈，若同一变量在代码中被SET/RESET或赋值超过一次，且中间没有互斥条件，则报告。对于定时器，检查其预设值PT是否为变量，且是否有越界保护。该阶段可快速筛选出80%的明显错误。

3.2 基于符号模型检验的形式化验证
对于静态分析无法判定（如涉及两个功能块交互）的代码段，构建符号模型。PLC程序的状态 $S=(I,Q,M,T)$S=(I,Q,M,T)，其中 $I$I 为输入映像区，$Q$Q 为输出，$M$M 为内部存储器，$T$T 为定时器剩余时间。转换规则：

• 每个网络（Network）被视为一个同步转移关系 ${\text{Trans}}_i:S\to S^{\mathrm{\prime }}$Transi​:S→S′。
• 整个扫描周期是一个复合转移 $\text{Scan}={\text{Trans}}_N\circ \cdots \circ {\text{Trans}}_1$Scan=TransN​∘⋯∘Trans1​。

使用线性时序逻辑（LTL）描述期望属性：

• 安全属性：$\mathrm{\square }(Pump\mathrm{\_}On\to \mathrm{\neg }Valve\mathrm{\_}Open)$□(Pump_On→¬Valve_Open)（泵启动时阀门不得打开）。
• 活性属性：$\diamond (Start\mathrm{\_}Pressed\to \diamond Conveyor\mathrm{\_}Run)$⋄(Start_Pressed→⋄Conveyor_Run)（按下启动后最终传送带运行）。

将PLC-IR模型和LTL属性输入支持硬件描述语言Verilog的模型检验器（如nuXmv）。采用有界模型检验（BMC）和k-归纳法，在有限深度内反例查找。

4. 实验验证与案例分析

4.1 被测对象
选取一条真实的非标电池模组装配线PLC程序，代码量约1500行ST语言，控制14个轴、30个气缸和200余个传感器信号。

4.2 漏洞挖掘结果

• 静态分析发现：6处双线圈隐患、3个定时器未初始化。
• 形式化验证发现深层次漏洞：一处安全光幕触发后的急停恢复逻辑存在死锁。验证器发现一旦急停发生在特定工位（第7步），状态机将进入“等待复位”且无法跳出的状态，违反了活性属性 $\diamond (E\mathrm{\_}Stop\mathrm{\_}Released\to \diamond System\mathrm{\_}OK)$⋄(E_Stop_Released→⋄System_OK)。追溯代码发现是复位信号与使能信号的依赖顺序错误。
• 数值漏洞：验证器通过攻击边界条件，发现当某计数器累计到32768时（超出16位整数上限），会使后续一段位置计算溢出变为负数，导致机器人朝错误方向移动。传统测试从未触达此边界。

4.3 性能对比
与传统随机测试和人工走查相比，形式化验证虽然初期建模耗时2小时，但验证过程覆盖了全部理论状态空间（约2^200种），而随机测试覆盖率不足10%。验证单个属性平均耗时45秒，整体完成挖掘耗时3.5小时，比穷举仿真测试（估计需300小时）效率提升近百倍。

5. 结论与展望

本文提出的混合方法兼具静态分析的高效性与形式化验证的完备性，在非标PLC程序漏洞挖掘中展现出显著优势。但该方法对复杂算法（如PID、浮点运算）的支持尚弱。未来工作：1) 结合抽象解释技术，降低模型检验状态空间；2) 开发自动化反例诊断与修复建议生成功能，降低工程人员使用门槛。