用 lambda 演算证明智能体能抵御提示注入

这是什么？

大多数针对提示注入的防御都是经验性的：一个分类器、一道护栏、一个试图识别恶意输入的过滤器。它们一直有效，直到攻击者找到能绕过它们的措辞。Zac Garby、Andrew D. Gordon 与 David Sands 的一篇论文走了另一条路。该论文于 2026 年 2 月首次发布于 arXiv，并在 2026 年 7 月 13 日以更新版本重新公布。它引入了一种小型形式语言——一套 lambda 演算——用以刻画现代 AI 智能体真正的样子：一段将 LLM 调用、工具调用与后续计算交织在一起、在运行中逐步构建对话的代码。

演算的意义在于可以对其证明性质。作者并不停留在”某种防御大概有帮助”的论断上，而是精确定义智能体程序的含义，然后证明一个关于”哪些输入可以影响哪些输出”的定理。这是一项基础性工作，而非漏洞利用：它为智能体框架的设计者提供了一种严谨的方式，去推理为何一次注入能够、或不能够触及危险操作。

工作原理

核心思想是把 LLM 当作编程语言中一个普通的原语。该演算在无类型 lambda 演算之上扩展出一个调用模型的操作：它将一个值序列化，作为提示发送给 LLM，再把响应解析为一个新的项，供程序继续求值。由于模型的输出以代码和数据的形式重新进入程序，推理与行动之间紧密的耦合被显式化，而不再隐藏在框架内部。

在此之上，该语言增加了两类原语。第一类将对话视为一等对象：可以延展当前对话，fork 出一个不继承既往上下文的全新子对话，或 clear 累积的历史。第二类追踪信息流：项可以被打标签并被查询，因此语义会记录一个值的来源，以及它被允许影响什么。

当对话与标签进入语义之后，通常只是非正式说法的防御就变得精确了。隔离子对话是一个 fork，其不可信内容被隔离，从而无法改写父对话的指令。生成代码的隔离意味着模型产生的输出无法以可信代码的权限执行。而信息流限制从一开始就约束什么能到达一次 LLM 调用：不可信数据可以被读取，但不被允许左右一个特权决策。论文的核心结论是一个对终止不敏感的非干涉定理：在这些限制下，低完整性的输入无法破坏高完整性的输出，机密值也无法泄漏到不应看到它们的通道中。这正是经典信息流安全所追求的完整性与机密性性质，如今被针对智能体对话加以陈述并证明。

为何重要

提示注入之所以顽固，是因为常规防御针对的是字符串——这段文本看起来是否恶意？——而真正的失效关乎权限：不可信数据最终影响了一个可信操作。一套将两者分离的演算，让框架作者能够陈述他们想要的性质（“智能体从网络上读到的任何内容都不能触发付款”），并核验其设计确实强制了这一点，而不必寄望某个过滤器能拦下每一种措辞。

它还提供了一套共同的词汇。各团队各自临时重复发明的模式——双 LLM 拆分、工具输出隔离、能力受限的代码执行——都归结为相同的底层原语：对话 fork 与信息流打标签。能够为它们命名并加以组合，正是把零散的缓解手段变成一种架构的关键，也让两个系统的比较不再仅凭感觉。对于构建编程智能体、RAG 助手与多工具工作流的人而言，其要义是：抗注入可以是一项设计期的保证，而不仅是运行期的补丁。

其局限也应当直说。一个证明只对它所描述的模型成立：定理约束的是用该演算写成的程序，而真实部署只有在其运行时忠实实现这套语义时，才继承相应保证——标签被诚实传播、fork 被真正隔离、生成代码确实被剥夺权限。该演算并不会让 LLM 拒绝一条坏指令；它确保不可信内容永远不会获得发出这条指令所需的地位。

防御建议

以来源而非措辞作为控制点。按来源为数据打标签，并强制不可信来源无法影响特权工具调用，对应论文所形式化的信息流限制。

将不可信的工作 fork 进隔离子对话。当智能体必须读取一个可信度未知的网页、文档或工具结果时，在一个无法改写父对话指令的隔离上下文中处理它，然后只返回一个经过核验的最小结果。

不给生成代码以可信代码的权限。模型产生、而后由你执行的一切，都应以被削减、经显式授予的能力运行——绝不使用智能体宿主的环境权限。

优先选择你能陈述其安全性质的设计。如果你写不出”哪些输入被允许影响哪些操作”，你就无法判断某个过滤器是弥合了缺口，还是仅仅收窄了它。在评审智能体架构时，把该演算的原语——对话隔离与信息流打标签——当作检查清单。

状态

项目	详情
发布	arXiv 预印本，2026 年 2 月；更新版本于 2026 年 7 月 13 日公布
作者	Zac Garby、Andrew D. Gordon、David Sands
性质	形式化基础／防御性研究——无漏洞、无利用代码、无 CVE
关键结论	面向智能体对话的对终止不敏感非干涉定理（完整性 + 机密性）
原语	LLM 调用项；对话管理（延展、fork、clear）；信息流标签
相关场合	哥本哈根大学 COPLAS 讲座