Signalの暗号をDeepMindのAIが検証、新たな欠陥なし

Signalの暗号検証で何が分かったのか

Signalの古いバージョンを同じツールで調べたところ、セキュリティ上の欠陥が見つかり、形式検証できないことも示された。ただ、これらは既知で、とうに修正済みの問題だという。

Signalのプロトコルはオープンソースで、WhatsApp、Facebook Messenger、Google Messagesも採用している。Telegramと違い、Signalではエンドツーエンド暗号化がメッセージと音声通話で初期設定から有効だ。

手作業の検証は時間がかかる。証明したい性質を記述し、数式に直し、証明を組み立てる必要があるためだ。AIエージェントはこの期間を大きく縮められる可能性がある。SignalのCTO、Ehren Kret氏は、AI絡みの脅威が増すなか、コードのプライバシー保証への信頼がさらに高まるとコメントした。

今回の検証の限界は

DeepMindによると、分析範囲は限定的で、Signalのモバイルアプリ全体は対象外だ。Signal Foundationによる過去の形式検証も土台にしている。AIで大規模かつ現実的なコストで自動化できるかも未解決だ。

DeepMindは作成した仕様と証明を、他の研究のために公開する。商用の検証サービスを出す計画があるかどうかは不明だ。研究者のSwarat Chaudhuri氏は、世界中のソフトウェアに広げるにはまだ距離があると述べ、AIが目標も証明も作る「雰囲気だけの世界」は望まないとして、人間の確認を残す考えを示した。