不可焚毁的安全内核：面向AI智能体及其他可逃逸AI系统的运行时人工智能对齐技术
The Unfireable Safety Kernel: Execution-Time AI Alignment for AI Agents and Other Escapable AI Systems
Seth Dobrin, Lukasz Chmiel
arXiv (Cornell University) · 2026-06-24
摘要
AI智能体被赋予访问工具、应用程序接口及其他基础设施的权限，因而成为这些系统中的主动主体。当前主流的解决方案是将控制机制嵌入智能体的运行时环境，包括系统提示词、输出过滤器以及防护库。然而，位于智能体地址空间内的任何控制措施都可能被能够影响其运行的输入所突破；这一规律同样适用于所有能够深度介入自身运行时的AI系统，我们将此类系统称为可逃逸AI系统。为了实现架构层面的有效控制而非依赖协作式请求，我们总结出授权机制必须满足的四项特性：进程隔离、在结构化必经路径上实施事前强制约束、在请求层面与系统层面均采取失效封闭原则，以及生成可在受控系统信任边界之外验证的外部签名证据。我们将这一层级的技术定位为运行时人工智能对齐，以此补充训练阶段的对齐技术（如强化学习微调、宪法性人工智能）与推理阶段的对齐技术。我们提出了不可焚毁的安全内核，这是用Rust语言编写的参考实现，满足了上述四项要求。其失效封闭特性通过两个层面得到机器验证：一是利用Z3求解器进行的SMT定理证明，二是对生产环境中的决策函数进行的穷尽有界模型检测（采用Kani工具，覆盖全部4种测试场景）。该内核的Python到Rust迁移过程以字节级等价性为判定标准（1000个测试用例全部通过；17类对抗性样本无一例外）。我们对该内核在实时可逃逸AI系统中的应用效果进行了测试，该系统是一个具备自我改进能力的确定性世界模型；面对试图利用其自我修改机制进行逃逸的对手，在1000次自我修改尝试中，针对安全关键核心的704次攻击均被阻断，未能实现逃逸；在操作员手动触发终止开关的情况下，后续的300次攻击同样被阻止。另外一轮包含6240次授权请求的测试中，也未出现任何成功绕过的情况。针对3种宣称拥有智能体控制权的现有系统，智能体能够主动调用控制功能；而在该内核框架下，智能体则丧失了这种选择权。
本摘要由 AI（Hy-MT2-Pro）翻译生成，仅供参考，请以原文为准。
AI 综述
基于摘要生成- 主要观点
- 论文把当前主流的代理管控范式——系统提示词、输出过滤器、护栏库——归为置于代理自身运行时之内的内部控制，并提出其结构性缺陷：凡位于代理地址空间内的控制，都可被影响该代理的输入所触及。该论断被推广至一切对自身运行时具有足够可达性的 AI 系统，作者命名为「可逃逸 AI 系统」（escapable AI systems）。据此，作者主张授权机制必须满足四项属性：进程分离；在结构性唯一路径上做事前执行；在请求级与系统级同时 fail-closed；以及可在受控系统信任边界之外验证的外置签名证据。作者将该层次定位为「执行时对齐」（execution-time AI alignment），与训练时对齐（RLHF、Constitutional AI）和推理时对齐并列且互补。作为论点的实现与验证，论文给出 Unfireable Safety Kernel 这一 Rust 参考实现，并以「代理调用控制」与「代理无从选择」的对比，区分本文方案与三种声称占据代理控制平面的当代系统。
- 研究方法
- 研究采取属性推导、参考实现、机器验证与对抗评测依次推进的路径：先从内部控制的可达性论证导出四项必要属性，再以 Rust 实现该内核。形式化检验环节在两层上验证 fail-closed 不变式：一层是以 Z3 求解的 SMT 定理，另一层是以 Kani 对生产决策函数做穷尽式有界模型检验（4/4 个 harness 通过）。工程迁移环节以字节等价作为放行门槛，覆盖 1000/1000 条 fixture 与 17/17 个对抗类别。实证环节在一个处于运行状态的可逃逸 AI 系统上展开；该系统是确定性的、自我改进的世界模型，由内核进行治理，并由搜寻逃逸的对抗者驱动该系统真实的自我修改接缝：在 1000 次自我修改中，针对安全关键内核的 704 次尝试全部被拒绝；另有 300 次在操作员 kill switch 之下也被拒绝；还另设 6240 次授权往返的独立评测轮次（campaign），未出现成功绕过。
- 学术贡献
- 概念层面，论文提出「可逃逸 AI 系统」这一类别，并为架构性控制（相对于请求性和协作性控制）给出四条可判定的属性判据，把 AI 安全中的控制问题从策略配置问题重新表述为运行时权限架构问题。层次划分层面，论文将执行时对齐确立为独立于训练时对齐与推理时对齐的第三层，为对齐技术图谱补入一个此前由提示词与护栏近似替代的位置。方法层面，论文把 SMT 定理证明与有界模型检验组合用于生产决策函数的 fail-closed 不变式，并以字节等价 fixture 与对抗类别作为语言迁移的放行条件，为安全关键组件的重构提供可复用的验证流水线。材料与实证层面，作者在真实自我修改接缝上以对抗者驱动的方式取得可计数的拒绝记录（704/704、300、6240 次无绕过），这类来自活跃的可逃逸系统的数据在代理控制议题中尚不常见。上述贡献对 AI 代理权限架构、对齐技术分层以及形式化验证在安全工程中的实施这三个子议题具有直接价值。
- 存在局限
- 评测对象仅为一个确定性的、自我改进的世界模型；确定性使自我修改接缝的状态空间与可枚举性显著低于以自然语言为接口的随机性 LLM 代理，因此把结论外推到此类系统缺乏材料支持。对抗者由作者自行设计，威胁模型覆盖以 17 个对抗类别为界，论文未说明该类别集合的完备性依据，也未报告未被覆盖的逃逸路径（如工具链、供应链或签名证据验证者本身被攻破）。与三种当代系统的比较在摘要中仅以「代理调用控制」与「代理无从选择」的定性表述给出，未提供对照实验的指标与配置，材料中未明确提及比较所用的具体基准。1000 次自我修改与 6240 次授权往返的规模虽可计数，但未报告失败模式的分布、延迟与吞吐开销，也未涉及操作员误用或 kill switch 本身被绕过的情形。四项属性系由可达性论证推导而来，论文未对其做消融，因而无法判断四者中哪一项在实证中真正承载了安全性。
- 进一步研究方向
- 其一，将同一逃逸搜寻对抗评测轮次迁移到以随机性 LLM 为决策核心的代理 harness 上，保留相同的自我修改接缝与 kill switch 配置，检验 fail-closed 在非确定性下是否仍成立，并统计拒绝率与误拒率。其二，对四项属性逐一做消融实验：分别移除进程分离、事前单路径执行、双级 fail-closed 与外置签名证据，测量各条件下 6240 次量级授权往返中的绕过数，以确定属性的负载权重。其三，将四项属性形式化为独立的机器可检验规约，并证明 Rust 实现与该规约之间的精化关系，把当前的 Kani harness 从决策函数层扩展到进程边界与证据签名层。其四，引入独立于作者的第二方验证者来验证外置签名证据，测量跨信任边界的验证开销与证据链失效模式。其五，扩大自我修改评测轮次的规模并公开失败样本，用以检验 704/704 的拒绝记录在更长运行与更强对抗者下的稳定性。
本综述由 AI（deepseek-flash）基于摘要自动生成，仅供参考，不代表原文作者观点，请以原文为准。
参考文献
相关论文
话题：Security and Verification in Computing