AlphaProof 代码与信号：检查机器代码安全证明和信任假设

本视频涵盖的内容

• AI 代理生成候选证明；Lean 的内核检查它们是否确立了人类批准的形式化声明。
• 验证目标是特定的编译后的 libsignal CLI 工具，具有受信任的语义和密码约定。
• 证明编译后的二进制文件，可将 Rust 编译器从该二进制文件所述属性的信任基础中移除。
• 研究人员报告了两次孤立的重新引入了以前修复的违反其符号安全定理的错误。
• 比较器根据受保护的批准规范检查定理和每个相关定义；修正案通过单独的审查流程。

翻译的文字记录

译自英文原版旁白。可用音频和字幕由 YouTube 控制。

谁来检查 AI 安全证明？

0:00 AI 安全审计听起来仍然像信任聊天机器人。 Google 新的 Signal 结果附带了数学证明，一个单独的内核 进行检查。在此视频中，Google 证明了什么？ 他们如何阻止代理改变目标？ 这是有用的答案。 模型编写候选证明，Lean 根据关于选定编译代码的 人类批准的声明检查证明。 人类仍然拥有声明和假设。

0:21 您可以检查结果，而无需相信模型的胜利演讲。 单独的检查可以发现悄悄改变问题的情况。 我们将深入研究定义。 今天是 11 月 10 日星期二，这里是 The Daily Diff。 AlphaProof Code 是 Google 的框架，用于在人类指导下编写软件规范并使用 AI 代理生成经过检查的证明。 本研究的目标是 libsignal，即实现 Signal 消息传递的 Rust 库， 在一个特定的命令行程序中。

0:45 Google 今天宣布了这项工作。 其论文称五名研究人员工作了四个星期。 代理编写证明，而人类大部分精力都花在 规范上。需求已经找到了一种方法，变得更加昂贵 的会议。规范说明了程序必须做什么，

声明如何成为证明目标？

0:59 攻击者控制什么，以及论证需要哪些假设。 审阅者会问它是否抓住了人们关心的安全性。 一个对弱问题的完美答案并不能解决这个问题。 该团队建立在早期对 Signal 握手及其消息密钥的 研究基础上。形式化分析已经研究了这些设计。 Google 的声明将其安全论证与未经修改的生产 库的编译实现联系起来，在该实现中，设计必须经受住与 实际代码的接触。Signal 的首席技术官 Ehren Kret，

1:27 描述了超越早期验证较小范围的扩展。 实现细节包括乱序 消息和用于 延迟消息的存档会话。真实软件保留了你优雅图表中丢弃的收据。 研究人员使用标准编译器将未经修改的 Rust 库编译成

为什么证明编译后的二进制文件？

1:41 Arm 64 位 Linux 可执行文件。 他们的定理使用形式化指令模型描述该二进制文件， 跨越了源代码和优化机器代码之间的鸿沟。 破坏所述属性的编译器错误将使定理为假。 因此，编译器脱离了该二进制文件的信任基础。 您仍然信任指令模型和 Lean 的检查器。 信任边界已移动，并且它有一个地址。 大约 650 万行已验证的证明建立在约 26000 行

2:06 受信任的规范和指令语义行上。 这些是工件计数。 将它们视为智力分数就像根据开发人员 node 模块文件夹的大小来排名。 他们的 node 模块文件夹。

哪些安全属性在实现差距中幸存下来？

2:16 论证涵盖消息机密性和认证， 在所述模型下具有前向保密性和妥协后安全性。 后两者描述了密钥失窃损害的限制以及新鲜密钥交换后的恢复。 每次保证都对攻击者和会话有条件。 密码原语位于受信任的契约之后。 该证明假设这些例程按规范运行，并依赖于密码 安全假设。一个证明使密码学理想化；另一个则推理 攻击者成功概率。

2:42 两者都对其涵盖的场景有限制。 询问是哪个构建、哪个属性以及哪个假设。 此结果涉及研究人员的命令行工具。 群组消息是未来的工作，计算模型排除了 多设备状态。声称每个 Signal 安装都无 bug 超出了 定理的范围。研究人员将两个以前修复的 Signal bug 重新引入

规范能拒绝损坏的代码吗？

3:02 隔离副本并进行编译。 检查的证明表明这些二进制文件违反了符号安全定理。 这测试了规范是否能拒绝真实的损坏实现。 您的绿色对勾需要红色测试。 Google 发布了带有检查说明的规范和证明。 存储库称，干净构建需要数小时和大量内存。 在笔记本电脑上阅读公告要容易得多。 硬件模型和受信任的合约仍需审查。

3:26 我没有为这一集重建巨大的工件。 我们正在报告已发布的结果及其边界。 外部人员有途径检查它，这对我来说比另一次 AI 胜利巡演更重要。现在是陷阱。

正确的证明能回答错误的问题吗？

3:36 Lean 可以接受一个几乎没有要求的正确证明。 不可能的假设可以使定理变得空洞。 更改标题定理下埋藏的定义会削弱 目标。该论文设计了针对此的检查。 守门人保留一份经批准的规范，证明代理无法 写入。它们可以通过单独的修正程序提出更正。 安全削弱被升级为潜在错误。 证明者声明的成功在这里没有权威。

4:00 人类裁决对信任假设的更改， 直接或通过其策略，并在每次活动后审查修正案。 专家判断仍需负责。 代理可以请求不同的任务。 它不能给自己打及格分。

什么能捕捉到不断变化的目标？

4:13 这是承诺的检查。 Lean 的比较器将定理及其所依赖的每个定义与 受保护的批准副本进行比较。 它还检查允许的公理并在新的内核中重放证明。 因此，悄悄削弱辅助定义会改变被 比较的事物。已接受的证明必须确立批准的目标。 这仍然让人类负责选择一个强大的目标和诚实的 假设。对于您自己的 AI 工作流程，请将接受标准置于

4:37 工作人员的编辑权限之外，并单独审查拟议的更改。 Google 的结果使这种分离具体化。 证明作者完成工作； 检查边界决定它是否有效。 如果您更愿意阅读而不是听我说，那么每天早上，diff 都会免费发送到您的收件箱， 网址是 daily diff dot dev，链接在下方。 所以今天的结论是 SHIP IT。

我会采用这种证明工作流程吗？

4:54 我会采用这种已验证的证明工作流程，因为批准的声明与生成答案的 代理是分开的。 我会将范围和假设附在每个结果上。 订阅，点击铃铛，并在评论中告诉我你是否会 盖上不同的印章。这就是今天的 diff。 我是 Axrisi 的 Niko。 负责任地合并。

来源

1. AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeepingSwarat Chaudhuri and colleagues / Google DeepMind and Google
2. Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO responsePushmeet Kohli and Swarat Chaudhuri / Google DeepMind
3. Code-verification repository — initial commit, public artifacts and checking instructionsGoogle DeepMind / GitHub
4. The PQXDH Key Agreement Protocol — older official specification and prior-analysis contextEhren Kret and Rolfe Schmidt / Signal
5. The Double Ratchet Algorithm — Triple Ratchet sectionTrevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
6. Google DeepMind leadership — Demis Hassabis's relevant lab identityGoogle DeepMind
7. Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsementChristopher P. Michel / Cmichel67 / Wikimedia Commons
8. Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlikeCreative Commons
9. Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claimImgflip / user-uploaded meme template
10. Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claimBoomerang Official / GIPHY / Tom and Jerry
11. Boomerang GIF source link — uploader-provided provenanceBoomerang
12. AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claimsHacker News
13. Code-verification licence — Apache 2.0 for Google code, third-party licences retainedGoogle / GitHub