PolyGram: A Certifying Compiler for Network Policies

Abstract

Network policies govern the backbone of the Internet. An error in their enforcement can have serious security and operational consequences, including large-scale operational outages. Yet correctness of their implementation is difficult to ensure due to the complex transformations from high-level specifications to low-level artifacts. Existing verification tools are often tied to specific languages or targets, limiting reuse and leaving much of the toolchain unverified. We present POLYGRAM, a language-agnostic framework built on the HOL4 interactive theorem prover for analyzing and transforming network policies across abstraction layers. POLYGRAM uses Multi-Terminal Binary Decision Diagrams (MTBDDs) as a unifying intermediate representation and provides a generic, certifying transformation that constructs both an MTBDD and a formal proof of semantic equivalence with the source policy. This transformation can be instantiated for diverse policy representations by verifying a small set of representation-specific components. Building on this foundation, we introduce a validation-based approach to trustworthy policy compilation that reduces compilation correctness to MTBDD equivalence checking. We further demonstrate how the same certified construction supports reusable policy analysis, including duplicate rule detection, policy equivalence checking, and policy minimization.