LLMエージェントのための検証可能な安全なツール利用：STPAとMCPの融合

私はしばらくの間、GuardAgent、ShieldAgent、AGrailといったガードレールに関する文献を読んできましたが、それらはすべて検出率を向上させる一方で、実際には何も保証できないことを密かに認めています。CMUとノースカロライナ州立大学のDoshiらによるこのICSE NIER 2026の論文は、異なる角度からアプローチしています。エージェントの不正な動作をより確実に検出する方法を問うのではなく、安全でない動作を形式的に不可能にする方法を問うているのです。これはポジションペーパーであり、実証研究ではありませんが、その枠組みは注意深く読む価値があるほど鋭いものです。

論文の概要

Aarya Doshi, Yining Hong, Congying Xu, Eunsuk Kang, Alexandros Kapravelos, および Christian Kästner による "Towards Verifiably Safe Tool Use for LLM Agents" (arXiv:2601.08012) は、LLMエージェントのツール利用に関する安全仕様を導出し、強制するための手法を提案しています。中心となる洞察は、エージェントシステムにおけるリスクは主に*ツールの合成（tool composition）*から発生し、個々のツールの失敗からではないため、コンポーネントレベルの保護策では防げないということです。例えば、カレンダーの競合を解決するエージェントが、プライベートな健康記録を正しく照会し、電子メールを正しく送信したとしても、その記録の内容を患者の同僚に漏洩させてしまうという、壊滅的な事態を引き起こす可能性があります。

提案されている解決策は2つの部分から構成されています。第一に、著者らは航空や原子力システムの安全工学手法であるSystem-Theoretic Process Analysis（STPA）を適用し、エージェントレベルのハザードを特定し、安全要件を導出し、それらをデータフローとツールシーケンスに関する仕様として形式化しました。第二に、各ツールが構造化されたメタデータ（機能階層：読み取り専用、書き込み専用、読み書き、実行；機密性分類；信頼レベル）を宣言する必要がある、機能強化されたModel Context Protocol（MCP）フレームワークを導入しました。強制メカニズムは4つの階層で構成されています：証明可能な安全でないフローのための自動ブロックリスト、必須シーケンスのためのマストリスト（mustlist）、事前承認された操作のためのアallowリスト、そして曖昧なケースのための確認エスカレーションです。

形式検証ステップでは、一次述語論理ツールであるAlloyを使用して実行空間をモデル化し、規定されたポリシーの下で安全違反が発生しないこと、かつ安全なトレースが到達可能であることを網羅的にチェックします。これが本論文の主要な「結果」です。NIER（New Ideas and Emergent Results）のショートペーパーであるため、ベンチマークの精度数値がないのは想定内です。

主なアイデア

• STPAは、エージェントの安全性をシステム工学の問題として再定義します。損失を特定し、危険な相互作用を遡って要件を導き出し、それを強制コードを書く前に実行します。
• 仕様は2つの種類に分類されます：情報フロー制約（例：「イベントメールには受信者に属さない個人データを含めてはならない」）と時相論理制約（例：「すべての update_event の後には、各出席者への send_email が続かなければならない」）。
• 4階層の強制（ブロックリスト / マストリスト / アallowリスト / 確認）は、セキュリティ疲労を軽減するように設計されています。ほとんどの安全なフローは事前承認されているため、エージェントが常に許可を求めることはありません。
• Alloyによる網羅的なトレース分析により、タスクの機能を維持しつつ、カレンダーのケーススタディにおいて安全でないフローが存在しないことが確認されました。
• このアプローチ全体は、汎用アシスタントではなく、タスク特化型エージェントを対象として明示的に範囲を絞っています。著者らは、限定的なエージェントの方が安全性を確保しやすいことを認めています。

何が有効で、何が不足しているか

知的な動きは健全です。安全性が重要な工学分野からSTPAを借用するのは正しい直感です。確率的なガードレールとは異なり、このアプローチは要件をシステムトレース上の述語に変換し、推定ではなく検証を可能にします。4階層の強制階層は思慮深く設計されています。特にブロックリストと確認の区別は重要です。なぜなら、永続的な確認プロンプトはユーザーの信頼を損ない、無視されるようになるからです。

とはいえ、この論文の限界は大きく、ほとんど対処されていません。メタデータの信頼性に関する問題は認識されていますが、解決されていません。フレームワーク全体が、ツールの開発者がツールを正確にラベル付けすることに依存しています。サードパーティのツールが一般的なオープンなMCPマーケットプレイスでは、ラベルの正確性を強制するメカニズムがありません。また、形式検証は手作りのAlloyトイモデルで行われており、アプローチの実現可能性は示していますが、実際のシステムに大規模に適用できることを示したわけではありません。

また、なぜハザード分析手法として、脅威モデリングやHAZOPではなくSTPAが最適なのかという説得力のある議論も見当たりません。カレンダーのケーススタディは例示的ですが、あまりにも小規模です。さらに、関連するMCPセキュリティ文献（arXiv:2601.17549）が詳細に調査している、機能を意図的に誤認させる敵対的なツールプロバイダーについての議論もありません。

率直な評価としては、これはコンセプト実証のための形式モデルを伴う設計提案です。ポリシーエンジンの構築、多様なツールにわたるラベルのカバレッジのテスト、自律性と安全性のトレードオフの実証的な測定といった、困難なエンジニアリング作業は今後の課題とされています。

金融AIにとっての重要性

Beancountへの書き戻しを行うエージェントは、まさにこの論文が想定しているハザードパターン、つまりツールの合成によって創発的なリスクが生じるという問題に直面しています。機密性の高い口座エントリを読み取り、その要約を共有元帳に投稿するエージェントは、個別のステップとしては完全に合理的であっても、システムレベルでしか見えない機密性制約に違反している可能性があります。ステークホルダーの損失から開始し、それを要件に反転させるSTPAのアプローチは、損失が規制違反、不正開示、不可逆的な元帳の変更である金融ドメインにきれいに当てはまります。

Beancountのツール群がますますMCPサーバーとしてラップされるようになっているため、MCPの拡張は直接的に関連しています。もしそれらのツールが機能階層や機密クラスを構造化され機械可読な形式で宣言できれば、エージェントが自己規制することを期待するのではなく、プロトコルの境界でデータフローポリシーを強制することが可能になります。「すべての post_transaction の前には成功した balance_check が必要である」といった時相論理制約は、金融エージェントが書き込みを確定する前に保証すべき不変条件そのものです。

現時点で欠けているピースは、これらがまだ実際に構築されテストされていないことです。しかし、元帳エージェントの安全性を考えるための設計語彙として、STPA + IFC（情報フロー制御）は、これまでの文献の中で最も原理に基づいたフレームワークです。

次に読むべきもの

• "Securing AI Agents with Information-Flow Control" — arXiv:2505.23643, Microsoft Research; テイントトラッキングを備えた具体的なIFCシステム（Fides）を実装し、AgentDojoで評価。本論文を実証的に補完するもの。
• "Breaking the Protocol: Security Analysis of the Model Context Protocol Specification and Prompt Injection Vulnerabilities in Tool-Integrated LLM Agents" — arXiv:2601.17549; 本論文のフレームワークが守ろうとしているMCPの攻撃面を直接分析。
• "Systematic Hazard Analysis for Frontier AI using STPA" — arXiv:2506.01782; AIシステム全般へのSTPA手法のより最近の適用例。この手法がどのようにスケールするかを理解するのに有用。