From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware
本文介绍了 Encore!，一种裸机延续传递风格（Continuation Passing Style）虚拟机，它通过将核心结构化为一个可证明的状态转移函数，使得在微控制器上执行经过 Rocq 提取的经过形式化验证的 Scheme 固件成为可能，从而促进了具有机器检查保证的 AI 辅助安全关键型代码的生成。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正在为一家银行建造一个高安全性保险库。你需要编写指令（即“固件”），告诉保险库如何开启、关闭以及如何计数金钱。在过去，编写这些指令非常困难，而检查其中是否存在错误更是难上加难。现在，有了人工智能，我们可以瞬间生成这些指令，但这产生了一个新的问题：我们如何信任一段由我们无法完全理解的机器所编写的代码？
这篇名为《从 Rocq 到金属》（From Rocq to Metal）的论文提出了一个解决方案：一种用在数学上被证明是完美的方法来编写这些关键指令，然后将该证明直接运行在如硬件钱包等设备中发现的微小、廉价的计算机芯片上。
以下是他们使用简单类比对该方法的拆解：
1. 问题所在：“重型宇航服” vs. “微型机器人”
大多数现代允许进行“数学证明”的编程语言（如 Lean 4 或标准 OCaml）就像是重型、高科技的宇航服。它们对于宇航员（强大的计算机）来说非常出色，但对于必须装进信用卡大小设备中的微型机器人（微控制器芯片）来说，它们太重、太臃肿了。
- 问题在于： 如果你试图把那套沉重的宇航服穿在微型机器人身上，机器人会被重量压垮。它没有足够的电池（RAM）或存储空间（Flash）来运行那套“证明”软件。
- 旧方法： 开发人员过去会在重型宇航服中编写代码，然后手动将其翻译成一种简单的语言给机器人使用。但这种翻译就像是在玩“传声筒”游戏——错误会悄悄溜进来，数学证明也会因此丢失。
2. 解决方案：“安可！”（轻量级翻译器）
作者构建了一个名为 Encore! 的新工具。你可以将 Encore! 想象成一个专门的、超轻量级的翻译器，它可以装进微型机器人的口袋里。
- 它是如何工作的： 你在一种严谨的、数学化的语言 Rocq 中编写你的指令（这就像是用完美的逻辑来写一份食谱）。
- 神奇之处： Encore! 不会将食谱翻译成混乱且易错的语言，而是直接将其转换为机器人可以执行的微小、高效的“字节码”。
- 结果： 机器人运行的是与经过数学证明的完全相同的逻辑。不存在“传声筒”游戏；证明过程一直延续到了底层硬件（Metal）。
3. 架构：“状态机”
为了实现这一点，作者重新组织了软件的构建方式。他们将设备视为一个棋盘游戏。
- 游戏板（状态）： 当前的情况（例如，“等待用户按下按钮”）。
- 掷骰子（事件）： 发生了某事（例如，“用户按下了按钮”）。
- 规则书（经过验证的核心）： 一个纯粹的、数学化的函数，它规定：“如果棋盘处于状态 A 且你掷出了 6，那么棋盘必须移动到状态 B。”
- 裁判（未经验证的部分）： 系统中与物理世界进行交互的部分（读取按钮、点亮屏幕）。这些部分是唯一没有经过数学证明的部分，但它们被保持得非常小巧且简单。
为什么这很重要： “规则书”（业务逻辑）可以根据你的需求变得多么庞大和复杂，它始终是 100% 可证明的。而“裁判”则保持精简且恒定。这意味着你可以添加复杂的特性，而不会增加验证的难度。
4. 与 AI 的联系：“证明即代码审查”
该论文提出了一个未来前景：AI 帮助编写代码，但 AI 不仅仅是在靠猜。
- 旧方法： AI 编写代码；人类阅读代码以检查漏洞。这种方式无法规模化。
- 新方法： AI 编写数学证明（定理）。计算机检查该证明。如果证明有效，代码就被保证是正确的。
- 类比： 与其要求人类阅读一本 100 页的小说来寻找一个错别字，不如要求计算机检查一个 10 页的数学方程。如果方程是正确的，那么故事就是正确的。
5. 结果：它确实奏效了
团队在真实硬件（一个使用非常微小、安全芯片的 Ledger Flex 硬件钱包）上测试了这一点。
- 他们提取了一个交易签名应用（那种用于转移资金的应用）。
- 他们在 Rocq 中编写了核心逻辑并证明了其正确性。
- 他们使用 Encore! 将其运行在芯片上。
- 结果： 该芯片成功运行了经过数学验证的代码，解析了数据，并签署了交易，同时完全符合设备的微小内存限制。
总结
这篇论文证明了你不需要在高安全性（数学证明）和微型硬件（微控制器）之间做选择。通过构建一个定制的、轻量级的引擎（Encore!）并将软件结构化为简单的棋盘游戏，他们展示了“完美”的代码可以在“不完美”的芯片上运行。这为经过自动验证的 AI 生成代码打开了大门，使硬件钱包等关键设备变得更加安全和可靠。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。