PRESS RELEASE 調査・レポート 2026/11/02 09:30

AIセーフティに「検証可能な実行保証」を。株式会社AIアシュアランス、「サイバーアシュアランス」の公開PoC2件を発表

AIセーフティに「検証可能な実行保証」を。株式会社AIアシュアランス、「サイバーアシュアランス」の公開PoC2件を発表　株式会社AIアシュアランスのプレスリリース

株式会社AIアシュアランスがPR TIMESで配信したプレスリリースの原文を、Zero Press が転載して掲載しています。

株式会社AIアシュアランス（本社：東京都新宿区、代表取締役：前木秀光）は、AI・自動化システムの重要な操作について、「実行してよい条件」と「実際の結果」を証拠から確かめるサイバーアシュアランス技術の公開PoC（概念実証）2件を発表します。対象は、コールドチェーンの引き渡しと、検証可能なフィジカルインターネット構想を支える企業間接続です。[1]–[4]

不適合な要求を止めるだけでなく、不足する情報を補えば進めること、処理の重複を抑えること、結果が分からないまま次へ進めないことを、操作デモ・公開コード・検証記録で示します。両PoCの公開モデルは、定理証明支援系Lean 4による形式検証を含む自動検査に成功しています。[2][4]

中核は「何を許したか」と「何が起きたか」を切り離さないこと

当社のサイバーアシュアランスは、形式検証を中核に、証拠の再検証と実行時の強制制御を組み合わせた「検証可能な実行保証」技術です。操作前後の状態、承認、作用範囲、実行結果を証拠で結び付け、実行時の許可・拒否・継続制御につなげます。

AIの提案や、過去に得た承認を、そのまま実行権限とは扱いません。実行直前の条件を確認し、実行後は結果との対応を確かめます。攻撃検知や認証を置き換えるのではなく、それらと接続して、重要操作を進める最後の段階と、その後の確認を支える基盤です。

PoC① コールドチェーン：品質が正常でも、引き渡しを許可できるとは限らない

温度管理が必要な物流では、品質の判定だけでなく、受領する権限、記録の不足、上流での保留、実行直前の変更も確認する必要があります。本PoCは、これらを分けて確認し、条件が成立したときだけ模擬引き渡しを実行します。[1]

例えば、記録不足なら保留し、不足を補って条件がそろえば進めます。一度成立した同じ要求を再送しても、重複して引き渡しません。実行結果が確認対象と食い違う場合は、その結果を正常完了として扱わず、隔離します。

「問題があるのに進める」と「解消できたのに止め続ける」の両方を避ける。その判断と結果を、後から確かめられることが、このPoCの価値です。

公開画面では、条件の変更、記録の補完、再送を自分で試せます。操作を呼び出したか、作用が生じたか、正常完了を確定したかを比較でき、保存記録も再検査できます。

公開PoC： https://github.com/GhostDriftTheory/verifiable-coldchain-cyber-assurance

PoC② 企業間接続：相手側の結果を確かめてから、接続先を切り替える

当社とオンザリンクスが共同発表した「検証可能なフィジカルインターネット」は、企業が異なる目的や既存システムを維持したまま連携する構想です。今回、当社は、そのプラットフォームに必要な接続・実行保証の部分を、架空3社のシステムが通信するPoCとして公開しました。[3][5]

各社は自社の状態と条件を持ち、社内データを一括共有せず、限定した引き渡し通知を授受します。元の接続先で処理されたか分からない場合は、別の相手への切替えを保留します。取消しが確定した場合に限り、切替先について新たに承認を得ます。すでに処理済みなら、別の相手へ同じ処理を重ねません。

通信応答の消失、処理の途中停止、同時再送、承認後の変更など40シナリオを実際のプロセス間通信で検査しました。一社との接続が失効・停止しても、条件を満たす無関係な操作は継続します。また、実行側とは別の検証器によって、承認・実行・取消しの証拠の整合性を再検査できます。[3][4]

相手側の処理を確かめずに切り替える二重処理を避けながら、無関係な連携まで一律に止めない。企業ごとに管理が分かれる連携を、確認できる根拠で支えるPoCです。

