Checking Beliefs in Dynamic Networks

Network Optimized Datalog (NoD) is a tool for checking beliefs about network reachability policies in dynamic networks. A belief is a high-level invariant (e.g., “Internal controllers cannot be accessed from the Internet”) that a network operator thinks is true. Beliefs may not hold, but checking them can uncover bugs or policy exceptions with little manual effort. Refuted beliefs can be used as a basis for revised beliefs. Further, in real networks, machines are added and links fail; on a longer term, packet formats and even forwarding behaviors can change, enabled by OpenFlow and P4. NoD allows the analyst to model such dynamic networks by adding new rules. By contrast, existing network verification tools (e.g., VeriFlow) lack the ability to model policies at a high level of abstraction and cannot handle dynamic networks; even a simple packet format change requires changes to internals. Standard verification tools (e.g., model checkers) easily model dynamic networks but do not scale to large header spaces. NoD has the expressiveness of Datalog while scaling to large header spaces because of a new filter-project operator and a symbolic header representation. NoD has been released as part of the publicly available Z3 SMT solver. We describe experiments using NoD for policy template checking at scale on two large production data centers. For a large Singapore data center with 820K rules, NoD checks whether any guest VM can access any controller (the equivalent of 5K specific reachability invariants) in 12 minutes. NoD checks for loops in an experimental SWAN backbone network with new headers in a fraction of a second. The NoD checker generalizes a specialized system, SecGuru, we currently use in production to catch hundreds of configuration bugs over the past year.