論文の概要: Mythos and the Unverified Cage: Z3-Based Pre-Deployment Verification for Frontier-Model Sandbox Infrastructure

• arxiv url: http://arxiv.org/abs/2604.20496v1
• Date: Wed, 22 Apr 2026 12:28:23 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-23 15:36:11.124954
• Title: Mythos and the Unverified Cage: Z3-Based Pre-Deployment Verification for Frontier-Model Sandbox Infrastructure
• Title（参考訳）: Mythos and the Unverified Cage: Z3ベースのフロンティアモデルサンドボックスインフラストラクチャの事前デプロイ検証
• Abstract要約: 一部の二次アカウントはサンドボックスネットワークコードにCWE-190算術的脆弱性を仮定している。 本稿では,C/C++ インフラストラクチャにおける CWE-190/191/195 の算術的脆弱性パターンを,Z3 SMT ベースの形式検証エンジンである COBALT について述べる。 提案する: COBALT, VERDICT, DIRECTIVE-4, SENTINEL, 事前デプロイ検証, 事前実行制約, 出力制御, 実行時の監視をMythosインシデントによって公開された障害モードにマッピングする4層封じ込めフレームワーク。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The April 2026 Claude Mythos sandbox escape exposed a critical weakness in frontier AI containment: the infrastructure surrounding advanced models remains susceptible to formally characterizable arithmetic vulnerabilities. Anthropic has not publicly characterized the escape vector; some secondary accounts hypothesize a CWE-190 arithmetic vulnerability in sandbox networking code. We treat this as unverified and analyze the vulnerability class rather than the specific escape. This paper presents COBALT, a Z3 SMT-based formal verification engine for identifying CWE-190/191/195 arithmetic vulnerability patterns in C/C++ infrastructure prior to deployment. We distinguish two classes of contribution. Validated: COBALT detects arithmetic vulnerability patterns in production codebases, producing SAT verdicts with concrete witnesses and UNSAT guarantees under explicit safety bounds. We demonstrate this on four production case studies: NASA cFE, wolfSSL, Eclipse Mosquitto, and NASA F Prime, with reproducible encodings, verified solver output, and acknowledged security outcomes. Proposed: a four-layer containment framework consisting of COBALT, VERDICT, DIRECTIVE-4, and SENTINEL, mapping pre-deployment verification, pre-execution constraints, output control, and runtime monitoring to the failure modes exposed by the Mythos incident. Under explicit assumptions, we further argue that the publicly reported Mythos escape class is consistent with a Z3-expressible CWE-190 arithmetic formulation and that pre-deployment formal analysis would have been capable of surfacing the relevant pattern. The broader claim is infrastructural: frontier-model safety cannot depend on behavioral safeguards alone; the containment stack itself must be subjected to formal verification.
• Abstract（参考訳）: 2026年4月のClaude Mythosのサンドボックスエスケープは、フロンティアAI封じ込めの重大な弱点を露呈した。 セカンダリアカウントの中には、サンドボックスネットワークコードのCWE-190算術的脆弱性を仮定するものもある。 これは、特定のエスケープではなく、未検証で脆弱性クラスを分析します。 本稿では,C/C++ インフラストラクチャにおける CWE-190/191/195 の算術的脆弱性パターンを,Z3 SMT ベースの形式検証エンジンである COBALT を提案する。 私たちは2つの貢献のクラスを区別する。 検証: COBALTは実運用コードベースの算術的脆弱性パターンを検出し、具体的な証人によるSATの検証と、明示的な安全性境界の下でUNSATの保証を生成する。 NASA cFE, wolfSSL, Eclipse Mosquitto, NASA F Primeの4つのプロダクションケーススタディでこれを実証した。 提案する: COBALT, VERDICT, DIRECTIVE-4, SENTINEL, 事前デプロイ検証, 事前実行制約, 出力制御, 実行時の監視をMythosインシデントによって公開された障害モードにマッピングする4層封じ込めフレームワーク。 明示的な仮定の下では、MythosエスケープクラスはZ3で表現可能なCWE-190算術の定式化と整合性を持ち、事前展開形式解析は関連するパターンを克服できるであろうと論じる。 フロンティアモデルの安全性は、行動保護のみに依存することはできない;封じ込めスタック自体が正式な検証を受けなければならない。

関連論文リスト

