Sagar Chaki

Seyed K. Fayaz, Tianlong Yu, Yoshiaki Tobioka, Sagar Chaki, Vyas Sekar, Proceedings of the 13th USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2016.

Abstract:Network operators today spend significant manual effort to ensure that their networks meet their intended policies. While recent work on network verification has made giant strides to reduce this effort, they focus on simple reachability properties and cannot handle context- dependent policies (e.g., how many connections has a host spawned) that operators realize using stateful net- work functions (NFs). Together, these introduce new expressiveness and scalability challenges that fall outside the scope of existing network verification mechanisms. In response, we present BUZZ, a system that enables operators to test if a network with a stateful data plane correctly implements intended context-dependent policies. Our design makes three key contributions: (1) A formalization of the problem that entails the expressiveness requirements in modeling the data plane; (2) A scalable model of the data plane using an abstract traffic unit that encodes policy-relevant context and a representation of complex NFs as an ensemble of finite-state machines; and (3) A scalable application of symbolic execution to tackle state-space explosion. Our evaluation shows that our design choices make BUZZ several orders of magnitude faster than existing mechanisms. Using BUZZ, we found a range of both new and known policy violations.