Toward Synthesis of Network Updates

Andrew Noyes
(Cornell University)
Todd Warszawski
(Cornell University)
Pavol Černý
(University of Colorado Boulder)
Nate Foster
(Cornell University)

Updates to network configurations are notoriously difficult to implement correctly. Even if the old and new configurations are correct, the update process can introduce transient errors such as forwarding loops, dropped packets, and access control violations. The key factor that makes updates difficult to implement is that networks are distributed systems with hundreds or even thousands of nodes, but updates must be rolled out one node at a time. In networks today, the task of determining a correct sequence of updates is usually done manually – a tedious and error-prone process for network operators. This paper presents a new tool for synthesizing network updates automatically. The tool generates efficient updates that are guaranteed to respect invariants specified by the operator. It works by navigating through the (restricted) space of possible solutions, learning from counterexamples to improve scalability and optimize performance. We have implemented our tool in OCaml, and conducted experiments showing that it scales to networks with a thousand switches and tens of switches updating.

In Bernd Finkbeiner and Armando Solar-Lezama: Proceedings Second Workshop on Synthesis (SYNT 2013), Saint Petersburg, Russia, July 13th and July 14th, 2013, Electronic Proceedings in Theoretical Computer Science 142, pp. 8–23.
Published: 28th March 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.142.8 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org