The Unfireable Safety Kernel: Execution-Time AI Alignment for AI Agents and Other Escapable AI Systems
作者: Seth Dobrin, Łukasz Chmiel
分类: cs.AI, cs.CR, cs.LG
发布日期: 2026-06-24
备注: Pre-print submitted for publication
💡 一句话要点
提出不可逃避的安全内核以解决AI系统控制问题
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)
关键词: AI安全 执行时对齐 授权机制 不可逃避安全内核 Rust实现 对抗性测试 系统控制
📋 核心要点
- 现有AI系统的控制机制主要依赖于代理的运行时，容易受到输入的影响，导致安全隐患。
- 本文提出不可逃避的安全内核，通过四个关键属性实现架构控制，增强AI系统的安全性。
- 实验表明，该内核在面对逃逸对手时，成功拒绝了704次逃逸尝试，展现出强大的安全防护能力。
📝 摘要（中文）
AI代理被赋予访问工具、API和其他基础设施的权限，使其成为这些系统中的主动主体。现有方法将控制机制置于代理的运行时内部，但这使得任何控制都可能被影响其输入所触及。本文提出了一种新的授权机制，具备四个关键属性，旨在实现架构控制而非合作请求。我们介绍了不可逃避的安全内核（Unfireable Safety Kernel），并通过Rust实现了所有四个属性。实验结果表明，该内核在面对逃逸寻求对手时，成功拒绝了所有安全关键核心的逃逸尝试，展示了其在执行时AI对齐方面的有效性。
🔬 方法详解
问题定义：本文旨在解决现有AI系统控制机制的不足，尤其是代理运行时的控制容易被输入影响的问题。现有方法缺乏有效的架构控制，导致安全隐患。
核心思路：提出不可逃避的安全内核，强调在执行时进行AI对齐，补充训练时和推理时的对齐方法。通过外部化的签名证据和预先行动强制执行，确保系统的安全性和可靠性。
技术框架：该内核的整体架构包括四个主要模块：过程分离、结构性路径上的预行动强制、请求和系统级的失败关闭机制，以及可验证的外部签名证据。
关键创新：最重要的技术创新在于实现了一个机器检查的失败关闭不变性，利用SMT定理（Z3）和全面的有界模型检查证明（Kani）来确保安全性。
关键设计：在实现过程中，Python到Rust的迁移基于字节等价性，确保了1000个测试用例和17个对抗类的成功验证。
🖼️ 关键图片
📊 实验亮点
实验结果显示，在对抗逃逸寻求的对手时，该安全内核成功拒绝了704次对安全关键核心的逃逸尝试，且在6200次授权往返中没有成功的绕过。这表明该内核在执行时AI对齐方面的有效性和可靠性。
🎯 应用场景
该研究的潜在应用领域包括安全关键的AI系统、自动化决策系统和自主机器人等。通过增强AI系统的安全性和控制能力，可以在更广泛的场景中应用AI技术，降低潜在风险，提升系统的可靠性和信任度。
📄 摘要（原文）
AI agents are granted access to tools, APIs, and other infrastructure, making them active principals in those systems. The dominant approach places controls inside the agent's own runtime: system prompts, output filters, and guardrail libraries. Any control in the agent's address space is reachable by inputs that influence it; this generalizes to any AI system with sufficient reach into its own runtime, a class we term escapable AI systems. We identify four properties that an authorization mechanism must satisfy for architectural control rather than for cooperative requests: process separation, pre-action enforcement on a structurally only path, fail-closed at both the request and system levels, and externalized signed evidence verifiable outside the controlled system's trust boundary. We position this layer as execution-time AI alignment, complementing training-time alignment (RLHF, Constitutional AI) and inference-time alignment. We present the Unfireable Safety Kernel, a Rust reference implementation realizing all four. Its fail-closed invariant is machine-checked at two levels: an SMT theorem (Z3) and an exhaustive bounded-model-checking proof of the production decision function (Kani, 4/4 harnesses). A Python-to-Rust migration was gated on byte-equivalence (1000/1000 fixtures; 17/17 adversarial classes). We evaluate the kernel governing a live, escapable AI system, a deterministic, self-improving world model, against an escape-seeking adversary driving its real self-modification seam: across 1,000 self-modifications, all 704 attempts on the safety-critical core are refused, with no escape; a further 300, under the operator kill switch, are also refused. A separate campaign of 6,240 authorization round-trips had no successful bypass. Against 3 contemporary systems claiming the agent control plane, the agent invokes control; here, it lacks that choice.