Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis
本文提出了 ESBMC-LLB，这是一个形式化验证框架，它通过扩展 ESBMC-PLC+ 来检测 IEC 61131-3 PLC 程序中的梯形图逻辑炸弹（Ladder Logic Bombs），通过揭示隐藏的功能块逻辑并合成触发条件，在现有方法失效的公开数据集上实现了近乎完美的检测率以及对自适应触发器的鲁棒性。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，可编程逻辑控制器（PLC）就像是工厂的大脑，它不断运行着一个循环：观察传感器、做出决策、移动机器，然后在一瞬间重新开始。现在，想象一个狡猾的黑客在那个大脑里藏进了一个“逻辑炸弹”。这个炸弹就像一条沉睡的巨龙：在工厂正常运行时，它毫无反应；但只要某个隐藏的条件发生（比如计数器达到了某个特定的数值），它就会苏醒并制造混乱——要么让机器冻结，要么伪造传感器读数，或者在不该打开时强行打开阀门。
长期以来，用于检查这些“工厂大脑”的工具一直存在一个盲点。它们会检查主代码，但会忽略“功能块”（Function Blocks）——这些是主代码内部的小型子程序或微型程序。这篇论文解释说，那些“沉睡的巨龙”（炸弹）就躲在这些被忽略的功能块之中。因为旧工具会将这些功能块从它们的视野中剔除，导致恶意代码和安全代码在检查者眼中看起来完全一样。这就像是在人群中寻找间谍时，只通过观察人们的脸来判断，却忽略了间谍正躲在一件检查者根本不会去看的外套里。
大修方案：打开外套
作者 Pierre Dantas、Lucas Cordeiro 和 Waldir Junior 构建了一种名为 ESBMC-LLB 的新方法。他们的核心技巧简单而强大：他们让检查者能够看穿功能块内部。他们添加了一个“转换层”，将这些功能块中隐藏的代码进行“平铺化”处理，使其变得清晰可见。
一旦代码变得可见，他们便使用两个聪明的招式来捕捉炸弹：
- 秒表（扫描监视器/Scan-Watchdog）： 如果炸弹试图通过让程序进入死循环来冻结机器，检查者就会像一名拿着秒表的严格裁判。它会说：“你有 100 步的时间来完成这项任务。如果你超时，你就出局了！”如果炸弹试图无限循环，检查者会立即将其抓获。
- 接线测试仪（输出布线/Output Wiring）： 如果炸弹试图伪造传感器数据或强行移动机器，检查者会将隐藏代码的导线连接到主系统。如果隐藏代码试图发送一个“谎言”（例如在不该打开时告诉阀门打开），检查者会发现它违反了安全规则。
神奇的结果：找到“秘密代码”
最酷的部分在于：当检查者发现炸弹时，它不仅仅是简单地报错“错误！”。它实际上会吐出确切的触发条件。这就像是检查者在说：“我找到了这条巨龙，而且这是唤醒它的秘密密码：‘如果计数器达到 12’。”这被称为“触发合成”（Trigger Synthesis）。
效果如何？
团队在几组数据上测试了他们的方法，结果令人印象深刻，但也存在重要的局限性：
- 公开测试： 在一个包含 60 个程序（30 个安全程序，30 个带有炸弹的程序）的著名数据集上，他们的方法找到了全部 30 个炸弹。它抓住了每一个炸弹并找到了各自的秘密触发器。它还证明了那 29 个安全程序确实是安全的。其中一个安全程序由于过于复杂，检查器无法百分之百确定（它返回的是“我不知道”而非“安全”），但它并没有产生误判。
- “聪明”黑客测试： 他们尝试通过将触发器隐藏在数学谜题中（例如使用复杂的计算而非简单的数字）来欺骗系统。那些仅仅寻找模式的旧工具错过了这些技巧，但 ESBMC-LLB 理解了数学的含义，并抓住了全部 5 个这类复杂的变体。
- 大规模测试： 他们生成了 310 个程序（155 个安全，155 个带炸弹）来测试速度。系统抓住了 100% 的炸弹，平均耗时仅为 70 毫秒（这比眨眼还要快！）。
- 现实世界水厂测试： 他们在真实的工业水处理厂模拟环境（SWaT 数据集）中进行了测试。
- 在包含简单数学触发器的旧版本数据上，他们找到了 149 个中的 150 个 炸弹（99%），且零误报。
- 局限性： 当他们测试一个包含极其复杂的非线性数学（例如将一个数字反复自乘）的新版本时，系统卡住了。数学运算太难，导致检查器无法及时求解，检测率降至 49%。论文对此说明得非常清楚：他们的方法对于标准逻辑和简单数学非常出色，但在面对复杂的非线性数学时会遇到瓶颈。在这些特定情况下，另一种类型的工具（称为 CFG-triage 检测器）仍然更胜一筹。
他们并未声称的内容
作者们非常诚实地说明了他们的工具不能做什么。他们明确指出，如果一个炸弹被设计为快速完成任务（不产生死循环），并且没有违反他们告知检查者的任何特定安全规则，那么该工具可能会漏掉它。它并不是一个能发现所有潜在坏事的“万能魔棒”，它专门寻找那些会导致系统冻结或违反预设安全规则的行为。
总结
这篇论文表明，通过“打开外套”去观察功能块内部，并使用一个理解代码含义的智能检查器，我们可以捕捉到那些曾经隐藏在眼皮底下的隐蔽工业炸弹。它不仅能找到炸弹，还能准确告知我们如何触发它们（以便我们阻止它），并证明系统的其余部分是安全的——除非数学运算变得过于疯狂，在这种情况下，我们需要另一种类型的侦探。作者将此呈现为一种强大的新工具，它与现有方法协同工作，而非取代一切。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。