Network Optimized Datalog (NoD) has the expressiveness of Datalog while scaling to large header spaces because of a new filter-project operator and a symbolic header representation.
Manually discovering any significant number of rules a system must satisfy is a dispiriting adventure — Engler et al.
Lack of knowledge: a major impediment is determining what specification to check13.
Network churn: existing verification techniques operate on a static snapshot of the forwarding state; … bugs only gets triggered when failures occur …modeling such dynamism and provide insight into the effect of such changes.
| policy | example |
|---|---|
| production sets | customer VMs cannot access controllers |
| reachable sets | customer VMs can access VMs |
| reachability consistency | backup routes have identical reachability (same path path length) |
| middlebox | waypoint a middlebox |
| locality | packets between two stations in the same cluster should stay within the cluster |
equivalence of load balanced path: load balancer ACL Bug — R2 and R3 load balance traffic from a source S to destination D. R2 has an ACL entry that specifies that packets to the SQL port should be dropped but R3 does not. NoD query: is it possible that some packet reaches a destination under one hash function but not another
R2(dst,h) :- G12, R1(ds,h), select(h,dst)
R3(dst,h) :- G13, R1(ds,h), select(h,dst)
...
NoD solutions intricate
...
TBC