Googleは、Gemini 4 Carbonへのアクセスを拡大し、このモデル上に構築されたエージェントがSignalプロトコルコードの中核的なセキュリティ保証を形式的に検証するのに貢献したと発表した。
有料の開発者および企業は現在、Gemini APIおよびGemini for businessを通じてCarbonを利用できるようになり、Google AI Ultraの加入者もアクセス可能となった。11月30日までは、入力および出力トークン100万あたり2ドルおよび10ドルの導入価格が適用され、その後は倍増する。トークンとは、モデルがコンテンツを読み取りまたは生成する際に処理するテキストの単位である。
これまで、GoogleのFairwindプログラムに参加する一部のサイバーセキュリティ専門家のみがCarbonを利用できた。彼らは依然としてこのプログラムに所属している必要があり、脆弱性の検出、悪用、修正に関する主要なベンチマークでトップとされるバージョンである「Carbon for cyber」にアクセスできる。
サイバーセキュリティへの応用
Googleによれば、Wiz社は「Carbon for cyber」を使用して、2つの主要なSaaSプロバイダーにおいて「ゼロデイ」タイプの脆弱性を2時間で発見したという。一方、GoogleのCloud Vulnerability Research (CVR) チームは、このモデルを使用して、ある人気のあるオープンソースプロジェクトの2つのバグが、攻撃者によってすでに悪用されているPHPの一対の脆弱性「PHP2Shell」に匹敵する深刻度で悪用可能であることを確認した。
「Carbonを使用して概念実証を構築することで、CVRはメンテナがバグを深刻度『クリティカル』に再分類し、迅速に修正パッチを公開するのを支援しました」とGoogleは述べている。
Signalのコード検証
また、Google DeepMindは、人間の専門家とAIエージェントを組み合わせてソフトウェアを形式的に検証（つまり、定義された要件を数学的に満たすことを証明）する「AlphaProof Code」を発表した。同チームはこれを、Signalプロトコルのリファレンス実装である「libsignal」に適用した。このプロトコルのバージョンは、WhatsAppやGoogle Messagesでも動作している。
人間が、CarbonおよびClaude Opus 5.5上で実行されるエージェントと協力し、証明すべき内容を記述する仕様書を作成した。その後、Carbonを基盤とするエージェントが、無効な証明を拒否する証明支援系であるLeanで記述された約650万行に及ぶ証明の全てを生成した。Googleによると、証明された保証（前方秘匿性、侵害後の安全性、認証など）はコンパイルされたマシンコードに対して有効であり、一方、プロトコルの検証の多くは設計のみを対象としているという。
5人の研究者がこの証明作業を4週間で完了した。Googleは、この作業は従来、専門家が数年かけて行うものと見なされていたと評価している。この手法が実際の脆弱性を検出することを確認するため、チームはすでに修正済みのlibsignalの過去の2つのバグを再導入し、これらのバージョンがもはやセキュリティ保証を満たさないことを証明した。
この結果は、Googleがコンパイルしたコードバージョン（小さなコマンドラインツールを通じて実行）に基づくものであり、「Signalアプリケーション自体」には及ばない。また、一部のサイドチャネルも分析の一部から除外されている。「これらの結果は、AIによって、歴史的にほとんどのソフトウェアにとって高すぎた形式的検証が、現実のシステムに対して実用的になり得ることを示唆している」と研究者らは記している。SignalのCTOであるEhren Kret氏は次のように述べた。「AIに関連するセキュリティ脅威が増大する中、Signalプロトコル実装の厳密な検証は、我々のコードのプライバシー保証に対するさらなる確信を与えてくれる」。Googleはまた、仕様書と証明を公開している。
