Proof-based Verification of Software Defined Networks

Software defined network (SDN) eases the task of programming and managing computer networks. The conceptually centralized nature of the control plane provides a holistic view of the network, thereby making it feasible to verify SDN’s functionalities. Verification of SDN is gaining attention in the last few years. There are two main challenges of SDN: (1) SDNs are often programmed in general-purpose programming languages (e.g. Java, Python), which makes it tedious and error-prone to apply formal methods over controller applications; (2) the sheer scale of modern networks makes state explosion problem an insurmountable challenge for model checking. Model checking techniques combined with limiting the expressiveness of the programming language have demonstrated as an effective approach to verifying basic properties. However, due to the highly dynamic nature of SDN, verification of more complex security properties is still challenging.

To address the above challenges, we propose a unified framework for programming and verification of SDNs. Our framework relies on the use of a declarative language, Network Datalog (NDLog), which provides compact encoding of SDN functionalities and serves as a basis for formal analysis. As a preliminary step, we demonstrate that NDLog can encode basic openflow applications succinctly, and preserve well-formed logical structure. Based on the semantics of NDLog, we develop a sound program logic for verifying invariant properties of NDLog program. The approach of static analysis avoids the state explosion problem. Also, properties of the system can be verified in a compositional manner by dividing them into smaller invariants of different components. Compared to existing proposals such as Frenetic, NDLog has a tighter connection to first-order logic and therefore makes the verification tasks easier.