# DeepMind、Signalの暗号コードをAIで検証

> AlphaProof Codeは4週間で、コンパイル済みのSignalコードにおける重要なセキュリティ特性を検証した。ただし、証明の対象は特定の保証に限られ、Signalの全機能を網羅するものではない。

Oossa · 2026-11-11 · https://oossa.com/ja/deepmind-used-ai-to-verify-signal-s-cryptographic-code

Google DeepMindは、Signalメッセージングプロトコルのリファレンス実装であるlibsignalについて、AlphaProof Codeを使い、重要なセキュリティ特性を数学的に検証したと発表した。作業にかかった期間は4週間。DeepMindによると、同様の検証には従来、専門家チームが何年も要していた。

このシステムでは、人間の研究者とAIエージェントが連携した。研究者とAIがSignalのセキュリティ目標を数学的な仕様に落とし込み、人間がそれを確認。その後、Gemini Carbonを搭載したエージェントが約650万行のLean証明コードを生成した。Leanは、数学的証明が規則に従っているかをチェッカーで検証できるプログラミング言語だ。エージェントはコードベースの約1％を、人間による確認が必要な箇所として提示した。

## 証明の対象は？

研究者らは、libsignalの耐量子計算機ハンドシェイクPQXDHとTriple Ratchetについて、コンパイル後の機械語を検証した。前方秘匿性、認証、端末が侵害された後の保護など、特定の性質を証明した。研究論文によると、コードは変更されていないRustから標準的なコンパイラーで生成され、その後、AArch64の機械語として検証された。

これは、抽象的な設計が安全だと証明するだけのものではない。定められたセキュリティ保証を、コンパイル済みコードに結び付けている。DeepMindは、広く使われている暗号プロトコルの実装を、この深さまで形式検証したのは初めてだとしている。チームは、過去に修正済みのバグ2件をコードの隔離版に再び組み込み、バグを含むバージョンが定められたセキュリティ特性を満たさないことを示す証明をシステムに生成させた。

## 証明には限界も

これは、Signalのあらゆる部分や、このプロトコルを使うすべてのアプリにセキュリティ上の問題がないと数学的に保証するものではない。証明の対象はlibsignalの特定の性質であり、アプリ全体ではない。また、承認された仕様、Leanのチェッカー、低レベルの暗号処理ルーチンに関する契約を前提としている。The Registerは、実際のメッセージデータの計算量的な秘匿性まで証明したものではないと指摘している。一方、DeepMindの論文は、記号モデルと計算モデルの両方で証明したと説明しており、いずれも基礎となる暗号プリミティブに関する仮定に依存する。

DeepMindは、検証に使った資料を公開し、他の人も利用できるようにするとしている。医療機器のファームウェアや電力網のソフトウェアなどへの応用を目指す一方、この手法を拡大するにはさらなる研究が必要だという。今回の成果は、実社会で使われるコードをより広く検証するための一歩であり、ほかのシステムも検証済みだという証拠ではない。

## 事実

- Google DeepMindは2026年11月10日、AlphaProof Codeを発表した。
- このシステムはlibsignalの検証で、約650万行のLean証明コードを生成した。
- 検証対象は、コンパイル済みAArch64機械語におけるPQXDHハンドシェイクとTriple Ratchetだった。
- 研究者らが過去に修正済みのバグ2件を再導入したところ、対象のバージョンが指定されたセキュリティ特性を満たさないことをシステムが証明した。

## なぜ重要か

Signalの利用者にとって、今回の成果は中核プロトコルの実装における特定のセキュリティ特性に、機械で検証された証明を加えるものだ。ただし、アプリ全体にバグがないことを示すものではなく、暗号コンポーネントに関する前提にも依存する。

## 出典と参考資料

1. [Google Deepmind's AlphaProof Code verified Signal's cryptographic core in four weeks instead of years](https://the-decoder.com/google-deepminds-alphaproof-code-verified-signals-cryptographic-core-in-four-weeks-instead-of-years/) – The Decoder, 2026-11-11
2. [Introducing AlphaProof Code: a breakthrough in verifying complex software at depth](https://deepmind.google/blog/introducing-alphaproof-code/) – Google DeepMind, 2026-11-10
3. [Google DeepMind](https://google-deepmind.github.io/code-verification/) – Google DeepMind
4. [The Register](https://www.theregister.com/ai-and-ml/2026/11/10/google-deepmind-melds-humans-and-ai-agents-to-vet-signals-secure-messaging-techniques/5308625) – The Register

最終更新: 2026-11-11