AlphaProof Codeとシグナル：検証済みマシンコードのセキュリティ証明と信頼された前提条件

この動画の要点

• AIエージェントが候補証明を生成し、Leanのカーネルがそれらが人間が承認した形式的主張を確立しているかを確認します。
• 検証対象は、信頼されたセマンティクスと暗号契約を持つ特定のコンパイル済みlibsignal CLIハーネスです。
• コンパイル済みバイナリを証明することで、そのバイナリの明示されたプロパティについて、Rustコンパイラが信頼された基盤から除外されます。
• 研究者らは、以前修正されたバグが記号的セキュリティ定理に違反する2つの孤立した再導入を報告しています。
• 比較器は、定理とすべての依存定義を保護された承認済み仕様に対してチェックします。修正は別のレビュープロセスを経て承認されます。

翻訳されたトランスクリプト

オリジナルの英語ナレーションから翻訳されています。利用可能なオーディオとキャプションはYouTubeによって管理されています。

AIセキュリティ証明をチェックするのは誰か？

0:00 AIセキュリティ監査は、やはりチャットボットを信頼するようなものに聞こえる。 Googleの新しいSignalの結果には、別のカーネルが チェックする数学的証明が付属している。このビデオでは、Googleは何を証明したのか？ そして、エージェントが目標を動かすのをどう防ぐのか？ これが役立つ答えだ。 モデルは候補証明を作成し、Leanはそれらの証明を 人間が承認した、選択されたコンパイル済みコードに関する主張に対してチェックする。 主張と前提は依然として人間が所有している。

0:21 モデルの勝利宣言を信じることなく、結果をチェックできる。 別のチェックで、質問が密かに変更されるのを防ぐ。 定義まで追ってみよう。 11月10日火曜日、The Daily Diffをお届けする。 AlphaProof Codeは、Googleのソフトウェア仕様作成フレームワークで、 人間のガイダンスに基づいて、AIエージェントを使って検証済み証明を生成する。 この研究は、Signalのメッセージングプロトコルを実装するRustライブラリであるlibsignalを、 特定のコマンドラインプログラム内で対象としている。

0:45 Googleは本日この研究を発表した。 その論文によると、5人の研究者が4週間かけて取り組んだという。 エージェントが証明を作成し、人間はほとんどの労力を 仕様に費やした。要件は、これまで以上に高価な 会議になる方法を見つけた。仕様は、プログラムが何をしなければならないか、

主張はどのように証明対象となるのか？

0:59 攻撃者が何を制御するか、そして議論に必要な前提条件を述べている。 レビュー担当者は、それがセキュリティ関係者が関心を持つものを捉えているかどうかを尋ねる。 弱い質問に対する見事に検証された答えは、その質問をそのまま残す。 チームは、Signalのハンドシェイクとそのメッセージキー ラチェットに関する以前の研究に基づいて構築している。形式的な分析はすでにそれらの設計を研究していた。 Googleの主張は、彼らのセキュリティ議論を、変更されていない本番環境の ライブラリのコンパイル済み実装に結びつけている。そこでは、設計が 実際のコードとの接触に耐えなければならない。Signalの最高技術責任者、Ehren Kretは、

1:27 以前の検証の小規模なスコープを超えた拡張について説明している。 実装の詳細には、順序が異なる メッセージや、遅延メッセージ用の アーカイブされたセッションが含まれる。実際のソフトウェアは、エレガントな図で捨て去った領収書を保管している。 研究者たちは、変更されていないRustライブラリを標準の

なぜコンパイル済みバイナリを証明するのか？

1:41 コンパイラでArm 64ビットLinux実行可能ファイルにコンパイルする。 彼らの定理は、形式的な命令モデルを使用してそのバイナリを記述し、 ソースコードと最適化されたマシンコードの間のギャップを埋める。 明示されたプロパティを破壊するコンパイラエラーがあれば、その定理は偽になる。 したがって、コンパイラはこのバイナリの信頼された基盤から外れる。 命令モデルとLeanのチェッカーは依然として信頼する。 信頼の境界が移動し、それにアドレスがある。 約650万行の検証済み証明は、約2万6千行の

2:06 信頼された仕様と命令セマンティクス行に基づいている。 これらはアーティファクトのカウントだ。 これらをインテリジェンススコアとして扱うのは、開発者を node modulesフォルダのサイズでランク付けするようなものだ。

どのセキュリティ特性が実装ギャップを乗り越えたのか？

2:16 議論は、メッセージの機密性と認証、 前方秘匿性、および述べられたモデルにおける侵害後セキュリティをカバーしている。 最後の2つは、キー盗難による損害の限界と、新しい 交換後の復旧について説明している。各保証には、攻撃者とセッションに関する条件がある。 暗号プリミティブは、信頼された契約の背後にある。 証明は、これらのルーチンが指定どおりに動作すると仮定し、暗号学的 セキュリティの前提に依存している。ある証明は暗号を理想化し、別の証明は 攻撃者の成功確率について推論する。

