OpenShellでのAIエージェント制御への形式手法適用から学んだこと

OpenShellにおけるAIエージェント制御への形式手法適用から得られた知見

本稿では、パーミッションレビューがエージェント規模で破綻する理由と、Z3オープンソースライブラリを使用して、エージェントが提案するポリシー変更が承認された範囲内に収まっていることを示す形式的な証明を作成する方法について掘り下げます。

なぜパーミッションレビューはエージェント規模で破綻するのか

AIエージェントはますます賢くなり、我々が彼らに依頼する作業はますます自律的になっています。現在、多くの人がClaudeやCodexを使って、一度に1つのPRを反復処理するために少人数のエージェントグループを使用しています。ますます、私たちはエージェントに、数百または数千時間かけて作業する数百のエージェントを必要とする、長期間でオープンエンドなリサーチタスクを任せるようになりつつあり、これはセクターにおける次のブレークスルーを解き放つ可能性があります。

これらのユースケースが拡大するにつれて、いくつかのことが起こり始めます。

• エージェントのニーズは進化します。エージェントはタスクを進めるにつれて、データストア、コーディングリポジトリへのアクセス、インターネット検索能力、詳細なシミュレーションやテストの実行能力を必要とするようになります。
• 人間の監督はスケーリングしなくなります。これらのタスクが実行される規模では、すべてエージェントに対する人間の監督自体が不可能になります。

これは難しい問題提起をします。それぞれが独自のスコープされたポリシーを持つエージェントのグループが協力して作業する場合、システム全体に付与された権限を超えないようにするにはどうすればよいでしょうか？インターネットへの書き込みアクセスを持つエージェント、セキュリティツールへのアクセスを持つエージェント、あるいは「競合リサーチを行う」といった広範にスコープされたチャーターの下で作業するグループを想像してみてください。システムを人間のオペレーターの意図内に保つにはどうすればよいでしょうか？

これには、サンドボックス権限のリストを凝視するのをやめ、より高レベルで宣言的な方法で考え始めることができる、新しい制御とメカニズムのセットが必要です。本稿では、OpenShellチームがこの分野で行っている研究の一部、特に形式手法の使用について掘り下げ、単一のエージェントだけでなく、エージェントシステム全体の能力の「証明」を構築します。

私たちの考えを変えたデモ

OpenShellの最初のデモの1つで、Jensenのために、OpenShellのREST検査エンドポイントを使用して、広範にスコープされたAPIキーへのアクセス権を持つにもかかわらず、OpenClawエージェントがGitHubリポジトリへの書き込みを選択的に許可する能力を実演しました。デモは期待通りに始まりました。OpenShellのサンドボックスは、禁止されたリポジトリへの書き込み試行を検出し、それをブロックしました。次に表示されたメッセージは「ファイルは[禁止されたリポジトリ]に正常に書き込まれました」でした。ここで何が起こったのでしょうか？エージェントは自分がサンドボックスで実行されていることを認識し、次に低レベルのGitHubバイナリであるgit-remote-httpsを使用してGitHub認証情報を利用し、当時、リポジトリのクローンを許可するためにポリシーで承認していましたが、それらが書き込み能力を持つとは知らなかったバイナリを使用して、OpenShellのレイヤー7HTTP/REST/MCP検査をバイパスしました。

巧妙です。そして、ネットワーク、ファイル、ツール、AIモデル、および認証情報アクセスに関するサンドボックス/ランタイムポリシーの間には、AIエージェントが人間のオペレーターが明示的に望まないことを実行できる可能性のある意図しない組み合わせの指数関数的な数があるという点が浮き彫りになりました。

過去の作業 - AWSでのEC2、IAM、S3ポリシーの証明

2016年頃、私たちのチームのメンバーはAWSで働いており、同様の課題に直面していました。AWS IAMポリシー、AWS S3ストレージポリシー、履歴バージョンサポートのすべての素晴らしい複雑さを考えると、S3オブジェクトがパブリックインターネットからアクセス可能かどうかを断定的に言うことはできますか？

今日、これは少し奇妙に聞こえますし、2016年にもそうでしたが、システムを制御するために記述するポリシー間の可能な複雑さとレイヤー化された相互作用を考えるとそうではありません。Byron CookとAWSの同僚はZelkovaを開発しました。これはAWSアクセスポリシーをSMTフォーミュラとして形式化し、2018年にその作業を発表したときにはすでに毎日数百万回呼び出されていました。その取り組みはAWS全体に広がり、後の作業では1日あたり10億のSMTクエリへのスケーリングについて説明されています。

