LLMbda 演算：AI 智能体、对话与信息流

核心问题：如何为 LLM 智能体提供一种既表达力强、又可证明 sound 的 prompt injection 防御，而不把某种固定架构（如 dual-LLM）烘焙进框架。

• 场景与重要性：LLM 智能体规划、调工具、读取不可信数据并据此行动，作者称这使其暴露于 prompt injection——只应被读取的数据被当作指令执行。基于内容检查的防御（分类器、问模型输入是否像攻击）是军备竞赛，作者认为其保证不了任何东西。
• 现有方法的不足：作者指出 provenance 路线（dual-LLM 职责分离 + IFC）有三个困难：IFC 在边界处易错（文中给出 CaMeL 的两个泄漏例子：不更新未走分支标签的经典泄漏、未跟踪的 Python retry 循环把终止比特迭代成完整秘密）；刻意放松的跟踪（如 FIDES 不跟踪数据依赖控制流、留小域值逃生口）难以审计；CaMeL 与 FIDES 都把 dual-LLM 拆分硬编码进架构，且 CaMeL 无可比的 soundness 定理。
• 核心观察：作者认为 dual-LLM 的隔离保证可被 IFC 保证涵盖——只要 forking、clearing、prompting 等会话机制成为可编程原语，隔离就变成程序表达的策略，而非框架强加的形状。
• 论文提出什么：LLMbda 演算（会话、代码生成、动态 IFC 为一等构造）、全演算的 TIPNI 与 Insulated TIPNI 定理（Lean 4 机械化）、被机器检查定理覆盖的可执行解释器，以及在 AgentDojo banking 上评测的 Randori 智能体。
• 威胁模型：
  • 攻击者目标：通过不可信数据注入指令，让智能体执行非预期动作（如发送邮件、转账）。
  • 攻击者知识/能力：控制不可信输入；Insulated TIPNI 在攻击者选择所有不可信输入时仍成立（作者称）。
  • 受害系统：调用工具、维护 prompt-response 会话的 LLM 智能体。
  • 防御方假设：按来源给数据打标签（trusted/untrusted、secret），工具库开发者在敏感汇点放置标签检查。

基于信息流的注入防御

• CaMeL [20]——dual-LLM 的细化，特权模型生成并运行代码；论文批评其 IFC 子语言存在两处泄漏（§1），且无可比的 soundness 定理，CaMeL 作者自己称形式化是"crucial direction"。
• FIDES [18]——结合职责分离与 IFC；论文指出其刻意不跟踪数据依赖控制流，并提供小域值逃生口，其机密性保证是 taint-tracking（explicit secrecy [58]）。
• Wu et al. [75]、Kim et al. [37]、Li et al. [42]——分别为固定系统架构证明非干扰、动态跟踪不可信源、静态分析输出计划语言。

语言化 IFC 基础

• Austin and Flanagan [7, 8]——纯动态信息流与 labelled lambda 演算，本文的标签机制最接近此；论文指出 [7] 的标签测试只对两点格证明非干扰，且其测试语义只适用于两点格。
• Bichhawat et al. [10]——达到任意格但省略测试；LIO [15, 63, 66]——标签为一等值；Zheng and Myers [79]、Tse and Zdancewic [64]——运行时计算的标签/主体。
• Hunt, Sands and Stucki [34]——把域论信息流性质弱化为终止不敏感版本的通用配方，本文据此定义 TIPNI；Smith and Alpízar [61] 与 Unruh [65] 提出了与 TIPNI 等价的性质。

LLM 的演算与概率编程

• OPAL [46]、Quasar [47]——面向 LLM 的 lambda 演算语言，论文指出两者都不处理 prompt injection 或非干扰。
• Zar [9]、Borgström et al. [13]、Kozen [39]、Wand et al. [68]——概率程序的验证采样器与语义对应，Theorem 3 与之同类但直接陈述为测度等式。

