arXiv:2602.16708cs.CRcs.AI2026-02被引 25

用形式化方法在智能体系统中强制执行安全策略,确保跨代理行为合规。

Formal Policy Enforcement for Real-World Agentic Systems

  • 通过面向切面编程将策略与推理分离,实时检查每一步决策是否合规。
  • 采用Datalog语言表达策略,支持递归规则和确定性执行,避免歧义。
  • 适用于多智能体系统中的信息流控制、审批流程等复杂合规场景。

当前智能体系统的安全策略大多依赖在系统提示中嵌入自然语言描述,并交由智能体自身推理判断是否遵守,这种方法缺乏形式化保障,且无法处理依赖执行因果历史的策略,尤其在多智能体系统中问题更为突出。本文提出一种基于面向切面编程的框架,将策略视为横切关注点,独立于智能体推理逻辑进行定义。策略以Datalog形式编写,基于一组抽象谓词描述执行上下文,由遵循假设/保证契约的可观测服务维护这些谓词,参考监控器在每个动作处查询策略并做出执行决策。当环境合同成立时,执行决策与策略语义一致。使用Datalog的优势在于支持声明式规则、递归表达传递关系,并实现确定性执行;同时具备高效的静态分析能力,可检测矛盾、冗余、包含和条件可达性,帮助作者验证策略意图并暴露自然语言规范中的模糊性。该框架已实现为FORGE系统,在不修改底层智能体的前提下对实际部署的智能体系统实施策略强制。在三个案例研究中评估:防御提示注入的信息流策略、多智能体药物警戒系统中的审批工作流、以及客户服务中的组织政策。

原文摘要 · Abstract (English)

Security policy enforcement in contemporary agentic systems predominantly consists of embedding natural-language policies within an agent's system prompt and delegating compliance to the agent's reasoning. This approach admits no formal enforcement guarantee and cannot express policies whose satisfaction depends on the causal history of an execution, a gap that becomes acute in multi-agent systems, where enforcement must reason across agents. We argue that policy enforcement in agentic systems is most naturally understood as a cross-cutting concern, and propose a framework grounded in aspect-oriented programming that specifies policies independent of the agent's reasoning and enforces them at every policy-relevant decision. Policies are written in Datalog over a set of abstract predicates describing the execution context, an observability service governed by a formal assume/guarantee contract maintains these predicates, and a reference monitor consults the policy at each action to produce an enforcement decision. When the environment contract holds, enforcement decisions coincide with the policy's intended semantics. We adopt Datalog as the policy language, a natural fit because it supports declarative rule specification, admits recursion for policies over transitive relationships, and yields deterministic enforcement. Datalog further admits tractable static analyses for contradiction, redundancy, subsumption, and conditional reachability, enabling authors to verify policy intent and surface ambiguities inherent in natural-language specifications. We realize the framework in FORGE, which enforces policies over agentic deployments without modification to the underlying agents. We evaluate FORGE on three case studies: information flow policies for prompt injection defense, approval workflows in a multi-agent pharmacovigilance system, and organizational policies for customer service.

智能体系统形式化验证策略强制Datalog

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。