Google DeepMind 的一項分析已對 Signal 協議的安全性完成「形式驗證」。該協議長期被視為端到端加密通訊的黃金標準，Edward Snowden 是知名支持者；除了 Signal 應用，WhatsApp 和 Google Messages 亦採用同一協議，這項工作被形容為「里程碑式發展」。
重點文章
形式驗證以數學證明安全
「形式驗證」是指以數學證明或證偽某密碼演算法或協議在所有情況下均滿足其安全聲明。它保證協議不會在任何情況下失效，標準遠高於傳統測試方法；後者旨在尋找漏洞，卻無法保證沒有其他漏洞存在。
代理式 AI 驗證運算需求高
以代理式 AI 執行形式驗證，對密碼學和 AI 而言均屬重大突破。然而，這種做法運算需求極高，Google 向 Wired 表示，目前尚未清楚更廣泛應用是否實際可行。DeepMind 研究科學家 Swarat Chaudhuri 向 WIRED 表示，團隊對這項結果非常振奮，但要將此擴展至全球所有軟件仍有漫長距離，而他們希望做到；研究人員強調，這只是更大過程中的一個里程碑。這項分析耗時四星期，所需資源規模尚未披露，因此不應預期其他大批協議會在一夜之間獲得驗證。儘管如此，這仍是一項重大成果。
驗證針對協議而非應用
需注意的是，這次驗證針對協議本身，而非整個 Signal 應用。Google 亦得以在過去未使用 AI 完成的形式驗證工作基礎上推進。不過，當以含有已知漏洞的舊版 Signal 進行測試時，分析識別出這些漏洞並標記為未通過形式驗證，令人鼓舞。
