FLOVER, a model checking system which verifies that the aggregate of flow policies instantiated within an OpenFlow network does not violate the network’s security policy. We have implemented FLOVER using the Yices SMT solver, which we then integrated into NOX, a popular OpenFlow network controller. FLOVER provides NOX a formal validation of the OpenFlow network’s security posture.
We propose a provably correct and automatic method for verifying that a given non-bypass property holds with respect to a set of flow rules committed by an OpenFlow controller. Non-bypassability is a basic security property, which is enforced by most firewalls and switches.
Our experimental evaluation of FLOVER performance shows that our prototype implementation on Yices can detect coverage and modify violations of up to 200 rules in under 131 ms and 120 ms respectively.