Google DeepMind、AlphaProof CodeでSignalプロトコルの機械語を形式検証したと発表

Google DeepMindのPushmeet Kohliは、チームがSignalメッセージングプロトコルの基盤となる機械語について、主要なセキュリティ特性を証明したと発表した。DeepMindによると、広く利用されているプロトコルの本番コードが、これほど深いレベルまで、いかなる手法によっても形式検証されたのは初めてだという。これらはDeepMind自身の主張だ。

この取り組みでは、DeepMindがGemini CarbonなどのLLM上で動作する、形式検証のための新しいエージェント型フレームワークと説明するAlphaProof Codeを使用した。DeepMindによると、検証はデバイス上で実行されるコードにまで及び、約1カ月を要した。同様の取り組みには、チームで合計数十年分の作業が必要になる場合もあるという。また、パートナーとしてSignalチームの協力を挙げている。

DeepMindは、他の人々が活用できるよう、形式仕様と検証成果物をオープンソース化している。11月10日朝の時点で、この投稿はXで1,297件の「いいね」を獲得していた。