Lean 中的 LLM 工具与其他防御

• Lean Copilot [62]、LLMstep [70]、LeanAide [25]——调用 LLM 辅助证明开发，未对 harness 证明任何性质；Lean4Agent [69] 验证工作流的 Hoare 式前后条件，但智能体在 Lean 之外运行。
• LBAC/TypeGuard [80]（Haskell 类型检查能力）与 tacit [50]（Scala 3 捕获检查）——同期类型化 harness；论文在 §7.3 与其比较评测结果。Spotlighting [33]、Task Shield [35]——非 IFC 的注入防御。

基线与基准：对比基线是 CaMeL（作者重跑，分 policy 开/关两种设置），基准为 AgentDojo [21] 的 banking 套件。

作者定位：LLMbda 是作者所称首个可执行文件本身是机器检查安全定理对象的 LLM 智能体 harness，其保证是覆盖全演算（含代码生成智能体）的元定理，而非绑定某个固定规划器形状。

整体思路：把智能体系统的操作核心做成一个无类型 call-by-value lambda 演算 LLMbda 的一等构造，每个值携带标签、每条归约规则传播标签；隔离成为程序表达的策略，重分类（endorse）成为显式可审计的构造；全部语义与定理在 Lean 4 中机械化。

会话与代码生成

• 状态是与 LLM 的会话（消息列表）；send e 把序列化后的提示追加到会话，recv 按当前会话从模型采样响应并解析为表达式继续求值；派生形式 @e ≜ (λ_. recv) (send e)。
• fork e 在会话的临时副本上求值再丢弃，clear 清空会话；二者让 dual-LLM 式隔离成为可编程策略（如 prelude 函数 quarantine 在 fork+clear 的子会话中处理不可信内容）。
• 代码生成：响应可被解析为 lambda 抽象并执行；§2 给出带语法提示与重试的生成循环示例。

标签与动态 IFC

• 标签取自 join-半格（⊔、⊑、⊤、⊥），示例用 {U, S} 幂集四点格；值默认标 ⊥（parsimonious 原则），会话状态标签为所有已发消息的上界。
• 原语：静态/动态标签表达式 l:e 与 e1:e2、测试 e1?e2、断言 assert e1 e2（违反时求值卡住，解释器报运行时错误）。
• 标签测试把结果返回到 pc⊔l（被测策略标签）而非数据自身标签，作者称这使测试非干扰；对比 [7] 返回到裸 pc、只对两点格 sound。
• 概率大步语义 pc \vdash C, e \Downarrow C', V \triangleright w, s：消耗采样轨迹 s、联合概率 w；Confinement（Lemma 1）保证 pc 不高于结果标签。

TIPNI 与证明技术

• 不可区分性 ∼n：对只能看到标签 ⊑ n 的观察者相同；配置的指称是终态上的子分布，缺失质量即不终止概率。
• TIPNI 定义：\mathrm{TIPNI}(m) \triangleq C_0 \sim_m C_1 \land e_0 \sim_m e_1 \Rightarrow \llbracket pc \vdash C_0, e_0 \rrbracket_m \smile \llbracket pc \vdash C_1, e_1 \rrbracket_m，即 ∼m 相关输入产生兼容（存在共同支配子分布）的 m 观察者指称；由 [34] 的通用配方导出。
• 性质：确定性时与 TINI 重合（Lemma 3）、总终止时与 PNI 重合（Lemma 4）、泄漏以平均不终止概率为界（Lemma 5）；作者指出其与 [61]、[65] 的已有性质等价。
• 证明技术（作者称其为贡献）：定义 m-skipping 语义 ⇓♯，标签变高（̸⊑ m）时短路返回哑值 {}；靠 stripping（支配原语义）、high-blindness（对 ∼m 输入返回相同分布）、sub-distribution 三个机械化引理构造见证 ω。完整规则集 76 条在 Lean 开发中。

