A Decision-Diagram Framework for Conflict Detection in Multi-Layer Cilium Network Policies

Cilium is among the most widely deployed Container Network Interfaces (CNIs), serving as the default CNI in the Google Kubernetes Engine. It extends standard Kubernetes NetworkPolicy (KNP) with two additional types—CiliumNetworkPolicy (CNP) and CiliumClusterwideNetworkPolicy (CCNP)—each with distinct semantics. When all three coexist in a cluster, the resulting composition is difficult to reason about formally, leading to misconfiguration and security incidents. Existing verification tools, KANO and VeriKube, address subsets of the problem but share two critical limitations: neither provides a formal denotational semantics that precisely characterizes the three-layer composition, nor a canonical representation enabling policy-equivalence checking with completeness guarantees. We close this gap with three contributions. First, we develop the first formal denotational semantics for Cilium’s three-layer composed policy—KNP (additive), CNP (deny-wins), CCNP (cluster-override)—and prove that the composite function is Hyper-Rectangular Piecewise-Constant (HRPC)-like. Second, we construct a Reduced Ordered Interval Decision Diagram (ROIDD) for the composite policy space and prove a canonicity theorem—canonical for a fixed field order—enabling policy-equivalence checking as structural isomorphism in O(|ROIDD|) time. Third, we develop certified conflict-detection algorithms for shadow, redundancy, and cross-layer conflict anomalies across all three layers with formal proofs of soundness and completeness. Experimental evaluation on synthetic policies confirms zero mismatches between ROIDD evaluation and ground-truth brute force; detection of shadow, redundancy and cross-layer anomalies at precision and recall of 1.000, scored against exhaustive enumeration of the entire packet space; agreement with a live Cilium v1.19.5 data plane on every probe of a scenario built to exercise each clause of the composite semantics; ROIDD compression ratios of 5–15× over the unshared decision tree on the compressed evaluation domain; and low-microsecond (0.74–1.95 µs) per-packet lookup latency that is independent of policy size. A native C++ implementation, evaluated on the same policy dataset, reconstructs the identical decision-diagram structure and classifies each packet in under 60 ns—roughly 30× faster than the Python reference—confirming that sub-microsecond classification is inherent to the algorithm rather than an artifact of the implementation language.