6. Relationship with previous work
The first use of SAT solvers for configuration synthesis was reported in [27]. The Alloy [1] system provides a firstorder logic language (Boolean logic with individuals and quantifiers over finite domains). Statements in this language are verified by transforming these into Boolean formulas and solving these with a SAT solver. However, quantifier removal, an essential part of translating first-order logic into Boolean, can lead to very large Boolean formulas. Thus, this approach does not scale to networks of realistic size. DADC addresses this problem by preprocessing constraints to solve as much of these as possible using algorithmic methods, leaving behind a constraint that truly requires the power of an SMT solver [18].
The systems described in [8], [12], [6], are only for verifying reachability properties of a network. They are not intended for the other tasks that DADC accomplishes such as configuration synthesis and repair.
DADC has been motivated by the same problems that Software-Defined Networking has been: it is hard to conceptualize networks as a whole, configuration is hard, and networks are not programmable. SDN’s approach to solving these problems is to separate the data and control planes. The network fabric contains utterly simple networking devices with only data-plane features such as forwarding and access control. All control-plane features such as routing protocols, tunneling and encryption are abstracted away into a logically centralized controller. The controllers communicate with devices over an out-ofband network using a well-defined API such as Openflow [13]. The biggest concern about this approach is that the powerful control-plane protocols have to be reimplemented from a centralized standpoint. If configuration is hard, programming is a lot harder!
DADC solves the first problem by allowing one to specify network-wide requirements. In other words, the conceptualization of the network as a whole is the set of requirements that it should satisfy. DADC solves the second problem by solving requirements using SMT solvers. What makes configuration hard is that requirements induce complex constraints between configuration variables and these constraints have to be manually solved. By using DADC to automatically and correctly configure existing control-plane protocols, one can fully exploit their power. For the third problem, it relies on interfaces provided by vendors, e.g., SNMP or SSH. The granularity of these interfaces is indeed coarse. However, well-defined APIs are now being offered in the new generation of components. DADC will be extended to use these in the future. A description of the application of DADC to specifying and emulating hybrid networks i.e., with both pure SDN and legacy components, is described in [15].
7. Overview of SAT and SMT solvers
Boolean logic is the most primitive language for modeling constraints. Examples of Boolean constraints are p∨q, p∧q, ¬p, p כq where p,q are propositional variables. The satisfiability problem (SAT) is to find values of propositional variables so a given constraint becomes true. For example, p∧q has only one solution, p=t,q=t, whereas p∨q has three solutions: p=t, q=t; p=t,q=f; p=f,q=t. Even though SAT is NP-complete, modern solvers [28] can often solve millions of Boolean constraints in millions of variables in seconds. The techniques behind these solvers were pioneered by Professor Sharad Malik, one of our coauthors. If a constraint is unsolvable, SAT solvers output an unsat-core, a typically small part of the constraint that is itself unsatisfiable. An unsat-core can be taken to be the “root-cause” of unsatisfiability. For example, the constraint p כq∧p∧¬q∧u∧v∧w∧x ∧y∧z has unsat core p⊃q∧p∧¬q. The variables u,v,w,x,y,z do not contribute to unsatisfiability.
However, Boolean logic is too low-level a language for modeling network constraints. We need to be able to talk about things like routers, interfaces, addresses and relationships between these. While these things and relationships can, in principle, be expressed in Boolean logic, a much more expressive option is to use the languages offered by Satisfiability Modulo Theories (SMT) solvers such as Z3 [33], CVC4 [4] and Yices [32]. These combine SAT solvers with domain-specific ones. Three domains, and their solvers, used in DADC are EUF (Equality of Unintepreted Functions), linear arithmetic and bitvector logic. EUF can be used to model data structures.
References
[1] Alloy: A language and tool for relational models. http://alloy.mit.edu/alloy
[2] Commercial Solutions for Classified Program. https://www.nsa.gov/ia/programs/csfc_program/
[3] Common Open Research Emulator (CORE). http://www.nrl.navy.mil/itd/ncs/products/core
[4] CVC4 SMT solver. http://cvc4.cs.nyu.edu/web/
[5] Fadi A. Aloul, Bashar Al Rawi, Mokhtar Aboelaze. Identifying the Shortest Path in Large Networks using Boolean Satisfiability.http://www.cse.yorku.ca/~aboelaze/publication/ABA06.pdf
[6] George Varghese, Yahoo Labs, Nick McKeown, Peyman Kazemian. Header Space Analysis: Static Checking For Networks. 9th USENIX Symposium on Networked Systems Design and Implementation, 2012. http://cseweb.ucsd.edu/~varghese/PAPERS/headerspace.pdf
[7] GNS3 Emulator. http://www.gns3.com
[8] Haohui Mai, Ahmed Khurshid, Rachit Agarwal, Matthew Caesar, P. Brighten Godfrey, Samuel T. King. Debugging the Data Plane with Anteater http://pbg.cs.illinois.edu/papers/anteater-sigcomm2011.pdf
[9] Jgroups. http://www.jgroups.org
[10] Leonardo De Moura, Nikolaj Bjørner. Satisfiability modulo theories: introduction and applications. Communications of the ACM. Volume 54 Issue 9, September 2011. http://cacm.acm.org/magazines/2011/9/122785-satisfiability-modulo-theories/abstract
[11] Leslie Lamport. Time, clocks and the ordering of events in a distributed system. Communications of the ACM, Volume 21 Issue 7, July 1978.
[12] Mohammed Noraden Alsaleh, Ehab Al-Shaer, Adel El-Atawy. Towards A Unified Modeling and Verification of Network and System Security Configuration. 5th Symposium on Configuration Analytics and Automation (SafeConfig 2012) http://goo.gl/bBdq3H
[13] Openflow SDN standard. https://www.opennetworking.org/sdnresources/ openflow
[14] Sanjai Narain, Dana Chee, Chung-Min Chen, Brian Coan, Ben Falchuk, Dov Gordon, Jon Kirsch, Siun-Chuon Mau, Aditya Naidu, Simon Tsang. Declarative, Distributed Configuration. PODC 2014 Distributed Software-Defined Networking Workshop, Paris, France, 2014. papers/narain/DSDN.pdf
[15] Sanjai Narain, Dana Chee, Sharad Malik, Shuyuan Zhang. Planning Hybrid SDN and Legacy Networks. Open Networking Users Group Conference, Research Track, Columbia University, New York, May 14, 2015.
[16] Sanjai Narain, Dana Chee, Sharad Malik. Demonstrating Assured and Dynamic Configuration over a live, emulated network.http://www.argreenhouse.com/papers/narain/ADCLive- Demo.pdf
[17] Sanjai Narain, Gary Levin, Vikram Kaul, Rajesh Talpade. Scalable and interactive method of generating and modifying network configurations to enforce compliance with high-level requirements. US 8,315,966. Granted 2012
[18] Sanjai Narain, Gary Levin, Vikram Kaul. Declarative Infrastructure Configuration Synthesis and Debugging. Journal of Network Systems and Management, Special Issue on Security Configuration. 2008.
[19] Sanjai Narain, Gary Levin. Query-based semantic analysis of ad hoc configuration languages for networks. US 8,554,796. Granted 2013.
[20] Sanjai Narain, Gary Levin. Router route reconfiguration planning. US 8,805,770 B2. Granted 2014
[21] Sanjai Narain, Gary Levin. Verifying access control policies with arithmetic quantifier-free form constraints. US 8,826,366 B2. Granted 2014
[22] Sanjai Narain, Konstantin Arkoudas. Optimal network configuration repair. US 8,725,902 B2. Granted 2014.
[23] Sanjai Narain, Rajesh Talpade, Gary Levin. Network Configuration Validation. Chapter in Guide to Reliable Internet Services and Applications, edited by Chuck Kalmanek, Richard Yang and Sudip Misra. Springer Verlag, 2010
[24] Sanjai Narain, Sharad Malik, Shuyuan Zhang. Planning Hybrid SDN and Legacy Networks. Open Networking Users Group Conference, Research Track, Columbia University, New York, May 14, 2015
[25] Sanjai Narain. BGP Stable Path Problem Specification in Alloy . Formal Methods in Networking Class, Princeton University, 2010
[26] Sanjai Narain. Moving-Target Defense by Configuration-Space Randomization. Filed 2014.
[27] Sanjai Narain. Network Configuration Management Via Model Finding. Proceedings of USENIX Large Installation System Administration (LISA) Conference, San Diego, CA, 2005. Also in Proceedings of ACM Workshop on Self-Managing Systems, Newport Beach, CA, 2004. Full report.
[28] Sharad Malik, Lintao Zhang. Boolean Satisfiability from theoretical hardness to practical success. Communications of the ACM. Volume 52 Issue 8, August 2009. http://goo.gl/2Grdy6
[29] Shuyuan Zhang, Abdulrahman Mahmoud, Sharad Malik. Verification and synthesis of firewalls using SAT and QBF. IEEE International Conference on Network Protocols, October 2012, Austin, TX
[30] Shuyuan Zhang, Laurent Vanbever, Sharad Malik, Sanjai Narain. In-Band Update for Network Routing Policy Migration. IEEE International Conference on Network Protocols, October 2014, Research Triangle, NC.
[31] Software Defined Networking. https://ee.stanford.edu/research/ software-defined-networking
[32] Yices SMT solver. http://yices.csl.sri.com/
[33] Z3 SMT solver. https://z3.codeplex.com/
RELEASE STATEMENT
Distribution A: Approved for Public Release; Distribution Unlimited : 88ABW-2015 4645 20150929.