そのアイデアは、形式手法、特に定理証明器を使用して、IAM、S3、およびEC2ポリシーを形式的にモデル化することでした。これらのポリシーとその相互作用を形式論理でモデル化したら、不変条件（真であると期待されるもの）が成り立つことを証明できます。これは非常に成功し、複雑なポリシーを形式論理でモデル化するという集中的なタスクの後、それらの間の実際のクエリは非常に高速になり、コンピューティングリソース全体で水平にスケーリングできるという追加の利点がありました。

同じ問題、今度はエージェントで

今日の私たちの課題は非常に似ています。エージェント、またはエージェントシステムはそれぞれ、ファイルシステム、ネットワーク、認証情報、ツール、およびMCPポリシーを持っており、それぞれ異なる機能を持っており、エージェントが異なるエージェントと通信できるため、それらを組み合わせて使用できます。

Frontier Labsは、専門モデルによるエージェントアクションの信頼できるAIエージェントレビューを提唱しており、最も重要なイベントを人間の承認のためにエスカレートし、承認の疲労を軽減しています。しかし、AIモデルは、人間と同様に、確率的であり、重要な詳細を見落とす可能性があります。さらに、すべてのエージェントアクションを同等の知能を持つレビューアモデルでレビューすると、コンピューティングコストが2倍になり、総トークンスループットが半分になります。

OpenShellで実験および検証しているのは、形式手法を使用して、ポリシー内の特定の不変条件（たとえば、コードリポジトリへの書き込みや本番データベースへの削除をブロックするルールをバイパスする意図しない方法）をモデル化し、柔軟に「証明」することです。ポリシーのモデリングは複雑であり、最新の状態に保つ必要があることがわかりましたが、非常に強力な利点があります。

• いつでも不変条件を形式的に監査または証明できる能力
• ポリシーの理解に対する決定論的な「証明」
• これらのチェックはミリ秒単位で実行され、トークンは不要

これらの論理チェックは、一時的な使い捨てリポジトリへの削除アクセスを要求する場合と本番リポジトリへの削除アクセスを要求する場合のようなコンテキストを理解しません。しかし、人間または信頼できるAIレビューアと組み合わせることで、これらの証明は、機密性の高い物理的（現実世界）または規制管理された環境で実行するために必要な形式的な監査トレールを提供し、かつ、誤解されたり誤誘導されたりすることのない出力により、確率的なAIレビューアに信じられないほどの価値を提供できます。

ポリシー定義に対する証明は何をもたらすのか？

私たちは、形式手法をエージェント制御における非常に有望な研究分野と見なしています。これらの証明が実際にどのように機能するかについては、こちらのアドバーサリアルリサーチ実験を参照してください。https://nvidia.github.io/OpenShell-Research/dev-notes/posts/2026-08-27-adversarial-policy-review-long-horizon-agents/

形式手法は、ポリシー検証にのみ使用されてきたわけではなく、フライト制御システム、コアインターネットスイッチングおよびルーティング、システム上のソフトウェア間の複雑な依存関係が正しく一致することを保証するために日常的に使用するパッケージマネージャーなど、クリティカルシステムで長い歴史があります。

多くのAI研究者にとって、大学で形式検証のクラスを取ったことがあるかもしれませんが、実際に形式検証を使用したことがある人はごく少数です。本稿の残りの部分では、アルゴリズム検証の入門を探索し、人気のあるオープンソースソルバーを使用して、OpenShellでのエージェント制御のための最小限の例をゼロから構築します。

SAT、SMT、およびZ3を5分で

コンピュータサイエンスと形式手法では、SAT（充足可能性）ソルバーは、ブール式が充足可能かどうかを回答します。変数（たとえばxとy）に真となる可能な値がある場合、SATソルバーはtrueを返します。そうでない場合はfalseを返します。

変数aとbのような変数を与えると、この式を真にする割り当てを見つけることができます。

a AND (NOT b)

対照的に、SMT（充足可能性モジュロ理論）ソルバーは、整数、実数、文字列、正規言語、配列、ビットベクトル、およびその他の有用なドメインといった理論で推論のスタイルを拡張します。

Z3は、Microsoft Researchによって開発および保守されているSMTソルバーおよび定理証明器です。Z3は汎用的であり、私たちの特定の剤ポリシーの要素をZ3が理解する構造にマッピングするためのコードを構築する必要があります。

たとえば：

