用语义差异定位授权策略的行为变化

AI 把需求写成权限策略之后，最难审的往往不是语法，而是它有没有悄悄改掉条件。两份策略看起来差很多，可能只是顺序不同；只改了一个 And，却可能放宽整条授权规则。

AWS ML Blog 这篇文章给出的办法是：先声明哪些表达式等价，再用反统一算法提取共同结构，把分歧集中展示。它适合给 AI 生成的策略做辅助审查，但不能替代需求核对，也不能凭两份结果相似就证明它们正确。

先消除表达差异，才能看见行为差异

原文从一个简单需求开始：敏感数据发往外部目的地时，必须加密。两个候选分别写成：

• 敏感数据且目的地在外部，则要求加密。
• 目的地不在内部且数据敏感，则要求审计。

这里混着三类变化：条件换了顺序，external 换成了 Not internal，结论从 encrypted 变成了 audited。文本 diff 会全部标出来，但审查者真正需要追问的是最后一项。

反统一（anti-unification）寻找两个表达式最具体的共同模式，经典形式来自 Plotkin 的 1970 年论文。这个引擎把算法放在 e-graph 上运行。可以把 e-graph 理解为一个保存「哪些表达式已经被证明等价」的数据结构：同一个意思允许保留多种写法，比较时可以利用这些等价关系。

等价关系需要明确声明。And 的 :assoc-comm-idem 表示结合律、交换律和幂等律，因此重新分组、调换顺序、重复条件都不算差异；:identity (Lit true) 则允许把缺失的条件与真值对齐。Or 对应的单位元是 (Lit false)，Eq 可以通过 :comm 声明交换律。

但外部目的地是否恰好等于非内部目的地，属于业务知识，引擎不会自行猜测。下面这段规则把它加入比较依据：

(rewrite (external d) (Not (internal d)))
(run 2)
(antiunify ruleA ruleB :algorithm exact)

要看的是第一行：它决定了一类差异能否被忽略。原文要求运行到饱和，也就是不再产生新的等价关系；示例中的 (run 2) 不能直接当作所有规则集都够用的固定次数。

加入规则后，结果只剩加密与审计的分歧：

(anti-unify :size 8 :cr 0.1429 :completion exact
  (Implies (And (sensitive data) (external dst)) (Variants encrypted audited)))

最后一行的 Variants 保存了两个候选的不同读法。统一选择每个 Variants 的第一个分支，可以恢复第一份输入；统一选择第二个分支，可以恢复第二份输入，恢复过程允许使用已声明的等价关系。

它交付的是共同结构和待审分歧，不是一张正确性证书。

两个真正的错误，怎样从大量改动里浮出来

原文更完整的案例是一条跨 Region 复制策略：源桶必须启用版本控制，目标必须位于批准的 Region；机密对象还要求源和目标属于同一账户，并启用使用客户管理密钥的服务端加密。对象大小不超过阈值时直接复制，超过时使用分段复制。

两个候选有五处文本差异。条件重排、Eq 参数交换、批准区域展开为 us-east-1 和 eu-west-1，属于表达变化。另两处改变行为：

• 机密对象的同账户检查与 sseCmk 从 And 变成 Or，满足任意一项就能通过。
• 阈值比较从 Lte 变成 Lt，恰好等于 multipartThreshold 的对象会走不同分支。

普通 diff 把 28 行中的 18 行标成变化。语义比较先吸收顺序和参数变化，再通过 (rewrite (approvedRegion r) (Or (usEast1 r) (euWest1 r))) 加上这个部署的区域定义，运行 (run 3) 后，只留下上述两个行为分歧。

其中 And 对 Or 的结果并不直观：它会生成两个相邻的 Variants，借助真、假单位元完成对齐。这是因为一阶反统一不能直接把连接词本身抽象掉。审查者仍然需要读懂这些节点合起来表达了什么。

原文用 :cr 衡量结构共享程度，公式是 (s - a) / b：s 是结果节点数，a、b 是当前 e-graph 中两个输入最小已知等价形式的大小，分别取较小者和较大者。Variants 标记不计数，但两个分支都计数。

