AlphaProof Code 和 Signal：已驗證機器碼安全證明和受信任假設

本影片涵蓋的內容

• 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 的檢查器。 信任邊界已移動，並且它有一個地址。 大約六百五十萬行的已驗證證明建立在大約兩萬六千

2:06 行受信任的規範和指令語義行上。 這些是構件計數。 將它們視為智力分數，就像根據開發人員的 節點模塊文件夾大小來排名他們一樣。

哪些安全屬性在實施差距中倖存下來？

2:16 這些論證涵蓋訊息機密性和身份驗證， 在規定的模型下具有前向保密性和洩露後安全。 後兩者描述了被盜密鑰損害的限制以及在新的 交換後恢復。每個保證都有關於攻擊者和會話的條件。 密碼學原語位於受信任的契約背後。 該證明假設這些例程按規範運行，並依賴於密碼學 安全假設。一個證明將密碼學理想化；另一個則推理關於 攻擊者成功概率。

2:42 兩者都對它們涵蓋的場景有限制。 詢問哪個版本、哪個屬性以及哪些假設。 此結果涉及研究人員的命令列工具。 群組訊息是未來的研究工作，計算模型排除了 多裝置狀態。聲稱每個 Signal 安裝都無錯誤，這超出了 定理的範圍。研究人員將兩個先前已修復的 Signal 錯誤重新引入

規範可以拒絕損壞的代碼嗎？

3:02 獨立副本並進行編譯。 已驗證的證明表明這些二進位文件違反了符號安全定理。 這測試了規範是否可以拒絕實際損壞的實現。 你的綠色勾選標記需要紅色測試。 Google 發布了規範和證明，並附有檢查說明。 儲存庫稱，乾淨的構建需要數小時和大量記憶體。 在筆記本電腦上閱讀公告要容易得多。 硬件模型和受信任的契約仍需審查。

3:26 我沒有為這一集重建這個巨大的構件。 我們正在報告已發布的結果及其邊界。 外界有途徑檢查它，這對我來說比另一個 AI 勝利圈更重要。現在是陷阱。

正確的證明會回答錯誤的問題嗎？

3:36 Lean 可以接受一個幾乎沒有要求聲明的正確證明。 不可能的假設可以使定理變得空洞。 更改標題定理下面埋藏的定義會削弱 目標。該論文設計了對此的檢查。 守門人保留了一份未公開的已批准規範，證明代理無法 寫入。他們可以通過單獨的修訂程序提出更正。 安全弱化會作為潛在錯誤升級。 證明者的成功聲明在這裡沒有權威。

4:00 人類裁定對受信任假設的更改， 直接或通過其策略，並在每次活動後審查修訂。 專家判斷仍然承擔責任。 代理可以請求不同的分配。 它不能給自己一個及格分數。

什麼會捕捉不斷變化的目標？

4:13 這是承諾的檢查。 Lean 的比較器將定理及其所依賴的每個定義與 受保護的已批准副本進行比較。 它還檢查允許的公理並在新的核心中重放證明。 因此，悄悄削弱一個輔助定義會改變被 比較的內容。一個被接受的證明必須建立已批准的目標。 這仍然讓人類負責選擇一個強大的目標和誠實的 假設。對於你自己的 AI 工作流程，將驗收標準保留在

4:37 工作者的編輯權限之外，並單獨審查提議的更改。 Google 的結果使這種分離具體化。 證明撰寫者完成工作； 檢查邊界決定它是否有效。 如果你寧願閱讀這份報告而不是聽我說，那麼每日差異會 每天早上免費發送到你的收件箱，網址是 thedailydiff.dev，連結在下方。 所以今天的判決是 SHIP IT。

我會發布這個證明工作流程嗎？

4:54 我會發布這個已驗證的證明工作流程，因為已批准的聲明與 產生答案的代理保持分離。 我會將範圍和假設附加到每個結果中。 訂閱、點擊鈴鐺，並在評論中告訴我你是否會蓋上 不同的印章。這就是今天的差異。 我是 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