Director: Simon S. Lam (more publications)
Hongkun Yang and Simon S. Lam, ``Real-time Verification of Network Properties using Atomic Predicates,'' IEEE/ACM Transactions on Networking, April 2016, Vol. 24, No. 2, pages 887-900 (first published as IEEE Early Access Article, 2015, Digital Object Identifier: 10.1109/TNET.2015.2398197); an early version in Proceedings of IEEE ICNP 2013, Göttingen, Germany, October 2013.
Abstract—Network management will benefit from automated tools based upon formal methods. Several such tools have been published in the literature. We present a new formal method for a new tool, Atomic Predicates (AP) Verifier, which is much more time and space efficient than existing tools. Given a set of predicates representing packet filters, AP Verifier computes a set of atomic predicates, which is minimum and unique. The use of atomic predicates dramatically speeds up computation of network reachability. We evaluated the performance of AP Verifier using forwarding tables and ACLs from three large real networks. The atomic predicate sets of these networks were computed very quickly and their sizes are surprisingly small.
Real networks are subject to dynamic state changes over time as a result of rule insertion and deletion by protocols and operators, failure and recovery of links and boxes, etc. In a software-defined network, the network state can be observed in real time and thus may be controlled in real time. AP Verifier includes algorithms to process such events and check compliance with network policies and properties in real time. We compare time and space costs of AP Verifier with Header Space and NetPlumber using datasets from the real networks.
Index Terms—Automated tools, formal methods, network management, network policies and properties, protocol verification, reachability computation.