セキュリティ

米Google DeepMindは11月10日（日本時間10日）、形式検証の新しい枠組み「AlphaProof Code」を発表した。人間の指導のもとでAIエージェントが、メッセージアプリSignalの暗号プロトコルの参照実装「libsignal」について、前向き秘匿性や認証などの主要なセキュリティ特性を、コンパイル済みの機械語の水準で数学的に証明した。論文によるとエージェントが生成した証明は約650万行で、作業は5人のチームで4週間だった。対象はCLIで動かす実行ファイルで、低水準の暗号処理は前提として扱っている。

開発支援AIの米Cursorは10月29日、自社の拡張機能ストアで、Anthropic製の拡張機能「Claude Code」を改ざんした版が約11時間配られていたと公表した。入れた利用者は最大約5000人。改ざん版は端末の情報を集め、攻撃者がSSHで入り込めるよう設定を書き換えようとした。Cursorはストアを止めて作り直し、2.1.314以降への更新を求めた。ほかのストアで配られた版は影響を受けていない。