論文の概要: Access Control as Verified Parse Constraints
- arxiv url: http://arxiv.org/abs/2609.12488v1
- Date: Fri, 11 Sep 2026 06:33:41 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-15 07:38:31.643551
- Title: Access Control as Verified Parse Constraints
- Title（参考訳）: 検証Parse制約としてのアクセス制御
- Abstract要約: セキュリティゲートウェイは、ネットワークとポリシー決定の間のコードパスに、繰り返し実装バグを出荷する。
既存のアプローチでは、厳密さを保ったままにするか、差分テストのみで形式的なモデルを手書きのエンジンに接続する。
私たちのコントリビューションはクラスの結果です。フォワードオンリーでバックトラックフリーのEverParseバリデータです。
- 参考スコア（独自算出の注目度）: 2.230473633870735
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Commercial security gateways repeatedly ship implementation bugs in the code path between the network and the policy decision: hand-written enforcement logic that diverges from the policy author's intent, and ad-hoc request parsers at the network boundary that introduce memory-safety flaws of their own. In both cases the bug is in the deployed enforcement code, not in the policy. Existing approaches either leave the enforcement runtime unverified or connect a formal model to a hand-written engine only by differential testing. Our contribution is a class result: a forward-only, backtrack-free EverParse validator is a verified recognizer for a bounded, finite-state class, and access-control decision functions with fixed-offset fields and bounded disjunction belong to it, so one machine-checked proof transfers to every policy in the class rather than being re-established per policy. Concretely, we encode a bounded policy language's decision function into a fixed-size byte buffer and verify the enforcement code once---covering all byte values---with an SMT solver, proving the validator accepts if and only if the decision function accepts, for every policy, request, and session. Editing rule content over a fixed endpoint set then needs no new proof; adding endpoints reruns the toolchain; extending the language needs new proofs. We establish faithful enforcement of a policy, not that a policy is itself secure. The verified gate is platform-independent, requiring only EverParse/Z3 and a C compiler, whose correctness we assume. We demonstrate a deployment on the seL4 microkernel, which ensures every request passes through the gate and that unverified components cannot corrupt the verified enforcement chain.
- Abstract（参考訳）: 商用のセキュリティゲートウェイは、ネットワークとポリシー決定の間のコードパスに、ポリシー作成者の意図から分岐する手書きの強制ロジックと、独自のメモリセーフティ欠陥を導入するネットワークバウンダリにおけるアドホックなリクエストパーサという、繰り返し実装バグを出荷する。
どちらの場合も、バグはポリシーではなく、デプロイされた実行コードにある。
既存のアプローチでは、実行時を未検証のままにするか、差分テストのみで正式なモデルを手書きのエンジンに接続する。
フォワードオンリーでバックトラックフリーのEverParse Validatorは、固定オフセットフィールドとバウンドディジャンクションを持つ、バウンド、有限状態クラス、およびアクセス制御決定関数の認証された認識器であり、そのため、1つのマシンチェックされた証明がポリシーごとに再確立されるのではなく、クラス内のすべてのポリシーに転送される。
具体的には、有界ポリシー言語の決定関数を固定サイズのバイトバッファにエンコードし、一度すべてのバイト値を探索し、SMTソルバで検証し、決定関数が全てのポリシー、要求、セッションに対して受け入れられた場合にのみ、バリケータが受け入れることを示す。
固定されたエンドポイントセットでルール内容を編集すると、新しい証明が不要になり、エンドポイントを追加するとツールチェーンが再実行される。
我々は、政策自体が安全であるということではなく、政策の忠実な執行を確立する。
検証されたゲートはプラットフォームに依存しておらず、EverParse/Z3とCコンパイラしか必要としない。
これにより、すべてのリクエストがゲートを通過し、検証されていないコンポーネントが検証された実行チェーンを破壊できないことが保証される。
関連論文リスト
- PolicyMem: Geometric Policy Memory for LLM Governance [72.04962480384322]
我々は、自然言語ポリシーを再利用可能な幾何学的メモリオブジェクトとして外部化する幾何学的ポリシーメモリであるPhysicalMemを紹介する。
メモリライターは、自然言語ポリシーをポリシーメモリスロットにコンパイルし、クエリ応答ペアはプロジェクションエネルギーを介してポリシーメモリを読み取る。
得られた政策証拠プロファイルは、安全判断を直接仲介し、政策帰属および事後検証のために再利用される。
論文 参考訳（メタデータ） (2026-09-12T06:07:43Z) - LMSM: LLM Security Framework Inspired by Linux Security Modules [56.93644694627783]
大規模言語モデル(LLM)は階層化されたディフェンスでデプロイされることが多いが、悪意のあるプロンプトはそれらをバイパスすることができる。
我々は,Language Model Security Modules (LMSM) という,Linux Security Modules (LSM) の背後にある分離を LLM サービスに適応させるセキュリティフレームワークを提案する。
論文 参考訳（メタデータ） (2026-08-26T12:13:05Z) - Falsifiable Release Gates for Self-Improving Systems [0.0]
本稿では,フェール可能なリリースゲートと,そのようなシステムの構築と検証方法について述べる。
すべての新機能は、出荷前に、指定されたマシン検証可能な受け入れスイートをパスしなければならない。
コントロールリングによってマイニングされる安全クリティカルなプロパティ機能トークンのないエフェクターには、アクションは発生しない。
論文 参考訳（メタデータ） (2026-07-11T06:06:34Z) - AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis [0.2449909275410288]
AutoCedarは、自然言語のアクセス制御要件をレビューされ、チェック可能なターゲットに変換する検証済みのシステムである。
そして、そのターゲットに対するシーダーポリシーを合成する。
論文 参考訳（メタデータ） (2026-07-04T01:13:32Z) - VIGIL: Runtime Enforcement of Behavioral Specifications in AI Agent Skills [13.980239249972819]
VIGILはエージェントシステムのためのエンドツーエンドのランタイム実行フレームワークである。
エージェントの実際の実行トレースを、スキル仕様、オペレータ定義制約、複数のスキルにまたがるグローバルルールから、行動ポリシーに対してチェックする。
95%以上のリコールと偽陽性率で政策違反を検出する。
論文 参考訳（メタデータ） (2026-06-25T01:58:44Z) - LiSA: Lifelong Safety Adaptation via Conservative Policy Induction [45.88278850743155]
ガードレールはもはや単なる回答品質ではなく、秘密を漏らしたり、安全でない行為を許可したり、正当な作業をブロックしたりすることができる。
LiSAは、構造化メモリを通じて固定ベースガードレールを改善する保守的なポリシー誘導フレームワークである。
結局のところ、LiSAは、現実のエッジリスクの予測不可能な長いテールに対して、AIエージェントを保護するための実践的なパスを提供する。
論文 参考訳（メタデータ） (2026-05-14T06:47:35Z) - Skills as Verifiable Artifacts: A Trust Schema and a Biconditional Correctness Criterion for Human-in-the-Loop Agent Runtimes [0.0]
私たちは、スキルが検証されるまで、信頼されたコードであると主張する。
スキル検証がなければ、ループ内の人間ゲートは、あらゆる不可逆呼び出しに発射されなければならない。
すべてのスキルマニフェストに明確な検証レベルを含む信頼スキーマを提供します。
論文 参考訳（メタデータ） (2026-05-01T05:53:05Z) - PolicyBank: Evolving Policy Understanding for LLM Agents [51.86716874651299]
PolicyBankは構造化されたツールレベルの政策洞察を維持し、それらを反復的に洗練する。
PolicyBankは、人間の神託に対するギャップの最大82%を閉じている。
論文 参考訳（メタデータ） (2026-04-16T20:29:30Z) - Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
安全性に整合した大規模言語モデル(LLM)は、現実世界のパイプラインにますますデプロイされている。
敵は通常の評価では動作しないバックドアのチェックポイントを配布することができる。
最近のポストホック重み付け法は、そのようなバックドアを注入するための効率的なアプローチを提供する。
論文 参考訳（メタデータ） (2026-04-14T06:48:33Z) - Verification of Robust Properties for Access Control Policies [51.736723807086385]
既存のアクセス制御ポリシーの検証方法は、検証が進む前に、ポリシーを完全かつ完全に決定する必要がある。
本稿では,政策構造がどのような決定を下すか,どのような決定を下すか,あるいはその後の拡張に拘わらず,その決定を行うかという課題について,ロバストなプロパティ検証を導入する。
可能なすべてのポリシー拡張を普遍的に定量化しているにもかかわらず、判断は二階述語論理プログラミング言語における探索の証明に還元されることを示す。
論文 参考訳（メタデータ） (2026-03-13T17:14:38Z) - Conformal Policy Control [50.46542384484142]
我々は、安全な参照ポリシーを、最適化されているが未試験のポリシーの確率的規制として使う方法を示す。
保守的な最適化方法とは異なり、ユーザーが正しいモデルクラスを識別したとは仮定しない。
自然言語質問応答から生体分子工学まで,本研究の応用実験は,デプロイ開始当初から安全な探索が可能であることを示唆している。
論文 参考訳（メタデータ） (2026-03-02T18:54:36Z) - QuadSentinel: Sequent Safety for Machine-Checkable Control in Multi-agent Systems [22.833567409552074]
textscQuadSentinelは、安全ポリシーをマシンチェック可能なルールにコンパイルする4エージェントガードである。
textscQuadSentinelは偽陽性を減らしながらガードレールの精度とルールリコールを改善する。
論文 参考訳（メタデータ） (2025-12-18T07:58:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。