Endorse 与 Insulated TIPNI

• endorse e1 e2 把 e2 的完整性轴重分类到 e1 指定标签；格因子化为完整性 × 机密性两维（L ≅ I × S），弱化只限所选维。
• Insulated TIPNI（Theorem 2）：对 I-maximal 观察者（忽略完整性轴）TIPNI 成立——作者称即攻击者选择所有不可信输入、endorse 任意重分类，机密性保证都不受影响。
• 附录 E 给出两种不改语义的约束变体：robust_endorse（endorsed 比特阻断级联）与 bounded_endorse（小域，至多 log2 n 比特）；作者称形式化定量界留作未来工作。

实现与评测方式

• 解释器 peval 是 Lean 中 fuel 传递的纯函数，由 oracle 提供每次 recv 的响应；真实运行时 oracle 经 unsafe 实现发 HTTP 请求，对证明而言只是被全称量化的某个 oracle。
• Theorem 3（oracular correctness）：先采样 oracle 再跑确定性解释器所得分布等于 §3 的指称语义（假设响应按 M.weight 分布、总质量为 1）。
• Randori 智能体：dual-LLM 架构，P-LLM 生成代码、Q-LLM 隔离处理不可信数据；randori 练习阶段先在 mock 状态上跑修复循环（工具响应始终可信），再生成最终代码在真实世界执行；允许代码生成阶段预先 endorse 特定数据流。

实验设置

• 被测模型：GPT-5.2、Qwen3.7-plus、MiMo-v2.5 三个，同一模型同时承担代码生成（P-LLM）与隔离 Q-LLM 角色。
• 基准：AgentDojo banking 套件，16 个 user tasks × 9 个注入攻击 = 144 个任务/攻击对，每对重复 k = 3 次。
• 基线：作者重跑的 CaMeL，分 (no policy)（关策略检查）与 (with policy)（开策略检查）两行，只在 GPT-5.2 与 MiMo-v2.5 两个模型上跑。
• 指标：Utility（正确完成的用户任务比例，分 Safe/Attacked 两列，95% Student-t 置信区间、以任务或任务/攻击对为采样单位）；Security（成功击退攻击的对数，按 Category A/B 分层，95% Wilson score 区间）。
• Category 划分：Category A（97/144）是攻击所需工具调用本就不会出现在生成代码中的情形；Category B（47/144）是生成计划足以让攻击成功的其余情形。
• 消融：Randori (no endorse) 撤销 endorse 能力；所有 Randori 行 IFC enforcement 始终开启。

主结果

据 Table 1（AgentDojo banking，16 tasks × 9 attacks，k = 3）：

表格较宽，可左右滑动

系统	模型	Utility Safe	Utility Attacked	Security Cat. A	Security Cat. B
Randori	GPT-5.2	36/48 (75% ± 18.9)	281/432 (65% ± 6.7)	291/291 [96.2, 100]	139/141 [90, 99.8]
Randori	Qwen3.7-plus	36/48 (75% ± 20.0)	274/432 (63.4% ± 6.8)	291/291 [96.2, 100]	141/141 [92.4, 100]
Randori	MiMo-v2.5	31/48 (64.6% ± 22.0)	257/432 (59.5% ± 6.2)	291/291 [96.2, 100]	141/141 [92.4, 100]
Randori (no endorse)	Qwen3.7-plus	30/48 (62.5% ± 24.2)	260/432 (60.2% ± 7.2)	291/291 [96.2, 100]	141/141 [92.4, 100]
Randori (no endorse)	MiMo-v2.5	26/48 (54.2% ± 23.3)	243/432 (56.2% ± 6.8)	291/291 [96.2, 100]	141/141 [92.4, 100]
CaMeL (no policy)	GPT-5.2	32/48 (66.7% ± 23.4)	96/135 (71.1% ± 7.7)	98/99 [94.4, 99.8]	141/141 [92.4, 100]
CaMeL (no policy)	MiMo-v2.5	34/48 (70.8% ± 21.4)	104/144 (72.2% ± 7.4)	240/241 [95.3, 99.9]	138/141 [88.9, 99.6]
CaMeL (with policy)	GPT-5.2	18/48 (37.5% ± 26.6)	70/233 (30% ± 8.1)	97/97 [96.1, 100]	134/134 [92.4, 100]