简单案例中，输入各有 7 个节点，结果为 8，得到 0.1429；把两份完整输入并排保留是 14 个节点，得分为 1。这个值不是上限，例如输入各为 10、结果为 23 时，得分就是 1.3。复制案例加入区域规则后，:cr 从 0.5862 降到 0.4000，结果大小为 35。

:completion exact 表示搜索空间已经穷尽；budget 表示默认的 Monte Carlo 随时搜索耗尽了模拟次数。案例中的 :algorithm uct :playouts 3000 得到了与精确搜索相同的 size-35 结果，但不能据此推断所有输入都如此。

别只挑一个候选，正确策略可能需要拼出来

Dogwood 案例更能说明这套方法的用途。Dogwood 为 Cedar 授权策略增加时序条件，可以依据历史事件限制 AI agent 的行为。

需求是：只有最近 15 分钟内健康检查已返回 200，agent 才能向 /deploy 发起 POST。

候选 A 保留了方法和路径条件，却从 request 事件读取状态码，而这种事件没有该字段。候选 B 使用正确的 response 事件，却漏掉 /deploy 路径限制。健康检查通过后，它连 POST 到 /admin/purge-all 都会允许。

比较时，三条显式规则负责分钟转秒、常量乘法及时间比较方向转换，涉及 mins、secsTimes、secs、IBig::*、tLte、tGte，然后执行 (run 4)。连同已声明的代数，它们消除了六处表达差异，留下大小为 61、:cr 0.1864 的结果。

两个二选一分歧产生四种组合。Dogwood 的 schema 校验先排除使用 request 的两种，因为 output.status_code 不属于该事件；需求核对再决定保留路径条件。通过事件回放，可以验证错误候选允许目标外请求，而修复策略拒绝它。

最终答案是 B 的事件类型加 A 的路径条件，两份原始候选都没有写对完整策略。

这里还有一个重要前提：Cedar 的 && 会短路，交换操作数只有在两边都不会出错时才可靠。例如某个属性访问必须受到 has 检查保护，就不能随意重排。引擎不检查这个前提，比较过程依赖外部验证来排除顺序相关错误。

我的判断

我认可它把审查重点从整份文件缩小到具体分歧的做法。相比只给一个语义熵分数，保留共同结构与所有替代片段，更方便继续做 schema 校验、需求核对和反例分析。SMT 求解器还可以寻找「满足一份公式、违反另一份」的具体赋值，解释分歧会造成什么后果。

但它的可靠性建立在编码和比较规则可靠的前提上。规则少了，等价表达仍会显示为分歧；规则错了，真实差异可能被消掉。两个候选也可能共享同一个错误。

对于只涉及排序和格式的变化，规范化打印后再做文本 diff 通常更便宜，作者也承认这一点。这个引擎额外提供的价值，是利用单位元把缺失条件定位到共同结构内部，例如把路径限制与 eTrue 对齐，明确展示授权范围被放宽的位置。

工程证据也要按范围理解。作者在 Apple M3 Pro、Rust 1.97.1 的 release 构建下，对完整示例做了五次热运行，耗时 50–60 ms，包含解析、饱和、五次查询、回归检查和进程启动。这是案例实测，原文没有提供大规模策略集上的性能对照或检错率。

此外，引擎读取的是手工编码的 S-expression，不能直接导入 Cedar、Dogwood、OpenShell YAML 或 CEL。所给原文在 OpenShell 示例的输出处截断，后续 CEL 案例没有展开，不能据此评价完整覆盖能力。

能拿来做什么

• 如果团队正在用 LLM 把自然语言转成 SMT-LIB、Cedar 或 Dogwood，可以通过改变模型、提示词或采样温度生成多个候选，优先审核不稳定片段，再用独立检查验证共同部分。
• 对 Node 服务中的授权策略审查，可以重点检查缺失 guard、And 与 Or、Lt 与 Lte，并为对应分歧准备具体请求或边界输入，验证实际决策。
• 准备试用引擎时，可以检出原文固定提交 5a7969ae4ea88117a64faac4f42af5c358e213e2，执行 cargo build --release，再运行 ./target/release/semi-persistent doc/book/examples/12-first-au.egg。先复现示例，再评估自己的策略编码成本。
• 如果当前需求只是消除条件排序带来的审查噪声，可以先做规范化打印；当遗漏条件、业务等价关系和局部结构对齐成为主要困难时，再考虑引入反统一。