Language-Based Agent Control¶
会议: NeurIPS 2026
arXiv: 2605.12863
代码: https://github.com/timothytmzhou/elba
领域: LLM Agent
关键词: 智能体控制, 语言级安全, 类型系统, 信息流控制, 能力沙箱
一句话总结¶
提出基于程序语言理论的智能体控制范式（LBAC）及 Haskell 实现 Elba，将 LLM 智能体嵌入纯函数式强类型宿主语言中，利用静态类型检查与运行时抽象能力原生统一约束智能体代码与脚手架逻辑，在 AgentDojo 等基准上兼顾了比双模型硬隔离架构高近一倍的实用性与严格的无假阴性安全保证。
研究背景与动机¶
主流大模型智能体框架在控制力（Control）与表达力（Expressiveness）之间存在长期的两难割裂。一方面，基于固定工具调用的受限系统（如函数调用或单步 API）提供了严密的动作审计边界，但剥夺了智能体进行任意无副作用逻辑组合、结果自适应排序与高阶计算的能力；另一方面，基于沙箱化解释器（如 Bash、Python）的代码生成系统赋予了智能体极高的表达自由度，然而操作系统级粗粒度隔离与基于字符串正则匹配的权限系统，既无法表达应用级细粒度安全策略（例如“所有输出的参考文献必须源自可信学术数据库”、“客户 A 的数据绝不能流向客户 B”），又极易因 Shell 语法拼接或管道复合指令漏洞遭到绕过。
这种割裂的核心矛盾在于：现存的智能体安全防御多将安全策略置于代码执行环境“外部”或通过硬性的“代码与数据分离”架构进行物理隔离（如 Willison 的 Dual-LLM 模式或 CaMeL 框架）。然而，预先一次性生成代码并剥夺执行中观察能力的物理隔离严重损害了任务完成率；而基于事后匹配的审查机制又在语义层面缺乏形式化保证。
程序语言（PL）与语言级安全（Language-Based Security）领域长期以来证明了强类型系统能够在编译期完全消除整类非安全行为。本文的切入角度是：如果将 LLM 智能体本身建模为一个受宿主语言类型系统制约的普通纯函数，让智能体生成的程序、周围的脚手架控制流以及预置库共同寄宿在同一个类型安全的纯函数式语言中，那么类型检查器就能天然充当最外层的统一控制网。核心 idea：将智能体嵌入具备纯度和抽象数据类型的强类型宿主语言中，以类型签名定义安全策略与副作用边界，要求智能体生成必须通过静态类型检查的良类型程序，从而在无需代码与数据物理分离的前提下获得对完整智能体生命周期的严格安全保证。
方法详解¶
整体框架¶
LBAC 将整个智能体系统统一表述于单一的纯函数式强类型宿主语言（在系统实现 Elba 中为带有 Safe Haskell 扩展的 Haskell）。开发者在编写脚手架代码时，通过嵌入式领域特定语言（EDSL）定义受允许的自定义副作用 Monad 及不透明抽象数据类型（ADT）；系统核心暴露统一的高阶接口 agent :: Defs -> Prompt -> t，其中 Defs 是向智能体开放的类型与受限操作集合，t 为由上下文类型推导或显式标注决定的目标返回类型。
运行时执行流包含自适应的代码生成-类型检查回环：Elba 首先将系统提示词、可用函数签名及期望的具体类型 \(T\) 传递给 LLM 提示其生成程序；接着调用宿主语言编译器对其进行静态类型检查。若存在类型错误，错误诊断将被送回给模型重新自修正重试；通过类型检查后，程序交由安全解释器执行并将结果返回给宿主环境。智能体生成代码内部还可以通过递归调用 agent 派发具有同等或更严苛策略约束的子智能体。
%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
A["用户任务输入与脚手架上下文"] --> B["静态策略约束定义<br/>EDSL Effect Monad + 抽象类型 ADT"]
B --> C["提示词构造与类型推导<br/>确定 target type T 与可用 Defs"]
C --> D["LLM 智能体程序生成<br/>输出 Haskell 纯代码或受限 EDSL 程序"]
D --> E{"宿主类型检查器<br/>Γ ⊢ e_gen : T ?"}
E -->|类型检查失败| F["编译器类型错误反馈<br/>回传错误信息触发自修复重试"]
F --> D
E -->|类型检查通过| G["安全运行时受限解释执行<br/>Safe Haskell + 能力/LIO 运行时监控"]
G --> H["递归子智能体派发 / 最终策略保证输出"]关键设计¶
1. 静态策略约束定义：通过纯函数式效应 Monad 与抽象数据类型封锁副作用与数据伪造
为防止智能体越权调用原生系统功能（如调用标准库中的 writeFile 随意篡改文件）或伪造数据源，LBAC 依托纯函数式语言（Haskell）的无隐式副作用特性与 Safe Haskell 机制阻断底层逃逸接口（如 unsafePerformIO）。所有合规的交互动作均被封装在专用的自定义 EDSL 效应 Monad（如 BibIO、RIO 或 DC）中。当智能体目标签名设为纯类型（例如整数 Int）时，任何包含 IO 动作的代码由于类型不匹配均会在编译阶段被立即拒绝。同时，系统利用模块私有构造子定义不透明抽象数据类型（如 Trusted Bib），外部代码及智能体仅能通过可信 API（如 dblpFetchBib）获取该类型实例，而无法自行构造合法数据结构。因而，任何需要该抽象类型作为输入的受限写操作（如 appendToBibFile）从代数类型系统的根本结构上阻断了任意伪造或数据污染。
2. 递归智能体层次化类型继承：在单步代码生成中自然支持动态观察与策略收敛
传统针对代码生成的安全防御常假设智能体必须预先生成所有代码，无法像 ReAct 循环那样在感知中途观察数据。LBAC 揭示了智能体循环与函数式递归的同构性：在 Elba 中，智能体生成的一段程序内部可以直接包含对 agent 接口的递归调用。由于递归调用位于父级 Monad（例如 BibIO do 代码块）内部，宿主语言的 Hindley-Milner 类型推导机制会自动将其目标返回类型限定为 BibIO () 或更受限的无效应类型。子智能体因此在类型系统层面严格继承父级策略，杜绝了子智能体突破权限申请底层全量 IO 的漏洞；同时，父智能体可先执行搜索、读取第一条返回项并将观测嵌入新提示词中，使智能体系统能够以严密且层次化收缩的安全边界完成复杂的自适应决策。
3. 信息流控制与能力沙箱深度融合：泛化 Dual-LLM 范式并保持子智能体工具调用力
针对间接提示注入（Prompt Injection）和数据外泄，LBAC 引入成熟的粗粒度信息流控制库 LIO（Disjunction Category Labels）与路径能力约束。在 LIO 体系中，数据携带机密性与完整性标签，环境维护一个动态提升的浮动安全标签。通过高阶原语 toLabeled，智能体可在隔离子计算中执行任务：子智能体读取不可信网页时，其自身浮动标签的完整性被不可信源污染，返回值为不透明的 Labeled DCLabel Message，而父智能体外层标签不受影响。不同于现有 Dual-LLM 架构（必须完全禁止隔离模型调用任何工具，导致无法让子模型自行下载待总结内容），LBAC 允许子智能体继续保留受控工具调用权限（如安全抓取），通过运行时的浮动标签检查动态降低其执行特权动作的能力（低水位线原则，Low Watermark Policy）。对于文件系统，Elba 定义抽象 Path 能力对象并重载 // 运算，在运行时进行严格的符号链接解析与子树越界审查，在程序语义层彻底消除了基于 Bash 字符串模式匹配与逻辑连接符绕过的结构性缺陷。
一个完整示例：受限文献检索与编译期防伪造拦截¶
考虑一个从 DBLP 检索论文并写入 BibTeX 文件的任务。宿主环境声明：
data Trusted a -- 构造子未导出，外界无法伪造
type Bib = ...
dblpSearch :: String -> BibIO [DOI]
dblpFetchBib :: DOI -> BibIO (Trusted Bib)
appendToBibFile :: Path -> Trusted Bib -> BibIO ()
writeFile，或构造假数据传入 appendToBibFile：
-- 尝试伪造写入
p_malicious = do
writeFile "output.bib" "@article{fake_entry, ...}" -- 类型为 IO ()
appendToBibFile path ("@article{...}" :: Bib) -- 类型非 Trusted Bib
writeFile 返回的 Monad 为底层 IO ()，与当前任务上下文声明的目标类型 BibIO () 无法统一部合（Unification failure），编译直接报错；
2. 即使攻击者退而求其次调用 appendToBibFile，由于传入的不是经由 dblpFetchBib 输出并持有合法构造凭证的 Trusted Bib，类型检查器再次拒绝执行。
Elba 捕获类型错误并将其作为反馈引导模型重试。最终合法生成的代码：
p_safe = do
dois <- dblpSearch "differential privacy"
if null dois then return ()
else do
bib <- dblpFetchBib (head dois)
appendToBibFile bibPath bib
实验关键数据¶
主实验¶
论文在 AgentDojo 基准的 Slack 测试集（包含 21 项良性用户任务及 5 项提示注入攻击任务，全组合共 105 个攻击场景）上，将 Elba 与现存 SOTA 注入防御框架 CaMeL 进行端到端效用（Pass@1 任务完成率）对比。
| 系统 | 骨干模型 | 无攻击良性效用 (/21) | Direct 注入场景 (/105) | Important Instr. 注入 (/105) | Tool Instr. 注入 (/105) |
|---|---|---|---|---|---|
| Elba (有策略/LIO) | Claude Opus 4.7 | 10 (47.6%) | 52 (49.5%) | 51 (48.6%) | 50 (47.6%) |
| CaMeL (严格模式) | Claude Opus 4.7 | 5 (23.8%) | 24 (22.9%) | 23 (21.9%) | 22 (21.0%) |
| Elba (有策略/LIO) | Claude Opus 4.8 | 9 (42.9%) | 49 (46.7%) | 47 (44.8%) | 45 (42.9%) |
| CaMeL (严格模式) | Claude Opus 4.8 | 6 (28.6%) | 30 (28.6%) | 29 (27.6%) | 30 (28.6%) |
| Elba (有策略/LIO) | GPT 5.4 | 10 (47.6%) | 51 (48.6%) | 48 (45.7%) | 49 (46.7%) |
| CaMeL (严格模式) | GPT 5.4 | 5 (23.8%) | 23 (21.9%) | 26 (24.8%) | 25 (23.8%) |
| Elba (有策略/LIO) | Claude Sonnet 5 | 8 (38.1%) | 43 (41.0%) | 46 (43.8%) | 40 (38.1%) |
| CaMeL (严格模式) | Claude Sonnet 5 | 4 (19.0%) | 25 (23.8%) | 23 (21.9%) | 23 (21.9%) |
消融实验：最坏对抗注入与策略开关下的防御有效性¶
为了评估极端自适应注入下的鲁棒性，作者模拟了最坏情况对抗攻击：当包含 AgentDojo 注入标识符（TODO:）的外部数据送达子智能体时，提示词被完全替换为攻击载荷本身，强制受损子智能体按攻击意图执行指令。评测指标为注入抵御数与任务完成数（全量 735 次运行）。
| 系统配置 | 评测模型 | 注入抵御成功数 (/735) | 最终任务完成数 (/735) | 机制说明 |
|---|---|---|---|---|
| Elba (完整 LIO 策略) | Claude Opus 4.7 | 735 (100%*) | 351 | 完整性标签阻断受损子智能体提权执行特权写操作 |
| Elba (无安全策略/纯 IO) | Claude Opus 4.7 | 425 (57.8%) | 523 | 缺失 LIO 检查，42.2% 的直接注入成功突破并篡改动作 |
| Elba (完整 LIO 策略) | Claude Opus 4.8 | 735 (100%*) | 312 | 保证 0 漏报，无条件阻断向特权接收方泄露数据 |
| Elba (无安全策略/纯 IO) | Claude Opus 4.8 | 460 (62.6%) | 557 | 缺少标签溯源，37.4% 的注入攻击得逞 |
| Elba (完整 LIO 策略) | GPT 5.4 | 735 (100%*) | 290 | 跨模型一致抵御全部 735 次最坏对抗注入 |
| Elba (无安全策略/纯 IO) | GPT 5.4 | 670 (91.2%) | 256 | 模型自身对齐拒绝部分攻击，但仍有 8.8% 失守 |
| Elba (完整 LIO 策略) | Claude Sonnet 5 | 735 (100%*) | 294 | 形式化信息流下界约束提供百分之百防注入屏障 |
| Elba (无安全策略/纯 IO) | Claude Sonnet 5 | 540 (73.5%) | 494 | 无策略时 26.5% 的注入造成越权影响 |
*注：在 2940 次运行中有 28 次触发了 AgentDojo 将访问静态 URL 误判为成功注入的评分误报，人工审计确认无任何越权安全违规。
此外，在文献检索防伪造消融实验中，Pydantic-AI + 传统 Web 搜索工具生成的 1002 条引用中有 19 条属于幻觉伪造；而 Elba 利用 Trusted Bib 不透明类型约束，在 925 条引用中达成 0 幻觉伪造（0/925），同时输入/输出 Token 消耗分别降低 65 倍与 2.5 倍。代码生成阶段的类型检查平均重试次数仅为每任务 0.13 次，超出重试上限（3次）导致运行失败的比例极低（0.26%）。
关键发现¶
- 效用大幅跃升：在启用安全策略的相同前提下，Elba 的任务完成率达到了基线 CaMeL 的 2 倍左右。这主要是因为 LBAC 允许智能体在受控 EDSL 内自由交织数据读取与逻辑判断，摒弃了 CaMeL 必须预先静态生成整段固定流程的僵化结构。
- 确定性形式化防御零漏报：在强制执行攻击指令的最坏对抗注入测试下，无策略的智能体最高出现 42% 的失陷率；而启用 LIO 的 Elba 实现了对所有 735 次对抗注入的 100% 形式化阻断。
- 类型反馈开销极低：现代前沿模型（Opus 4.7/4.8、GPT 5.4、Sonnet 5）对 Haskell 类型系统的遵循度极高，代码首次通过率超过 87%，重试耗时仅占总运行时间的 3.4%。
亮点与洞察¶
- 将智能体控制重塑为类型系统工程问题：打破了过去只能依赖 Bash 正则表达式、不可靠的二次审核 LLM 或物理截断工具调用的旧范式，证明了程序语言几十年来成熟的纯度控制、Monad 效应系统和抽象数据类型能严密且轻量地管束当代大模型。
- 非侵入式复用成熟 PL 生态：Elba 无需自行发明新的安全机制，而是直接将学术界验证数十年的 LIO（动态信息流控制）、Safe Haskell 和代数能力系统开箱即用地引入智能体，兼得严密的形式化证明与现实工程可行性。
- 优雅解构 Dual-LLM 架构：通过
toLabeled原语，将业界粗糙的“隔离 LLM 禁绝工具调用”提炼为形式化的“标签浮动与局部解密（Declassification）”，允许被隔离的子智能体在安全水位下自主使用读取工具，极大释放了复杂智能体工作流的生产力。
局限与展望¶
- 动态 IFC 的过度保守性（False Positives）：LIO 采用的动态浮动标签（Low Watermark Policy）具有单向不可逆性，可能导致某些良性但涉及跨安全级数据组合的操作被拒绝，这也是开启策略后良性任务成功率略有下降的主要原因。
- 宿主语言生态与表达门槛：当前原型依托纯函数式语言 Haskell，对于习惯 Python 等主流命令式生态的开发者而言构建门槛较高；未来亟待将核心思想迁移至具备类型捕捉检查（Capture Checking）或代数效应支持的现代语言（如 Rust、Scala 3 或带有类型级装饰器的安全 Python 子集）。
- 更强类型属性的探索空间：目前主要验证了能力与信息流控制，未来可引入线性类型（Linear Types）实现一次性鉴权、细化类型（Refinement Types）约束算术界限与数组范围，以及摊还资源分析（AARA）保证智能体的计算与 Token 消耗上限。
相关工作与启发¶
- vs CaMeL (Debenedetti et al., 2025): CaMeL 采用静态架构硬隔离，要求智能体在看到真实数据前一次性生成完整程序，割裂了控制流与数据流；LBAC 允许智能体在执行期根据观察动态交互并递归派发子智能体，在同等阻断注入的前提下将任务效用翻倍。
- vs Fides / Prudentia (Costa et al., 2025; Kolluri et al., 2026): Fides 系列在工具调用外部构建定制的 IFC 拦截运行时；LBAC 则直接将控制内化于宿主语言类型系统，利用标准编译器与成熟 LIO 库原生保障全系统（包含脚手架）的统一语义。
- vs 系统级沙箱 (Bubblewrap / Docker / MiniScope): 操作系统沙箱只能提供粗粒度的静态路径或网络黑白名单；LBAC 基于类型的一等能力（First-class Capabilities）可在运行时动态缩紧、在进程内安全传递并作用于应用级逻辑资源。
评分¶
- 新颖性: ⭐⭐⭐⭐⭐ 突破性地将 PL 理论中的类型安全、纯度与 EDSL 原生映射到智能体控制中，视界开阔且立论优雅。
- 实验充分度: ⭐⭐⭐⭐⭐ 在 AgentDojo 基准上涵盖主流顶尖模型、极端自适应注入测试及真实文献防幻觉案例，对照详实。
- 写作质量: ⭐⭐⭐⭐⭐ 概念清晰，对比鲜明，代码范例与理论证明（类型可靠性归约）完备，行文极具说服力。
- 价值: ⭐⭐⭐⭐⭐ 为安全可靠智能体架构开辟了形式化程序语言路线，极具启发性与长远应用价值。