公開PoC： https://github.com/GhostDriftTheory/verifiable-physical-internet-cyber-assurance

なお、今回公開した2件のPoCおよび本プレスリリースは、当社が独自に実施・発表するものであり、株式会社オンザリンクスとの共同実証・共同発表ではありません。

政府が重視する「実行前検証・権限管理・観測と制御」に応える

総務省は2026年3月27日のAIセキュリティ対策ガイドラインで、ツール呼び出し前の検証や権限管理を具体化しました。AISIは7月7日の評価観点ガイド第1.20版で、AIエージェントの「観測と制御」を追加。総務省・経済産業省のAI事業者ガイドライン検討に関しても、10月28日に「AIによるリスク」の検討ワーキンググループ資料が公開されています。[6]–[8]

当社は、AIが業務システムや外部環境へ作用する場面に着目し、こうした政策課題に実行条件の検証と証拠の再確認で応えます。AIを業務に導入する企業が、システムの違いを越えて利用できる「検証可能な実行保証基盤」を目指します。

AIセーフティを「実行許可」から「検証可能な実行保証」へ

海外では、AWSのDogwoodが操作履歴・順序・結果に基づく実行時制御を、ICME LabsのPreFlightが形式的な規則による実行前判定と検証可能な証拠の生成を扱っています。証明と実行制御を結び付ける研究・実装も進展しています。[9]–[13]

しかし、AIや自動化システムが重要操作を行う場合、「操作を許可できること」と「相手先で何が実行され、次の操作へ安全に進めること」は同じではありません。

例えば、企業Aから企業Bへの操作が許可されても、通信障害によって結果が確認できなければ、Bで処理済みなのか未実行なのか分かりません。そのまま企業Cへ切り替えると、二重実行につながるおそれがあります。[3]

当社が今回提示するのは、単なる実行許可の判定ではなく、実行条件・実行結果・次の操作へ進む条件を結び付け、その保証範囲と証拠を第三者が再検証できる参照実装です。

既存のAI実行制御製品を導入していても、企業間の結果確認や取消し確定まで要求する場合には、それらを含む実行保証の設計・検証が必要です。[1]–[4]

なお、今回の実証は公開参照モデルと模擬環境を対象とし、実環境全体の安全性や、他社製品に対する性能上の優位性を証明するものではありません。[1][3]

2025年の基礎出願から続く、PCT国際出願5件

本技術群について、以下の5件のPCT国際出願を行い、2025年10月・11月の国内基礎出願に基づく優先権を主張しています。

技術の対象

PCT国際出願番号

操作制御・証拠保全・再検証

PCT/JP2026/034664

証明有効条件・実行協調・通信継続制御

PCT/JP2026/034666

操作後の安全継続・必要資源の確保

PCT/JP2026/034667

データ開示・外部処理結果の採用制御

PCT/JP2026/034668

派生情報の利用条件承継・利用終了検証

PCT/JP2026/034894

2026年5月26日には、「正当な証拠チェーンのない実行を通さない」という考え方を、ADICサイバーアシュアランス拡張のLean 4形式証明として公表しました。今回の公開PoCは、2026年5月に公表した形式検証の考え方を、物流・企業間接続の具体的な操作へ展開したものです。実行条件の検証と、操作結果を再検証できる仕組みを公開コードで示しています。 [14]

既存の物流・通信・セキュリティ基盤に組み込む

想定する接続先は、物流・倉庫システム、企業間データ連携、通信・ネットワーク、クラウド・AI基盤です。既存の認証、監視、ネットワーク検証、業務システムを置き換えるのではなく、重要操作の許可と結果確認をつなぐ層として組み込むことを目指します。

公開対象は、挙動を確認できる参照モデル、形式証明、試験結果、再検証に必要な証拠・手順に絞っています。今後、実環境との接続検証や共同実証への展開を目指します。

代表コメント

株式会社AIアシュアランス　代表取締役　前木秀光

「AIの提案が優れていても、そのまま実行してよいとは限りません。品質が正常でも、受け取る権限や記録が足りない。相手から返事がなくても、処理は済んでいるかもしれない。現場で問題になるのは、こうした判断と実行の間の違いです。

