The Unfireable Safety Kernel: Execution-Time AI Alignment for AI Agents and Other Escapable AI Systems

背景

随着 AI Agent（智能体）技术的演进，AI 系统不再仅仅是被动的文本生成器，而是被授予了对工具、API 以及底层基础设施的访问权限。这种转变使得 AI Agent 成为了这些系统中的“主动主体”（active principals）。

当前业界主流的 AI 安全控制方法，主要依赖于将控制逻辑置于 Agent 自身的运行时环境中。这包括系统提示词（System Prompts）、输出过滤器（Output Filters）以及护栏库（Guardrail Libraries）。然而，这种架构存在一个根本性的安全漏洞：任何位于 Agent 地址空间内的控制机制，都可能被能够影响其输入的外部数据所绕过或操纵。

本文将这类具有足够能力干预自身运行时环境的 AI 系统统称为“可逃逸 AI 系统”（Escapable AI Systems）。传统的对齐方法（如训练时对齐）难以解决运行时动态执行过程中的即时安全威胁，因此需要一种全新的架构级控制机制。

核心内容

本文提出了“不可发射安全内核”（Unfireable Safety Kernel），旨在通过执行时 AI 对齐（Execution-Time AI Alignment）来解决可逃逸 AI 系统的安全问题。该内核并非替代训练时对齐（如 RLHF、Constitutional AI）或推理时对齐，而是作为其必要的补充，专门处理运行时层面的即时授权与执行控制。

架构控制的四大属性

为了实现从“合作请求”到“架构控制”的转变，作者定义了一个授权机制必须满足的四个关键属性：

1. 进程隔离（Process Separation）：安全控制逻辑必须与 AI Agent 的运行环境在进程层面完全分离，确保 Agent 无法直接访问或篡改控制逻辑。
2. 结构性路径上的事前执行强制（Pre-action Enforcement on a Structurally Only Path）：所有操作必须在执行前经过强制检查，且该检查路径在系统结构上是唯一的、不可绕过的。
3. 故障安全（Fail-closed）：无论是在请求层面还是系统层面，一旦检测到异常或验证失败，系统必须默认拒绝执行，而非允许操作继续。
4. 外部化签名证据验证（Externalized Signed Evidence Verifiable Outside the Trust Boundary）：安全决策的证据必须经过签名，并能在受控系统的信任边界之外进行验证，确保证据的完整性和不可否认性。

Unfireable Safety Kernel 的实现

作者使用 Rust 语言实现了一个参考原型（Reference Implementation），该实现严格满足了上述四个属性。为了确保内核的绝对可靠性，作者采用了严格的机器验证方法：

• SMT 定理证明：使用 Z3 求解器对内核的“故障安全”不变量进行形式化验证。
• 有界模型检查：使用 Kani 工具对生产环境中的决策函数进行了穷举式的有界模型检查（4/4 harnesses），确保代码逻辑在所有测试路径下均符合安全规范。

在迁移过程中，从 Python 到 Rust 的重构严格基于字节等价性（Byte-equivalence）进行门控测试，涵盖了 1000/1000 个测试用例以及 17/17 类对抗性场景，确保了行为的一致性。

实验评估

为了验证该内核的有效性，作者在一个实时运行的、具有自我改进能力的确定性世界模型（即一个可逃逸 AI 系统）上进行了评估。攻击者试图利用系统的自我修改接口（self-modification seam）进行逃逸。

实验结果如下：

• 自我修改攻击：在 1,000 次自我修改尝试中，针对安全核心区域的 704 次尝试全部被拒绝，没有任何逃逸成功。
• 操作员强制关闭：另外 300 次尝试在操作员触发“紧急停止开关”（Kill Switch）后，同样被拒绝。
• 授权往返测试：另一项包含 6,240 次授权往返的独立测试活动中，未发现任何成功的绕过案例。

相比之下，当前声称提供 Agent 控制平面的三种主流系统，往往允许 Agent 调用控制逻辑；而在 Unfireable Safety Kernel 的架构中，Agent 根本不具备这种选择权，控制权限被严格剥夺并外置。

关键要点

• 问题定义：AI Agent 因拥有工具访问权而成为主动主体，传统基于 Agent 内部运行时（如 Prompt、Filter）的安全控制存在被输入数据操纵的风险，这类系统被称为“可逃逸 AI 系统”。
• 解决方案定位：提出“执行时 AI 对齐”，作为训练时对齐（RLHF 等）和推理时对齐的补充，专注于架构级的即时控制。
• 四大安全属性：
  1. 进程隔离。
  2. 结构性路径上的事前强制。
  3. 故障安全（Fail-closed）。
  4. 信任边界外的外部化签名验证。
• 技术实现：使用 Rust 编写参考实现，通过 Z3 定理证明和 Kani 有界模型检查进行机器级验证，确保“故障安全”不变量。
• 迁移验证：Python 到 Rust 的迁移通过字节等价性测试（1000/1000 fixtures, 17/17 adversarial classes）保证一致性。
• 实证结果：在对抗性自我修改攻击中，704 次针对安全核心的尝试全部被拒，无逃逸；6,240 次授权测试无成功绕过。
• 范式转变：从“Agent 调用控制”转变为“Agent 缺乏控制选择权”，将控制权从 Agent 地址空间中彻底移除。

意义与影响

这篇论文标志着 AI 安全从“软性约束”向“硬性工程保障”的重要转变。

首先，它揭示了当前主流 AI Agent 安全架构的固有缺陷。只要控制逻辑位于 Agent 的地址空间内，攻击者就有可能通过精心构造的输入来操纵这些控制机制。Unfireable Safety Kernel 通过进程隔离和外部化验证，从根本上切断了 Agent 对安全控制逻辑的直接访问路径。

其次，引入形式化验证（Formal Verification）到 AI 安全工程中具有示范意义。通过 SMT 定理证明和模型检查，作者不仅提供了代码层面的安全，还提供了数学层面的证明。这种“机器检查”的不变量验证，为高可靠性 AI 系统的构建树立了新的标准。

最后，该研究重新定义了 AI 对齐的层次。它表明，仅靠训练数据中的价值观注入（RLHF）是不够的，必须在系统执行层面建立不可逾越的架构屏障。对于未来具备自我修改能力、高自主性的 AI 系统而言，这种“不可发射”的安全内核可能是防止灾难性失控的必要基础设施。