VeriCon: Verifying Controller Programs in SDN

Software defined networking (SDN) aims to simplify network management by removing the control plane from switches and running custom control applications at a logically central controller. Unfortunately, writing control applications that always maintain a set of network invariants (e.g., the network does not contain forwarding loops or blackholes) is a challenging task. Prior work uses finite-state model checking and network snapshots to identify bugs in control applications. They can find errors, but they cannot guarantee the absence of errors.

VeriCon symbolically reasons about (potentially infinite) network states to verify that network-wide invariants are preserved for any sequence of "events" (e.g., the controller receives a packet header from a switch, or a link fails) and on all admissible topologies, where invariants and topologies are expressed via first-order logic. VeriCon is sound in the sense that if it outputs "no errors" then the preservation of the specified invariants is guaranteed. When verification fails, VeriCon displays a concrete scenario that violates the invariants, in the form of an admissible topology and an event, and it is therefore a useful tool for debugging controller programs.