• 作者称：Randori（策略常开）的 utility 与 CaMeL (no policy) 在置信区间内相当，约为 CaMeL (with policy)（37.5%）的两倍；表注称 CaMeL 部分受攻击/安全运行未完成，其格子只计已完成运行。
• 作者称 Randori 在 1296 次受攻击运行中仅 2 次被攻破（均为 GPT-5.2 下同一任务/攻击对的 Category B 运行）；作者认为该攻击是语义性的、超出 IFC 防御范围，且不用 endorse 时会被挡住。
• 作者指出 CaMeL (no policy) 在 GPT-5.2 上有 2 次 Category A 失守：task 12 中智能体实现了"解释器循环"，在无策略检查时让攻击者绕过 dual-LLM 模式。

与同期系统的安全-效用权衡对比

• 作者引用 TypeGuard（LBAC 的 Haskell 实现）在 AgentDojo slack 套件的结果：启用策略后 utility 从 15/21 降到 8/21（38.1%），同条件下 CaMeL 为 7/21；作者称这与 CaMeL 的效用下降模式相同。
• 作者引用同期报告：TypeGuard 击退全部 105 个 slack 注入对，tacit 在四个 stock 套件、两个模型的 2 × 963 次试验中仅 1 次失败；论文脚注说明跨论文数字仅供参考（套件、模型、攻击集、重复次数都不同）。
• 作者认为其 Category A/B 分解显示 banking 对中约三分之二靠"先规划后暴露"的架构即可击退，并指出 TypeGuard 与 tacit 刻意放弃代码/数据分离，每个任务-攻击对实际上都落在 Category B。

失效案例与消融解读

• 两次成功攻击：任务要求读文件并按内容付款，注入把文件内容换成恶意付款请求；作者称这属于语义攻击，IFC 层面唯一的挡法是不加区分地阻止任何不可信文件内容被"洗白"。
• (no endorse) 消融：utility 下降（见表），作者称这印证 endorse 对某些任务必要——tasks 0、2、12 要求读不可信文件并执行断言信任的动作；作者同时称恢复 endorse 以 Category B 安全的可控代价换回这些任务。
• Randori 的劣势：作者指出 LLMbda 语法全新、不在训练数据中，且缺少原生错误处理，许多运行时错误无法被 monadic 安全版本捕获，信息流错误在 randori 阶段不被抛出。

其他消融与分析

• CaMeL 论文自身的两次成功注入中，一次是同一文档导向付款案例（CaMeL 置于威胁模型外），另一次是 travel 套件中逐字引用酒店评论触发 AgentDojo 字符串匹配判据；作者称四个独立系统收敛于同一残余案例，支持将其读作 IFC 防御的语义极限。
• 作者称研究 CaMeL 解释器时发现意外的 taint 传播规则（如把不可信值插值进字符串字面量会隐式变可信），并认为其非干扰定理在 LLMbda 解释器中排除了这类缺陷。
• 附录 E.5 用六个不调用 LLM 的小例子探测 endorse 语义（洗 {U}→{}、不降机密性、受污染 pc 下惰性、值透传、非法目标报错、解除后续流测试）。

作者指出的局限与后续方向

