はじめに
AIエージェントが外部APIや業務システムを操作する場合、「操作が許可されたこと」と「実際に安全な結果が得られたこと」は同じではありません。
例えば、次のような問題があります。
- TOCTOU（Time-of-Check to Time-of-Use）：承認後、実行直前までに条件が変わる
- 重複実行：通信障害で応答が失われ、同じ操作が再実行される
- 結果不明：操作を送信したものの、相手側で処理されたか確認できない
- 証拠の不整合：記録された実行結果と、許可された操作が対応していない
これらは、AIモデルの出力品質を評価するだけでは解決できません。
株式会社AIアシュアランスでは、こうした課題に対して、形式検証、実行時制御、証拠の再検証を組み合わせた「検証可能な実行保証（Verifiable Execution Assurance）」の研究開発を進めています。
今回、その一部を2つの公開PoCとしてGitHubに公開しました。
| 公開PoC | 検証対象 | 技術要素 |
|---|---|---|
| Cold Chain Cyber Assurance | 温度管理物流の引き渡し操作 | Python / JavaScript / Lean 4 |
| VPI Cyber Assurance | 企業間の接続・実行・取消し・切替え | Python / HTTP / SQLite / Ed25519 / Lean 4 |
公開リポジトリ：
本記事では、何を実装・検証し、どこまでを保証対象としているのかを解説します。
1. 実行保証で解決したい技術的課題
一般的な操作認可では、アクセス権限やポリシーなどから実行の可否を判定します。
しかし、重要な操作では、それだけでは不十分です。
例えば、企業Aが企業Bに処理を依頼する場合を考えます。
企業A
|
| 操作要求
v
企業B
|
| 承認
v
実行
|
| 結果通知
v
企業A
この処理中に通信障害が発生すると、企業Aは結果を確認できなくなる可能性があります。
企業Bでは処理済みかもしれません。それにもかかわらず、企業Aが同じ操作を再送したり、企業Cへ切り替えたりすると、二重処理が発生するおそれがあります。
そこで、今回のPoCでは次の3つを区別して扱います。
① 実行条件の成立
必要な権限、証拠、状態、期限などが満たされているか。
② 実行結果の確認
実際の作用と、承認された内容が対応しているか。
③ 次の操作への移行条件
結果が確認できない場合に保留するか、別の操作へ進めるか。
重要なのは、実行前の認可だけでなく、実行後の状態と次の操作への移行までを検証対象に含めることです。
2. PoC① コールドチェーン：状態遷移と形式検証
最初のPoCでは、温度管理物流における引き渡し操作をモデル化しました。
2.1 7つの条件と2つの状態
公開Leanモデルでは、次の7つの抽象的な条件を扱います。
| 条件 | 内容 |
|---|---|
quality |
品質判定 |
records |
必要な記録の有無 |
authorized |
実行権限 |
evidence |
証拠の適合 |
upstream |
上流工程の状態 |
changed |
承認後の条件変更 |
resultMatches |
実行結果との一致 |
また、実行状態として以下の2つを管理します。
-
consumed：対象の模擬操作がすでに作用したか -
quarantined：結果不一致などによって隔離された状態か
モデルの判定結果は、主に以下の4種類です。
| 結果 | 意味 |
|---|---|
denied |
条件違反などにより拒否 |
hold |
情報不足などにより保留 |
released |
実行・結果確認が成立 |
quarantined |
実行後の結果不一致を隔離 |
ここで重要なのは、hold と denied を区別することです。
例えば、記録不足によって保留になった操作は、不足情報を補完した後に再評価できます。
一方、操作が一度作用した状態で同じ要求を繰り返しても、状態を維持する同一セッション内では重複作用させません。
2.2 Lean 4で検証した性質
公開モデルの形式化は ColdChainPublic.lean に収録しています。
主な検証対象は以下です。
- 必要な権限がなければ模擬操作を呼び出さない
- 記録不足の状態では操作を実行しない
- 保留状態では作用を発生させず、条件補完後の再評価を許す
- 結果が一致しない場合、正常完了として扱わない
- 状態を保持した任意長の逐次操作列において、模擬作用が最大1回となる
Lean 4.32.1で37命題のカーネル検査が成功しています。
さらに、公開モデルの入力192通りと状態4通りを組み合わせた768組について、Lean側と実装側の出力照合を実施しました。
公開入力：192通り
×
状態：4通り
|
v
768組の具体的な出力照合
|
+-- Lean 4
+-- Python
+-- JavaScript
この照合では、判定結果だけでなく、理由、処理段階、操作件数、作用件数、成功確定、次状態などの対応を検査しています。
ただし、768組の照合は、公開モデルの対象入力・状態における一致確認であり、PythonやJavaScriptの実装全体を形式的に証明したものではありません。
2.3 実装検査と証拠検証
形式証明とは別に、以下の検査も実施しています。
| 検証項目 | 結果 |
|---|---|
| Lean形式検証 | 37命題 |
| 具体的な実装照合 | 768組 |
| Pythonテスト | 272検査 |
| JavaScriptテスト | 272検査 |
| 意図的に誤ったLean命題 | 5命題の拒否 |
| 既存の署名付き証拠 | 50ケースの照合 |
50ケースの証拠は、別の模擬WMSプロセスを用いた既存実証の記録であり、今回の公開ブラウザモデルの実行結果とは区別しています。
署名検証によって記録の改変を検出できても、入力された情報そのものが真実であることを自動的に証明できるわけではありません。
この限界も、公開検証の対象としています。
3. PoC② 企業間接続：結果不明時の切替えを制御する
2つ目のPoCでは、フィジカルインターネット構想における企業間接続を想定しました。
架空の3社を、それぞれ別プロセス・別SQLiteデータベース・別署名鍵で構成しています。
対象となる操作は、限定された引き渡し通知 handoff.notice です。
3.1 実行と結果確認の構成
基本的な処理は以下です。
企業A（送信元）
|
| 操作要求
v
企業B（受信先）
|
| 受信側の条件確認
| 承認
v
実行直前の再確認
|
| 送信元の条件確認
| 短期実行許可
v
企業Bでの処理
|
| DBへの作用記録
| 署名付き実行結果
| 監査記録
v
証拠の再検証
実行側では、受信側の条件と許可期限を再確認した上で、対象となるDB記録、署名付き結果、監査記録を同一トランザクション内で確定します。
これにより、今回の限定されたDB操作について、作用記録と実行結果の対応を扱っています。
3.2 結果不明時の切替え
特に重要なのが、企業Bから企業Cへの切替えです。
Bから応答が届かなくても、Bで処理が完了している可能性があります。
そこで、元の接続先における終端状態を区別します。
| 企業Bの状態 | 企業Cへの切替え |
|---|---|
COMMITTED |
切替えを拒否 |
CANCELLED |
新たな承認を取得して切替え可能 |
| 結果不明 |
HOLDを維持 |
通信タイムアウトだけを根拠に、Bで処理されていないと推定することはしません。
また、Bで取消しが確定した後に古い要求が遅れて届いても、その要求による実行を許さないようにしています。
3.3 Lean 4による検証
企業間接続の形式モデルは VpiAssurance.lean に収録しています。
例えば、取消し済みの終端状態に対して、遅れて実行要求が到着しても実行済み状態へ変更しない性質を表現しています。
公開コードの一部を抜粋すると、次のようになります。
theorem cancellation_fences_late_commit :
commitTerminal .cancelled = .cancelled := rfl
また、すでに実行済みの状態を、後から取消し済みとして扱わない性質も検証しています。
theorem commit_survives_cancellation :
cancelTerminal .committed = .committed := rfl
これらに加え、任意長の抽象イベント列について、BとCの両方が実行済みとなる状態を回避する不変条件も検証しています。
ただし、Leanモデルが証明しているのは抽象化された状態遷移の性質です。
HTTP通信、SQLite、暗号ライブラリ、実環境での物理的な作用までを包括的に形式証明したものではありません。
3.4 通信実験と独立検証器
企業間接続PoCでは、実際のローカルHTTP通信を使用して40シナリオを検査しました。
対象には以下を含みます。
- 通信応答の消失
- プロセス停止・再起動
- 同時再送
- 取消しと実行の競合
- 承認後の状態変更
- 証拠の改変・欠落
自動テスト122件を確認し、GitHub ActionsではUbuntu／WindowsとPython 3.11／3.13の組合せに加え、Lean 4.19.0による形式検証ジョブが成功しています。
なお、122件には40シナリオを実行する検査も含まれているため、別々の試験件数として合算するものではありません。
また、verifier.py は実行側の主要モジュールをimportせず、署名、記録のつながり、承認、実行、取消し、切替えの整合性を独立した手順で検査します。
これは実行側と検証側を分離するための設計ですが、両者に共通する仕様上の誤りまで排除することを証明したものではありません。
4. 手元でPoCを実行する
どちらも公開GitHubから取得できます。
4.1 コールドチェーンPoC
Python 3.10以上で、公開モデルの基本操作とテストを実行できます。
git clone https://github.com/GhostDriftTheory/verifiable-coldchain-cyber-assurance.git
cd verifiable-coldchain-cyber-assurance
# 公開モデルのテスト
python poc.py test
# 記録不足からの回復
python poc.py run --case missing --complete
# 正常成立後の再送
python poc.py run --case normal --repeat
また、リポジトリの index.html を開くと、ブラウザ上で条件を変更し、模擬引き渡しの挙動を確認できます。
形式検証と証拠検証は以下です。
python -m pip install cryptography==46.0.4
# 既存の署名付き証拠を検証
python poc.py verify-evidence
# 実装照合
python poc.py model-check
# Lean 4形式検証
python poc.py formal-check
形式検証にはLean 4.32.1が、実装照合にはNode.jsなどの必要な実行環境が求められます。
Lean未導入、証明失敗、実装不一致などの場合に成功扱いしない検証手順としています。
4.2 企業間接続PoC
こちらはPython 3.11以上を使用します。
git clone https://github.com/GhostDriftTheory/verifiable-physical-internet-cyber-assurance.git
cd verifiable-physical-internet-cyber-assurance
python -m pip install -r requirements.txt
# ローカル通信実験と画面表示
python demo.py --serve
実行側と別の検証器による証拠の照合も可能です。
# 同梱された証拠の検証
python verifier.py sample.json
# 新しい通信実験
python demo.py --output run
# 新しい実験結果の検証
python verifier.py run/sample.json
# 自動テスト・通信検査
python validate.py
Lean 4.19.0を導入した環境では、形式検証を必須として実行できます。
python validate.py --require-lean
5. 形式検証で保証できること・できないこと
今回のPoCで特に重視したのは、形式証明と実装検査の対象を区別することです。
| 項目 | 今回の検証範囲 |
|---|---|
| 状態遷移の安全性 | 公開Leanモデルの前提下で形式検証 |
| 実装と形式モデルの対応 | 指定された具体入力・状態で照合 |
| 通信障害時の挙動 | ローカルHTTP環境で検査 |
| 証拠の整合性 | 公開された記録と検証条件を照合 |
| 実際の物流・外部APIの安全性 | 未実証 |
| 入力情報の真実性 | 自動的には保証しない |
| 実環境の全操作における重複実行防止 | 未実証 |
特に、証拠が整合していることと、現実世界でその内容が真実であることは区別する必要があります。
また、事後的に結果不一致を検出して隔離できても、すでに発生した作用を取り消せるとは限りません。
こうした保証範囲を明確にすることも、実行保証を設計する上で重要な要素です。
6. AIエージェントへの応用可能性
今回のPoCは、実際の生成AI APIを接続した実験ではありません。
ただし、扱っている技術的課題は、AIエージェントのツール実行や、複数システムにまたがる自動化と共通しています。
例えば、AIエージェントが外部システムを操作する際に、次のような設計が考えられます。
AIエージェント
|
| 操作提案
v
実行条件の検証
|
+-- 不適合 → 拒否
|
+-- 情報不足 → 保留
|
+-- 条件成立
|
v
実行時制御
|
v
外部システム
|
v
実行結果の確認
|
v
証拠の再検証
|
v
次の操作の可否判断
この構成では、AIが提案したこと自体を実行権限とは扱いません。
実行条件が成立しているかを確認し、その結果を検証した上で次の処理へ進めます。
実際のAIエージェントや業務システムに適用するには、ツール呼び出し経路への制御の組込み、認証・権限管理、障害回復、実行結果の観測などを追加で設計・検証する必要があります。
おわりに
AIの安全性を考える際には、モデルが適切な提案を生成できるかだけでなく、その提案をどの条件で現実の操作につなぐべきかが重要になります。
今回の2つのPoCでは、以下の点を公開モデルとして検証しました。
- 実行条件が成立しなければ操作を進めないこと
- 条件を補完すれば、保留された操作を進められること
- 結果不一致を正常完了として扱わないこと
- 通信結果が不明な場合、別の接続先への切替えを保留すること
- 形式証明、実装検査、証拠の再検証を組み合わせること
AIが操作を提案できることと、その操作を実行してよいことは別です。そして、操作を許可できることと、実行結果を確認できることも別です。
この違いをシステムとして扱い、後から検証できる形にすることが、今回のサイバーアシュアランス技術の目的です。
今後は、物流・倉庫システム、企業間データ連携、クラウド・AI基盤など、実環境との接続検証を進めていきます。
参考リンク
公開リポジトリ
関連する技術・発表
株式会社AIアシュアランス
※公開PoCは限定された参照モデルと模擬環境を対象としています。実環境全体の安全性、規制適合、第三者認証を示すものではありません。公開コードの利用条件は各リポジトリをご確認ください。