LLMbda 演算：AI 智能体、对话与信息流
论文信息
论文信息
摘要
大语言模型越来越多地被部署为智能体：它们进行规划、调用工具、读取不可信数据，并根据结果采取行动。这使它们暴露于提示注入（prompt injection）攻击：本意仅为读取的数据被当作指令执行。最原则性的防御方案是用来源（provenance）替代内容检查：根据来源对数据进行分类，并通过职责分离（双 LLM 模式）和信息流控制来保持可信与不可信数据的隔离。然而，领先的系统难以完全信任：流追踪容易出错，有意的松弛难以审计，而双 LLM 模式被硬编码到架构中。我们提出 LLMbda，一种无类型的按值调用 λ 演算，它将基于来源的防御变得既可表达又可证明是可靠的，且不承诺任何特定的架构。它将智能体系统的操作核心作为一等构造添加进来：支持分叉和清空的提示-响应对话、代码生成，以及动态信息流控制——其中每个值都携带一个标签，每个归约步骤都会传播该标签。隔离成为程序所表达的策略，而重新分类则成为一种显式、可审计的构造。我们的核心结果是在整个演算（包括生成代码的智能体）上的一个终止不敏感的概率无干扰定理，并有一个绝缘变体，即使攻击者选择所有不可信输入，该定理仍然成立。经过验证的解释器本身就是调用模型的工具（harness），据我们所知，这是第一个其可执行文件经过机器验证安全定理的 LLM 智能体工具，因此每个智能体都继承了这一保证。在 AgentDojo 银行基准测试中，基于 LLMbda 构建的智能体（始终启用强制检查）的实用性，与运行无策略检查（策略检查会使其实用性减半）的领先双 LLM 防御方案 CaMeL 相当，并且在 1296 次受攻击运行中仅有两例未能抵抗。我们的工具和所有证明均在 Lean 中完成。