⚡ electrical engineering

ESBMC-Arduino: Closing the Deployment Gap for Formal Verification of Open-Hardware PLCs

本文介绍了 ESBMC-Arduino，这是一个硬件忠实（hardware-faithful）的验证框架，它通过集成声明式硬件抽象层和可靠的输入范围建模，为开源硬件 PLC 弥合了部署差距，旨在消除由理想化整数假设引起的虚假报警，同时检测在运行于资源受限微控制器上的 IEC 61131-3 程序中存在的真实宽度相关缺陷。

原作者： Pierre Dantas, Lucas Cordeiro, Waldir Junior

发布于 2026-07-10

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Pierre Dantas, Lucas Cordeiro, Waldir Junior

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在建造一个管理水箱的机器人。你使用一种叫做 IEC 61131-3 的特殊语言来编写指令，这就像是工业机器的通用食谱。多年来，工程师们一直使用“超级机器人”模拟器来检查这些食谱是否安全。这些模拟器就像是拥有无限数字思维的巫师；它们假设机器人可以脑中持有任何数字，从负无穷到正无穷，并且传感器可以报告任何可以想象到的数值。

但这里有一个转折：你实际建造的机器人并不是巫师。它是一个微小的、廉价的微控制器（比如 Arduino），它生活在现实世界中。这个小芯片有一个非常具体且有限的大脑。它只能持有最高为 32,767 的数字。如果计算结果超过这个值，数字并不会仅仅是变大，而是会崩溃、折回底部，变成一个负数。这就像汽车的里程表，从 999,999 滚回到 000,000。

巨大的脱节
论文称之为“部署差距”（deployment gap）。这是“巫师的梦想世界”与“机器人局促的现实”之间的差异。

作者发现，当工程师使用旧有的“巫师”模拟器来检查他们的代码是否安全时，他们得到了大量的虚假警报。在他们测试的 123 个真实程序中，旧的模拟器尖叫着“危险！”达 54 次（虚假报警率为 44%）。但当他们仔细观察时，意识到这些“危险”是不可能发生的。模拟器想象出的传感器读数像是 -32,764。在现实世界中，连接到这个机器人的传感器只能读取 0 到 1,023 之间的数字（因为这是一个 10 位传感器）。-32,764 这个值就像温度计读数为“零下 32,764 度”一样——这根本不可能发生。

论文指出，依赖这些旧的模拟器就像是一个保安因为看到了幽灵而大喊“入侵者！”。保安在技术上关于幽灵的描述是“正确”的，但由于幽灵并不存在，这种正确是毫无用处的。作者明确排除了这样一种观点，即你可以只检查数学错误而不同时检查传感器实际能看到什么。他们表明，这样做会使验证在实践中变得“不健全”（unsound，即不可靠）。

神奇的修复方法：HAL 描述符
为了解决这个问题，作者构建了一个名为 ESBMC-Arduino 的新工具。把这个工具想象成一个“现实检查”过滤器。

在巫师模拟器查看代码之前，这个新工具会在每个传感器上附带一个微小的、自动生成的便签。它会说：“嘿，记住，这个传感器只能给出 0 到 1,023 之间的数字。”它还会提醒模拟器：“并且记住，机器人的大脑只能持有最高为 32,767 的数字。”

当模拟器带着这些规则运行时，奇迹发生了：

54 个虚假警报瞬间消失了。-32,764 这个幽灵消失了，因为模拟器现在知道这个数字是不可能的。
那 32 个已经被证明安全的程序依然保持安全。
最重要的是，该工具并没有漏掉任何真正的漏洞。它发现旧的模拟器隐藏了一种特定的真实危险：当一个传感器读数被乘以一个大数字（例如将原始传感器值转换为百分比）时，数学计算可能会导致这个微小机器人大脑的溢出。

真实的危险（以及它有多罕见）
论文发现，虽然“幽灵警报”很常见，但由于这种差距导致的真实漏洞在他们测试的公开代码中其实相当罕见。他们只在特定的场景中发现了真正的缺陷，即在 16 位板卡上，当传感器读数被乘以一个大的常数（如 100）时。

例如，如果传感器读取 898（这是一个正常的、真实的数值），而代码将其乘以 100，结果是 89,800。这对于 16 位机器人大脑（最大值为 32,767）来说太大了。数字发生了回绕，变成了一个负数，导致机器人误以为水箱是空的，而实际上水箱正在溢出。新工具捕捉到了这个精确的情景，并向工程师提供了导致崩溃的传感器读数的真实物理示例。

论文并未声称的内容
作者非常诚实地说明了他们没有做的事情。他们并没有证明现在所有的程序都是安全的。在 123 个程序中，有 91 个最终得到了“未知”的判定。这并不是因为工具坏了，而是因为要证明这些特定程序安全的数学逻辑对目前的引擎来说太难了，无法完成。该工具成功地消除了噪声（虚假警报）并保留了信号（真实的证明），但它还无法解决最难的谜题。

此外，他们也没有在浮点数（如 3.14 之类的十进制数）或复杂的物理模拟上进行测试。他们专注于整数（integers）和布尔逻辑（Boolean logic，即开/关开关）。

底线
这篇论文证明了，要验证开源硬件 PLC（如学校和小型工厂中使用的 PLC），你不能仅仅检查数学，你必须检查硬件的极限。通过自动添加一个告诉模拟器传感器实际能力的“现实检查”，他们将一个嘈杂、不可靠的工具变成了一个值得信赖的工具。他们并没有发现一百万个新漏洞，但他们阻止了工具“狼来了”式的乱叫，使得工程师能够重新信任安全检查。

技术摘要：ESBMC-ARDUINO

