DeepMind以AI代理驗證Signal加密實作安全性，數學證明擴及機器碼層級

作者李建興11/12 08:00全文約 836 字

文章摘要

iThome · 文章頁摘要

Google DeepMind運用AI代理對Signal核心加密程式進行形式化驗證，證明編譯後機器碼符合指定安全要求，研究歷時4周，產出約650萬行Lean證明

Google DeepMind公布AI代理形式化驗證（Formal Verification）框架AlphaProof Code，利用AI代理驗證Signal加密通訊協定的核心程式庫libsignal，將安全性證明延伸到編譯後的機器碼。...