• ポートは整数です。
• ホストとパスは文字列です。
• *、**、/.*/**のようなグロブは正規表現として表すことができます。
• ポリシーの合成はブール論理になります。

Z3ガイドは、以下の例に慣れてきたら、最も参照すべきものです。

いくつかの構造が、私たちが求めていることのほとんどをカバーしています。

クエリの方向性は重要です。

私たちはZ3にこれを証明するように依頼しません。

提案されたポリシーの追加は安全である

私たちは質問を形式的にモデル化し、非常に具体的な質問に答える必要があります。たとえば、このユースケースのためにZ3でモデル化した、より一般的で有用な証明の1つは、提案されたポリシーが、専門家によって事前に定義されたポリシー（たとえば、GitHub読み取り専用）では許可されないアクションを許可できるかどうかを尋ねるものです。前述のOpenClawがレイヤー7RESTポリシー検査をバイパスしようとした例に戻ると、レイヤー4を介したバイナリとネットワークアクセスを組み合わせることで、レイヤー4の機能がレイヤー7の機能を超えていることをZ3にエンコードします。したがって、認証情報（GitHub）とバイナリ、およびレイヤー4を介したネットワークアクセスを組み合わせたものは、レイヤー7（REST）を介した同じ認証情報+「gh」バイナリの以前に許可された組み合わせを超えています。プロバーはこれをすぐに検出し、警告を発します。

この場合のクエリは次のようになります。

proposed_policy_allows(action)
AND NOT safe_policy_allows(action)

または同じプロパティをセット差として記述することもできます。

Allowed(candidate) ∖ Allowed(safe_policy) = ∅

ソルバーがsatを返す場合、差は空ではありません。つまり、提案されたポリシーに、事前に承認された参照ポリシーには存在しない機能が存在することを意味します。

unsatを返す場合、モデル化された反例は存在しません。つまり、不変条件（仮定）のいずれも侵害されていないことを意味します。この種のクエリを自分で記述してみましょう。

最初の包含クエリ

ここにZ3のネイティブSMT-LIB形式の小さな例があります。これをcontainment.smt2として保存し、次を実行します。

z3 containment.smt2

この例では、同じ最大値に対して2つの候補ポリシーを比較します。

(declare-const binary String)
(declare-const host String)
(declare-const port Int)
(declare-const layer String)
(declare-const method String)
(declare-const path String)

; アクションのドメイン: 各リクエストは生のL4または検査されたRESTのいずれかです。
(assert (or (= layer "l4") (= layer "rest")))

; 強制されるRESTルールは、検査されたRESTトラフィックのみをカバーします。
(define-fun maximum-allows () Bool
  (and (= binary "/usr/bin/gh")
       (= host "api.github.com")
       (= port 443)
       (= layer "rest")
       (= method "GET")
       (str.prefixof "/repos/NVIDIA/OpenShell/issues/" path)))

(define-fun broad-candidate-allows () Bool
  (and (= binary "/usr/bin/gh")
       (= host "api.github.com")
       (= port 443)
       (= layer "rest")
       (= method "POST")
       (str.prefixof "/repos/NVIDIA/" path)))

(define-fun narrow-candidate-allows () Bool
  (and (= binary "/usr/bin/gh")
       (= host "api.github.com")
       (= port 443)
       (= layer "rest")
       (= method "GET")
       (= path "/repos/NVIDIA/OpenShell/issues/123")))

; 同じホストとポートへの生のL4ルールには、検査するメソッドやパスはありません。
; これはL4 *および* それを介して実行できるもの（RESTを含む）をカバーします。
(define-fun l4-candidate-allows () Bool
  (and (= binary "/usr/bin/gh")
       (= host "api.github.com")
       (= port 443)
       (or (= layer "l4") (= layer "rest"))))

; チェック1: 広範な候補は最大値を超えますか？
(push)
(assert (and broad-candidate-allows (not maximum-allows)))
(check-sat)
(get-value (layer method path))
(pop)

; チェック2: 狭い候補（GET、1つの問題）は最大値を超えますか？
(push)
(assert (and narrow-candidate-allows (not maximum-allows)))
(check-sat)
(pop)

; チェック3: 同じホストとポートへの生のL4ルールは最大値を超えますか？
(push)
(assert (and l4-candidate-allows (not maximum-allows)))
(check-sat)
(get-value (layer method path))
(pop)

最初のチェックはsatを返し、上記のget-modelは、安全な（最大）ポリシーでは許可されなかった組織のルートへの書き込みを示す証拠を返します。

sat                                                  ; チェック1: 広範な候補
((layer "rest") (method "POST") (path "/repos/NVIDIA/"))
unsat                                                ; チェック2: 狭い候補
sat                                                  ; チェック3: 生のL4
((layer "l4") (method "") (path ""))

2番目のチェックはunsatを返します。狭い候補が許可するすべての操作は、最大値内で既に許可されています。3番目のチェックは、前述のOpenClawのシナリオです。レイヤー4候補は、参照最大ポリシーと同じホストとポートを指定しますが、レイヤー4を介して通信します。これはOpenShellで強制できないワイヤープロトコルを使用します。プロバーはsatをlayer = l4および空のメソッドとパスで返します。この場合、L4がL7 RESTよりも広範であることを明示的に記述するルールを書く必要はありませんでした。これはエンコーディングから効果的に導き出されます。

OpenShellポリシー全体を形式論理としてエンコードする方法

OpenShellのランタイムプロバーは、任意のネットワークアクションに対して次の属性をモデル化します。

action = {
  binary: String,
  host: String,
  port: Int,
  layer: String,
  method: String,
  path: String
}

注: 上記のアクション例はサブセットにすぎません。OpenShellランタイムは、ファイルシステム、プロセス、認証情報、および推論の包含もカバーします。

エージェントによって提案されたポリシー変更を、Z3でチェックできるアクションにエンコードするために、Rustで記述されたコードを使用します。エンコードしたら、さまざまなチェックを実行できます。最初の非常に一般的なチェックは、候補（提案された）ポリシーが参照（安全な）ポリシーではできないことを実行できるかどうかを尋ねます。

let candidate_allows = policy_allows(candidate, &action);
let maximum_allows = policy_allows(maximum, &action);

solver.assert(Bool::and(&[
    candidate_allows,
    !maximum_allows,
]));

match solver.check() {
    SatResult::Unsat => MaximumPolicyCheck::WithinMax,
    SatResult::Sat => {
        let model = solver.get_model().expect("sat result has a model");
        let counterexample = counterexample_from_model(&model, &action)
            .expect("model contains a symbolic action");
        MaximumPolicyCheck::ExceedsMax { counterexample }
    }
    SatResult::Unknown => MaximumPolicyCheck::Unsupported {
        reason: "Z3 returned unknown".to_owned(),
    },
}

概念的には次のようになります。

policy_allows(a) = ⋁ rule_allows(rule, a)

rule_allows(rule, a) =
  binary_matches(rule, a) ∧ endpoint_matches(rule, a)

ここで、ポリシー言語全体をモデル化する複雑さが見え始めます。たとえば、OpenShellは*および**グロブセマンティクスをサポートしています。これらはZ3正規表現にコンパイルされます。グロブメカニズムに精通した人間として、単一の*はパスの/やホストの.を越えることはできないことを知っていますが、**は越えることができます。そのため、Rustコードを使用してこのロジックをエンコードします。Z3の正規表現理論は、シンボリック文字列が結果の言語に属するかどうかをチェックできます。そのスコープは意図的です。OpenShellは、任意の言語固有の正規表現ではなく、正規言語フラグメントをモデル化し、バックスラッシュなどの機能を使用します。サポートされていないポリシーサーフェスはクローズドで失敗します。包含に関する研究の詳細については、OpenShellのスパイクで最大ポリシーとナローネスバジェットを参照してください。https://github.com/NVIDIA/OpenShell/blob/spike/maximal-policy-prover-subset/crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md

エキスパートクエリは単なる数式です！

上記の例では、非常に一般的で拡張可能なクエリを使用しました。基本的に、どれほど複雑であっても、提案されたポリシーが、既にレビュー済みの別の安全なポリシーのサブセットであるかどうかを尋ねます。しかし、ポリシー言語をZ3でモデル化したら、好きなことについて質問できます。

OpenShellのポリシーアドバイザーには、提案されたポリシーすべてに適用される4つのエキスパートセキュリティチェックが組み込まれており、人間のレビューアまたはエージェントレビューアの承認のために提供されます。アドバーサリアルテストでは、これらのチェックの結果（騙されたり、操作されたり、直接無効化されたりすることのない）をエージェントレビューアのコンテキストとして提供することが、エージェントまたは人間のレビューアの信頼性を高めるための信じられないほど価値のある方法であることがわかりました。詳細はこちらをご覧ください。https://docs.nvidia.com/openshell/sandboxes/policy-advisor。

現在、OpenShellポリシープロバーは、承認前に提案されたすべてのポリシーに対して実行されるエキスパートクエリをエンコードしています。ドキュメントより：

結論

私たちは、長期間にわたる継続的に拡大し、重要ないタスクにおいて、エージェントを管理、監査し、信頼性を構築するのに役立つ形式手法の可能性に非常に興奮しています。形式手法に取り組んでいる方、またはOpenShellへの貢献に興味がある方は、CNCF Slackで私たちに連絡するか、週次のコミュニティミーティングに参加してください（サインアップはこちら：https://github.com/NVIDIA/OpenShell）。

リソース

上記の例に慣れてきたら、Z3の決定的な参照資料

• Z3ガイド
• Z3: 高効率SMTソルバー
• Z3正規表現
• Z3ソースと言語バインディング

同じ問題に対するDeepMindの検証済みコード生成アプローチ

• VeriGuard: 検証済みコード生成によるLLMエージェントの安全性向上

AIによるエージェント権限レビューに関するブログ

• 実践における信頼できるエージェント
• AIエージェント構築の実践ガイド

formal-methods z3 agent-security