• 数据源建模（§9 Conclusion）：工具调用与数据源的建模假设所有数据源都在程序内；作者认为更好的模型应允许 LLMbda 函数式程序与外部数据和工具的一般交互。
• endorse 滥用风险（§9）：含 endorse 的计划可把不可信数据洗过检查——§7.3 的两次成功攻击正是如此——且没有机制阻止过度宽松的规划器随意 endorse；作者称把约束规则提炼为设计规范（如执行前对计划做静态分析）是未来工作。
• 基准扩展（§7 开头）：作者计划未来在全部 AgentDojo 套件上、用完整 CaMeL 策略做基准；目前只实现了 CaMeL 策略的子集、只跑 banking 子集。
• 错误处理（§D.4）：作者称 Randori 的一大弱点是 LLMbda 缺少错误恢复，未来可考虑把错误处理作为语言原语或转向无运行时错误的全语言，并在 randori 阶段暴露信息流错误。
• 类型系统与语法（§D.4）：作者认为最小类型检查器可静态拒绝问题计划；对语法不在训练数据导致的 utility 成本，作者建议语法约束解码或更接近主流语言的表层语法。
• 鲁棒/定量 endorse（§E.2、§E.3）：知识型定义在概率设定下的发展留作未来工作；bounded_endorse 的形式定量界也留作未来工作。

实验覆盖范围

• 被测模型为 GPT-5.2、Qwen3.7-plus、MiMo-v2.5 共 3 个；CaMeL 重跑只覆盖其中 GPT-5.2 与 MiMo-v2.5 两个（Table 1）。
• 基准仅 AgentDojo banking 套件：16 user tasks × 9 injection attacks，k = 3 次重复；CaMeL 部分受攻击/安全运行未完成，其格子只计已完成运行（Table 1 注）。
• 消融仅 (no endorse) 一项，且只在 Qwen3.7-plus 与 MiMo-v2.5 两个模型上报告（Table 1）。
• 论文未报告评审模型或 LLM 裁判：utility 与 security 由 AgentDojo 的任务/安全检查器判定（§D.2），论文未说明其具体判定模型。
• 同一模型兼任代码生成与 Q-LLM；论文未评测 Q-LLM 换用更小模型的设置，§D.4 称解释器目前不支持多模型。

一篇形式化方法 + 系统论文：作者为 LLM 智能体的 prompt injection 防御提出 LLMbda 演算，并在 Lean 4 中完成全部机械化证明与可执行解释器。

• 问题：作者认为现有 provenance 防御（CaMeL、FIDES）的 IFC 在边界处易错、刻意放松难审计，且 dual-LLM 架构被写死、缺少覆盖代码生成智能体的 soundness 定理。
• 方法：LLMbda 把 prompt-response 会话（@、fork、clear）、代码生成和动态 IFC 作为一等构造，每个值带标签、每条归约传播标签；endorse 是显式可审计的重分类。作者证明全演算的 TIPNI（Theorem 1）与 Insulated TIPNI（Theorem 2，攻击者选择所有不可信输入时机密性仍成立），以及解释器的 oracular correctness（Theorem 3）；作者称其为首个可执行文件本身是机器检查定理对象的 LLM 智能体 harness。
• 结果 1：在 AgentDojo banking（16 tasks × 9 attacks，k = 3）上，Randori（IFC 常开）的受攻击 utility 为 59.5%–65%（三模型），与 CaMeL (no policy) 在置信区间内相当；CaMeL (with policy) 的 safe utility 降至 37.5%（Table 1）。
• 结果 2：Randori 在 1296 次受攻击运行中仅 2 次被攻破，均为 GPT-5.2 下同一语义性攻击（读文件并按内容付款）；作者认为这超出 IFC 防御范围。
• 结果 3：(no endorse) 消融显示 utility 下降（如 MiMo-v2.5 safe 从 64.6% 降至 54.2%），作者称印证 endorse 对读不可信文件并执行信任动作的任务必要。
• 结论与启示：作者认为隔离应成为程序表达的策略而非框架强加的形状；作者同时承认含 endorse 的计划可绕过检查，把约束 endorse 的设计规范与全套件基准列为未来工作。