• Evaluating the NIST Bugs Framework Against CWE as a Successor for Automated Vulnerability Classification [8.57966523475548]
  Bugs Framework(BF)は脆弱性を原因、操作、結果の3倍に整理し、そのような3倍を因果連鎖にリンクする。 我々は,BFがCWE(Common Weaknession)よりも構造化され,自動化に優しいフレームワークであるという主張を評価する。 我々の調査では、可用性に関する詳細なガイダンスを含め、BFの特定のギャップが明らかになっている。
  論文  参考訳（メタデータ） (2026-09-14T23:18:46Z)
• AI Slop and Hallucinations in Vulnerability Assessment: A Survey on Reasoning Failures and Trustworthy Mitigation [48.55515767840701]
  AIスロープ(AI slop)は、アーティファクト、幻覚的脆弱性、可視だが正しくないパッチ、セマンティックに再パッケージされたバグレポートである。 本稿では,実証的証拠を調査し,統一メカニズムを特定し,信頼に値するトリアージへの道筋をたどる。
  論文  参考訳（メタデータ） (2026-08-26T11:48:38Z)
• CyberFactory: Scaling Cyber Security Capabilities with Instances from the Wild [49.44069582581181]
  CyberFactoryは、CVEを含む公開脆弱性アーティファクトをワイルドから実行可能で検証可能なタスクインスタンスに変換する。 再利用可能な脆弱性分析スキルを使用して、ソースインスペクション、ドメイン前の問題解決、エビデンスベースのバリデーションを通じて教師を指導する。 CyberGymでは1時間の予算で52.4%のPass@1に達し、Qwen3.5ベースモデルを+22.8ポイント改善した。
  論文  参考訳（メタデータ） (2026-08-24T12:30:10Z)
• SafeCA: Safe Cross-Attention Localization and Regulation for Text-to-Video Jailbreak Defense [77.70598852234149]
  テキスト・トゥ・ビデオ(T2V)生成モデルは、現実世界のデプロイにおいてジェイルブレイク攻撃に対して脆弱である。 安全なクロスアテンション・ローカライゼーションと正規化のための機能レベル防衛機構であるSafeCAを提案する。 実験の結果、SafeCAは主流のT2Vモデルでジェイルブレイクの成功率を約20%削減することが示された。
  論文  参考訳（メタデータ） (2026-08-11T14:01:24Z)
• Crushing the Evidence: A Dual-Penalty Evasion Framework for Fooling White-Box Explainable AI Auditors [4.377640147713394]
  ポストホックモデルの説明器は、高感度ドメインのモデルを監査するために広くデプロイされている。 説明可能性パイプラインにおける潜在的な攻撃について、いくつかの研究がなされている。 より強力なホワイトボックス、勾配調整型回避攻撃フレームワークを導入する。
  論文  参考訳（メタデータ） (2026-08-01T10:03:14Z)
• Routing Ceilings Are Domain-Independent: Structural Prior Injection in Code Security Vulnerability Detection [0.0]
  大規模言語モデル(LLM)は、潜在能力と一貫したアクティベーションの間に、十分に文書化されたギャップを示す。 以前の報告では、構造的事前は分配性能を劇的に向上させるが、ゼロショットベースラインのアウト・オブ・ディストリビューション以下に崩壊する。 我々は、ソースコードの脆弱性検出においてSAIR設計を再現することにより、この現象がクロスドメインであるかどうかを検証する。
  論文  参考訳（メタデータ） (2026-07-16T06:45:08Z)
• Understanding and Mitigating Prompt Leaking Attacks in Real-World LLM-Based Applications [57.33208520608409]
  本稿では,大規模言語モデル(LLM)に基づくアプリケーションにおいて,プロンプトリークのシステマティックスタディを提案する。 デプロイの80%以上は、現実的な逆クエリの下で、システムにリークする。 我々は、最適化可能なソフトプロンプトを用いてモデルの注意を喚起する実用的な防御であるARAを提案する。
  論文  参考訳（メタデータ） (2026-06-17T04:20:00Z)
• MOSAIC-Bench: Measuring Compositional Vulnerability Induction in Coding Agents [2.1942030377331245]
  コーディングエージェントは、しばしばプロンプト毎の安全性レビューをパスするが、それらのタスクが通常のエンジニアリングチケットに分解されると、悪用可能なコードを出荷する。 199個の3段階攻撃チェーンのベンチマークであるMOSAIC-Benchを紹介する。 9つのプロダクションコーディングエージェントが53～86%の終末ASRで無害なチケットを構成しており、全ステージで2回しか拒否しないことを示す。
  論文  参考訳（メタデータ） (2026-05-05T16:38:23Z)
• Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
  安全性に整合した大規模言語モデル(LLM)は、現実世界のパイプラインにますますデプロイされている。 敵は通常の評価では動作しないバックドアのチェックポイントを配布することができる。 最近のポストホック重み付け法は、そのようなバックドアを注入するための効率的なアプローチを提供する。
  論文  参考訳（メタデータ） (2026-04-14T06:48:33Z)
• The Compliance Paradox: Semantic-Instruction Decoupling in Automated Academic Code Evaluation [11.984098021215878]
  SPACI(Semantic-Preserving Adrial Code Injection)フレームワークとAST-ASIP(Abstract Syntax Tree-Aware Semantic Injection Protocol)を紹介する。 これらの方法は、抽象構文木(英語版)の構文的に不活性な領域(トリヴィアノード)に逆方向の指示を埋め込むことにより、構文解析ギャップを利用する。 Python、C、C++、Javaの25,000のサブミッションにまたがる9つのSOTAモデルの大規模な評価を通じて、DeepSeek-V3のような高容量オープンウェイトモデルにおいて、破滅的な失敗率(>95%)を明らかにします。
  論文  参考訳（メタデータ） (2026-01-29T07:40:58Z)
• Why Does the LLM Stop Computing: An Empirical Study of User-Reported Failures in Open-Source LLMs [50.075587392477935]
  オープンソースのDeepSeek、Llama、Qwenのエコシステムから、705の現実世界の失敗に関する大規模な実証的研究を行った。 ホワイトボックスオーケストレーションは、モデルアルゴリズムの欠陥からデプロイメントスタックのシステム的脆弱性へと、信頼性のボトルネックを移動させます。
  論文  参考訳（メタデータ） (2026-01-20T06:42:56Z)
• The Trojan Knowledge: Bypassing Commercial LLM Guardrails via Harmless Prompt Weaving and Adaptive Tree Search [58.8834056209347]
  大規模言語モデル(LLM)は、有害な出力を誘導するために安全ガードレールをバイパスするジェイルブレイク攻撃に弱いままである。 CKA-Agent(Correlated Knowledge Attack Agent)は、ターゲットモデルの知識基盤の適応的木構造探索としてジェイルブレイクを再構成する動的フレームワークである。
  論文  参考訳（メタデータ） (2025-12-01T07:05:23Z)
• ARMOR: Aligning Secure and Safe Large Language Models via Meticulous Reasoning [64.32925552574115]
  ARMORは、jailbreak戦略を分析し、コアインテントを抽出する、大規模な言語モデルである。 ARMORは最先端の安全性能を達成し、平均有害率は0.002であり、高度な最適化ベースのジェイルブレイクに対する攻撃成功率は0.06である。
  論文  参考訳（メタデータ） (2025-07-14T09:05:54Z)
• AdversariaL attacK sAfety aLIgnment(ALKALI): Safeguarding LLMs through GRACE: Geometric Representation-Aware Contrastive Enhancement- Introducing Adversarial Vulnerability Quality Index (AVQI) [21.209413521884297]
  LLMに対する敵の脅威は、現在の防衛が適応できるよりも急速にエスカレートしている。 ALKALIは, 厳格にキュレートされた最初の逆数ベンチマークである。 本稿では、遅延空間正規化と協調するアライメントフレームワークGRACEを紹介する。
  論文  参考訳（メタデータ） (2025-06-10T15:14:17Z)
• CRAFT: Characterizing and Root-Causing Fault Injection Threats at Pre-Silicon [3.6158033114580674]
  フォールトインジェクション攻撃は組み込みシステムに重大なセキュリティ脅威をもたらす。 物理的欠陥がシステムレベルの行動にどのように伝播するかの早期発見と理解は、サイバーインフラ構造を保護するために不可欠である。 この研究は、プレシリコン分析とポストシリコンバリデーションを組み合わせたフレームワークであるCRAFTを導入し、障害インジェクションの脆弱性を体系的に発見し分析する。
  論文  参考訳（メタデータ） (2025-03-05T20:17:46Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。 RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。 これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。 我々は、無害な」知識基盤の著作権保護の名称を提案する。
  論文  参考訳（メタデータ） (2025-02-10T09:15:56Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。