Ferhat Erata

← All news

· AWS AI Blog

Semantic diffing of formal policies

We use anti-unification to find what two policies share and where they differ.

Rémi Delmas and I wrote about semantic diffing on the AWS AI Blog. Local rewrites let us recognize equivalent expressions and compress shared logic into a common backbone (an abstraction function). The remaining differences are the parts to review.

Two SMT-LIB policies feed a shared abstraction function F(k). Both require administrator, owner, or delegate authorization and encryption for confidential data, despite differences in syntax and ordering. The semantic diff isolates their usage limits: 100 in Policy A and budget minus reserve in Policy B. Only the differing limits are highlighted.
Both policies keep the same authorization and encryption requirements. The usage limit changes from 100 to the budget minus the reserved amount. The shared function captures the common logic; the diff isolates the limit. Open the full-size figure ↗

To make this scale, we use a semi-persistent e-graph. It handles equivalent reorderings and regroupings natively, keeps representations compact, and supports efficient backtracking.

This makes reviews easier in formal verification workflows involving languages such as Cedar, Dogwood, SMT-LIB, and Lean. Comparisons use the equivalences declared for the chosen encoding.

Read the AWS AI Blog post Source code

#FormalVerification #AntiUnification #EGraphs