私たちは、止めるべき操作を止めるだけでなく、確認できた処理は進め、その根拠と結果を後から確かめられる仕組みをつくっています。企業やシステムが違っても、確認できる証拠でつながる。AIを安心して業務に任せられる範囲を広げる共通基盤として、日本発のサイバーアシュアランスを育てていきます。」

技術解説：具体的な検証結果と、その読み方

以下は2026年11月1日に確認した公開版とCI（継続的インテグレーション：コードの自動検査）の記録に基づきます。件数は検査の種類を分けて示し、合算した攻撃遮断数や実運用の安全確率には換算しません。CI成功は検査の実行結果であり、第三者監査・認証ではありません。

検証の対象

確認した結果

件数・結果の読み方

コールドチェーン
公開モデル・実装

Lean 4.32.1で37命題、実装との768一致命題を確認。Python・JavaScript各272検査、誤った5命題の拒否、署名付き50ケースの観測改変50件の拒否も確認。CI成功。[1][2]

768組＝公開入力192通り×状態4通り。37は定理宣言数であり、独立した新規技術数ではない。

コールドチェーン
既存50ケース
署名付き証拠

事前拒否37件、事後隔離7件、正常・回復5件、検出限界を確認する負の対照1件。署名・記録の対応・集計を再検査。[1][2]

負の対照は、署名付きで整合する虚偽データが通る限界の確認。防御成功には算入しない。

企業間接続
通信・状態
形式検証

実HTTP通信40シナリオ、自動テスト122件を確認。Ubuntu／Windows×Python 3.11／3.13の4ジョブと、Lean 4.19.0必須ジョブの計5ジョブが成功。[3][4]

122件の中に40シナリオを動かす検査を含むため足し算しない。通常通過、拒否・保留、保証境界の確認を含む。

形式証明と実装検査は、別の範囲を確認しています

形式検証は、定めたモデルと前提の下で性質が成り立つことを機械的に検査するものです。コールドチェーンの37命題は7つの抽象条件と2つの状態変数を対象にし、同じ状態を保持する逐次操作での最大1回の模擬作用や、結果不一致を成功確定しない性質等を扱います。768組は公開モデルの全型付き入力・状態の出力照合であり、Python／JavaScript全体の正しさの証明ではありません。[1][2]

企業間接続のLeanモデルでは、取消し後の切替えや二重作用の回避を形式化しています。Lean 4.19.0による検証は、公開GitHub Actionsで成功を確認しています。[3][4]

模擬環境の成果と、本番で必要な確認

コールドチェーンは公開モデルの模擬操作と、別枠の模擬WMSによる保存証拠を扱います。実貨物の出荷、製品別の温度条件、医薬品の品質保証や規制適合を実証したものではありません。事後隔離は、すでに起きた作用を取り消すことではありません。[1]

企業間接続は同一PC上の別プロセス・別DB・別鍵による合成企業の試験です。対象の作用は限定した通知のDB記録であり、実在企業のネットワーク、VPN・ルーター、外部API、実貨物を制御していません。失効しても既発行の有効な許可は実行され得るため、失効と取消し完了を区別します。結果を確定できない間は、切替えを保留します。[3]

「証拠を再検証できる」の意味

署名やハッシュは、記録と鍵・照合基準との対応を確認するもので、元情報の真実性や実世界の事実を自動的に証明しません。50ケースの公開証拠の検査は、署名・観測・集計の対応確認であり、非公開エンジンや非公開原入力の再計算ではありません。信頼する鍵や原本を別経路で固定すること、観測の正しさと実行経路の迂回防止は、実環境への導入時に別途確認します。[1][3]

海外比較と出願について

海外比較は各提供者・著者の一次資料に基づく当社の技術的整理です。公開説明、研究上の形式化、公開実装、商用環境の検証は区別しており、機能不在・性能順位・提携を示しません。政策との対応も政府による認定ではありません。出願番号は国際出願の番号であって登録特許番号ではなく、優先権の主張とその効力・権利範囲は区別します。[9]–[13][15]