Verifying Rule Enforcement in Software Defined Networks With REV

Software defined networking (SDN) reshapes the ossified network architectures, by decoupling the control plane and data plane. Due to such a decoupling, SDN assumes that rules issued by the control plane are always correctly enforced by the data plane. However, this assumption breaks as an adversary can prevent the data plane from enforcing the rules, by exploiting the vulnerabilities of switch OS and control channel. The serious consequence is that packets may deviate from their original paths, thereby violating critical security policies like access control. To this end, this paper introduces rule enforcement verification (REV), which enables the controller to check whether switches have correctly enforced the rules that it issues. Since using message authentication code (MAC) can incur heavy switch-to-controller traffic, we propose the compressive MAC, which lets switches compress MACs before reporting to the controller, thereby significantly reducing the bandwidth cost. Finally, we propose a heuristic flow selection algorithm, which allows the controller to verify much less flows for rule coverage. We implement REV based on Open vSwitch with DPDK, and use experiments to show: (1) by using compressive MAC, REV achieves a 97% reduction in switch-to-controller traffic, and an $8\times $ increase in verification throughput; (2) by using the heuristic flow selection algorithm, REV can reduce the number of flows to verify by 40%-60%.