Google DeepMind 已數學驗證 Signal 加密協定

來自 Google DeepMind 的研究人員成功運用 AI 對 Signal 加密協定的關鍵組件進行了形式化驗證。這項為期四週的專案證明了利用自動化系統來檢查複雜軟體數學正確性的可行性。

在研究過程中，專家們採用了自動定理證明方法，以確認加密邏輯中不存在漏洞。傳統上，形式化驗證需要高素質工程師投入大量時間，但 AI 代理的整合顯著加快了程式碼分析的進程。這證實了自動化驗證作為確保關鍵系統安全工具的潛力。

實驗結果顯示，AI 有能力處理過去被認為僅限於數學專家才能完成的任務。使用此類方法，開發人員可以在惡意攻擊者利用之前，發現加密協定中隱藏的錯誤。未來，這種方法可能成為設計安全通訊軟體及其他以資料完整性為優先之服務的標準。