问题：开源硬件 PLC 中的部署差距
开源可编程逻辑控制器（PLC），例如运行在 Arduino OPTA、CONTROLLINO 和 Industrial Shields M-Duino 上的 OpenPLC，使低成本微控制器级设备也能使用 IEC 61131-3 编程。这些平台越来越多地被用于教育、小规模自动化以及作为工业控制系统（ICS）安全研究的运行时基座。然而，在现有的开源验证器（如 ESBMC-PLC、PLCverif）所使用的抽象模型与实际硬件执行环境之间，存在着一个关键的“部署差距”。

目前的验证器基于抽象的扫描周期模型运行，该模型假设整数是理想化且无界的，且输入不受约束。相比之下，实际部署的制品运行在资源受限的微控制器单元（MCU）上，具有特定的机器字长（例如，8 位 AVR 板上的 16 位 int）和有限分辨率的模数转换器（ADC，通常为 10 位，产生范围在 $[0, 1023]$ 的值）。这种差异导致了两种失效模式：

漏报缺陷： 程序在抽象模型中可能被证明是安全的，但由于整数溢出（例如，在 16 位板上的缩放计算发生回绕）而在设备上是不安全的。
幻象报警（误报）： 更严重的是，仅考虑字宽但忽略硬件输入边界的朴素宽度感知验证，会探索物理 ADC 无法产生的传感器值（例如负值或超过 1023 的值）。这会导致伪造的溢出报告。对 123 个真实第三方程序的语料库进行评估显示，朴素的 16 位溢出检查产生了 44% 的误报率（54/123），同时未发现任何真实的缺陷。

方法论：硬件忠实验证
本文提出了一种通过构建能忠实表示目标硬件的“部署模型”（ $M_{dev}$ ）来弥合这一差距的方法。其核心是 硬件抽象层（HAL）描述符 和一个**可靠的降级（lowering）**过程。

HAL 描述符 ( $H$ )： 一个捕获以下信息的声明式元组 $H = \langle w, b_{adc}, b_{pwm}, \mu \rangle$ $H = ⟨ w, b_{a d c}, b_{pw m}, μ ⟩$ ：
- $w$ ：机器字长（例如，AVR 为 16 位，ARM 为 32 位）。
- $b_{adc}$ 和 $b_{pwm}$ ：模数转换器（ADC）和脉冲宽度调制（PWM）输出的分辨率。
- $\mu$ ：通过自动从 IEC 61131-3 直接寻址方案中导出的 I/O 绑定映射（例如，%IW 地址映射到具有特定 ADC 范围的模拟输入）。
可靠降级： 该方法通过以下方式将 PLC 程序 ( $P$ $P$ ) 转换为部署模型 ( $M_{dev}(P, H)$ $M_{d e v} (P, H)$ )：
- 在目标字宽 $w$ 下解释算术运算（精确重现补码回绕）。
- 在采样输入后立即注入 assume 约束，将变量限制在其硬件可实现的范围内（例如， $0 \leq adc \leq 1023$ ）。
- 使用非确定性输出对非线性功能块（如 PID）进行过度近似，以保持可处理性。
验证引擎： 该方法无需修改即可复用 ESBMC 后端（基于 SMT 的有界模型检测和 $k$ -归纳法）。降级过程发生在梯形图（LD）前端，通过添加一个轻量级钩子（约 40 行代码）来强制执行输入边界并设置架构字宽。

核心贡献

硬件忠实验证方法： 一种正式的方法，将安全关键型嵌入式 C 的目标模型纪律（由 Frama-C 和 Astrée 等工具建立）转移到 PLC 领域。与这些工具不同，该方法自动从硬件描述符中推导输入边界，而不是需要手动输入契约。
ESBMC-Arduino 实例化： 一个针对 Arduino 类目标的具体实现，其 HAL 参数源自官方 Arduino 核心。它支持 16 位（AVR）和 32 位（ARM）目标。
实证评估： 对 123 个真实程序和 20 个受控模式语料库进行了严格评估。

结果

消除误报： 在 123 个程序的语料库中，启用 HAL 注解器消除了所有 54 个误报（将不安全数量从 54 降至 0），同时保留了每一个鲁棒性证明（32 个程序仍被证明是安全的）。
检测真实缺陷： 一个受控语料库表明，该方法能够检测出真实的、依赖于宽度的缺陷（例如，在 16 位板上 ADC 到百分比缩放过程中的溢出），并能提供物理可实现的证据。
跨工具验证： 使用独立的工具（在 C 镜像逻辑上使用 CBMC 和 Frama-C/EVA）重现了“幻象报警”现象，证实了该问题是由于缺乏输入建模的朴素宽度感知验证本身导致的，而非 ESBMC 特有的问题。
性能： HAL 注解器的开销微乎其微；验证时间保持在每程序一秒以内。
局限性： 虽然误报被消除了，但 91 个程序因带有内部状态的功能块在 $k$ -归纳法上的不完备性而返回了“未知（unknown）”结论。这是由于证明器在完成归纳步骤方面的能力限制，而非输入模型的限制。

意义
本文认为，这项工作的核心价值不在于发现了多少 Bug（在所调查的特定公开语料库中，Bug 较少，主要由布尔逻辑和定时器逻辑组成），而在于恢复了可靠性（soundness）。作者证明了，由于 44% 的误报率会淹没真实的发现，朴素的宽度感知验证在保障方面是不可用的。通过自动推导硬件可实现的输入范围，该方法将一个不可靠的工具转化为了一个仅发布可实现报告的工具，从而使工程师能够信任开源硬件 PLC 的验证结果。该方法被呈现为一种现实且低成本的采用策略（一个 4 字段描述符和 40 行钩子代码），它集成到了成熟的验证基础设施中，而非提出了一个全新的方案。

技术摘要：ESBMC-ARDUINO

类似论文