DeepMind 的 AlphaProof Code 驗證 Signal 的加密核心

Google DeepMind 發表 AlphaProof Code，這是一套能以數學方式證明軟體符合其安全規範的 AI 系統，並用它驗證了運行在 Signal 使用者裝置上的密碼學核心程式碼，耗時四週，而這類工作通常需要數年。在專家定義形式化安全需求後，建構於 Gemini Carbon 上的 AI 代理以 Lean 證明語言撰寫了超過六百萬行，並標記約百分之一的程式碼庫供人工審查，立即抓出兩個刻意植入的錯誤。Signal 技術長 Ehren Kret 表示，隨著 AI 威脅日益增長，這種方法強化了對資料隱私的信任，而 DeepMind 計畫透過 CodeMender 等系統，將此方法擴展至電網與醫療裝置。

根據 Ars Technica 報導，Google DeepMind 完成了一項為期四週的專案，以數學方法驗證了 Signal 的關鍵部分。這項工作暗示 AI 可能讓形式化驗證變得更加實用，不過報導並未提供進一步的技術細節。