Toward Comprehensive Network Verification: Practices, Challenges and beyond

Guaranteeing that large scale networks are always operated as policy goals dictate is critical for network availability, security, and performance. The problem is challenging, as it should not only assure the correctness of policy configurations across various network devices, but also guarantee the faithfulness of policy enforcement on actual packet forwarding behaviors. In this article, we provide a systematic overview of the direction of network verification, which covers both verification of network configurations and assurance of device actual behaviors. In particular, we summarize state-of-the-art designs with focuses from early stateless data planes with switches/routers to more recent stateful ones containing middleboxes. After analyzing and comparing these works, we also specify future directions in the verification of stateful networks.