2:42 どちらもカバーするシナリオに制限がある。 どのビルド、どのプロパティ、どの前提条件であるかを問う。 この結果は、研究者たちのコマンドラインハーネスに関するものだ。 グループメッセージングは今後の課題であり、計算モデルは マルチデバイスの状態を除外している。すべてのSignalインストールがバグフリーであると呼ぶのは、 定理の範囲外だ。研究者たちは、以前修正されたSignalのバグ2つを

仕様は壊れたコードを拒否できるか？

3:02 隔離されたコピーに再導入し、コンパイルした。 検証済み証明は、これらのバイナリが記号的セキュリティ定理に違反していることを示した。 これは、仕様が実際の壊れた実装を拒否できるかどうかをテストしたものだ。 緑色のチェックマークには赤色のテストが必要だ。 Googleは、仕様と証明を検証手順とともに公開している。 リポジトリによると、クリーンビルドには数時間とかなりのメモリが必要だ。 発表を読むのは、ラップトップではかなり簡単だ。 ハードウェアモデルと信頼された契約は、まだレビューが必要だ。

3:26 このエピソードのために、巨大なアーティファクトを再構築していない。 私たちは公開された結果とその境界について報告している。 部外者がそれを検査する道筋があることは、別のAIの 勝利のラップよりも私にとって重要だ。さて、罠だ。

正しい証明は間違った質問に答えることができるか？

3:36 Leanは、ほとんど何も求めないステートメントの正しい証明を受け入れることができる。 不可能な前提条件は、定理を空虚なものにすることがある。 見出しの定理の下に埋もれている定義を変更すると、目標が弱まる可能性がある。 論文はこの点に対するチェックを設計している。 ゲートキーパーは、証明エージェントが書き込めない、承認済みの仕様を保持している。 彼らは別の修正プロセスを通じて修正を提案できる。 セキュリティの弱体化は、潜在的なバグとしてエスカレートされる。 証明者の成功宣言には、ここでは権限がない。

4:00 人間は、信頼された前提条件への変更を、 直接的またはポリシーを通じて裁定し、各キャンペーン後に修正案をレビューする。 専門家の判断は依然として責任を負う。 エージェントは異なる割り当てを要求できる。 自身に合格点を与えることはできない。

変化する目標を何が捉えるのか？

4:13 これが約束されたチェックだ。 Leanの比較器は、定理とそれに依存するすべての定義を、 その保護された承認済みコピーと比較する。 また、許可された公理もチェックし、新しいカーネルで証明を再現する。 したがって、ヘルパー定義を密かに弱体化させると、比較される対象が 変わる。承認された証明は、承認されたターゲットを確立しなければならない。 それでも、強力なターゲットと正直な 前提条件を選択する責任は人間にある。自分のAIワークフローでは、承認基準を

4:37 作業者の編集権限の外に置き、提案された変更を別途レビューすること。 Googleの結果は、その分離を具体化している。 証明作成者が作業を行い、 チェック境界がそれが有効であるかを決定する。 私が話すのを聞くよりもこれを読みたい場合は、diffが毎朝あなたの受信トレイに届き、 daily diff dot devで無料で利用できる。リンクは以下。 今日の評決はSHIP ITだ。

この証明ワークフローをSHIP ITするか？

4:54 私はこの検証済み証明ワークフローをSHIP ITする。なぜなら、承認された主張が 答えを生成するエージェントとは分離されているからだ。 私はすべての結果にスコープと前提条件を付記し続けるだろう。 購読し、ベルを押し、コメントであなたが異なるスタンプを押したかどうか教えてほしい。 そして、これが今日のdiffだ。 AxrisiのNikoだ。 責任を持ってマージしよう。

情報源

1. AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeepingSwarat Chaudhuri and colleagues / Google DeepMind and Google
2. Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO responsePushmeet Kohli and Swarat Chaudhuri / Google DeepMind
3. Code-verification repository — initial commit, public artifacts and checking instructionsGoogle DeepMind / GitHub
4. The PQXDH Key Agreement Protocol — older official specification and prior-analysis contextEhren Kret and Rolfe Schmidt / Signal
5. The Double Ratchet Algorithm — Triple Ratchet sectionTrevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
6. Google DeepMind leadership — Demis Hassabis's relevant lab identityGoogle DeepMind
7. Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsementChristopher P. Michel / Cmichel67 / Wikimedia Commons
8. Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlikeCreative Commons
9. Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claimImgflip / user-uploaded meme template
10. Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claimBoomerang Official / GIPHY / Tom and Jerry
11. Boomerang GIF source link — uploader-provided provenanceBoomerang
12. AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claimsHacker News
13. Code-verification licence — Apache 2.0 for Google code, third-party licences retainedGoogle / GitHub