論文の概要: 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ベースのフロンティアモデルサンドボックスインフラストラクチャの事前デプロイ検証
• Authors: Dominik Blain,
• 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算術の定式化と整合性を持ち、事前展開形式解析は関連するパターンを克服できるであろうと論じる。 フロンティアモデルの安全性は、行動保護のみに依存することはできない;封じ込めスタック自体が正式な検証を受けなければならない。

関連論文リスト

• 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)

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

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