Traditional internet routing systems involve precise configuration of many low-level parameters on each network devise. Software-defined networks (SDN) is an emerging approach to computer networking which abstracts away these lower level details from the traffic specification, thus allowing network routing reasoning at a higher abstraction level. ExCAPE researchers are exploring synthesis in both traditional internet routing systems, as well as in the software-defined networks emerging approach.
The Route Shepherd toolkit, applies synthesis techniques to automatically configure routing protocols. The motivation of the work lies in the fact that interdomain routing protocol stability depends on the absence of policy con icts between autonomous systems, but since most policy is kept private, it is hard to ensure that conflicts are avoided. Route Shepherd begins from a partially specific policy configurations, and then apply various synthesis techniques to complete the specifications in a safe manner. Route Shepherd has been applied, for instance, to solve the routing recovery problem. Given a network that is currently oscillating (i.e. unsafe), we devise a synthesis method to determine the shortest possible sequence of configuration changes (link weight updates) in order to make a given oscillation go away, while preserving connectivity. We focus on link weight changes because these are frequently used for traffic engineering, including by automated processes, so there is precedent for deciding what the link weights should be in order to meet a network design objective. The fewer actions need to be taken, the faster the recovery process will be.
To tackle the above problem, Route Shepherd adopts ExCAPE's synthesis methodology of completing partial programs using formal tools. Here, the initial unsafe network is formulated as a Partial Stable Paths Problem (PSPP), a generalization of the well-known Stable Paths Problem (SPP) formalism; this is adapted for coping with missing (partial) information. Route Shepherd will then fill in configuration parameters that are missing or broken, i.e. synthesis a set of reconfiguration steps, in order for the configuration to reach a safe state. In order for synthesis to be carried out efficiently, we adopt the use of Max-SMT techniques. Our evaluation on actual Internet topologies and evaluation on the Emulab testbed shows that Route Shepherd can result in fast recovery times that outperform random strategies. We have developed a prototype of Route Shepherd demonstrated at SIGCOMM'12 .[GHLL12] As ongoing work, we are continuing our work with traffic engineering in mind, where the resulting policies should not only be safe, but also meet traffic engineering goals of the network operator.
Mapping virtual networks to physical networks under bandwidth constraints is a key computational problem for the management of data centers. Recently proposed heuristic strategies for this problem work efficiently, but are not guaranteed to always find an allocation even when one exists. Given that the bandwidth allocation problem is NP-complete, and the state-of-the-art SAT solvers have recently been successfully applied to NP-hard problems in planning and formal verification, the goal of this work is to study whether these SAT solvers can be used to solve the bandwidth allocation problem exactly with acceptable overhead. We investigate alternative ways of encoding the allocation problem, and develop techniques for abstraction and refinement of network graphs for scalability. We conducted experimental comparisons of the proposed encodings with the existing heuristics for typical data-center topologies [YWAL13].
We recently started exploring the use of synthesis techniques in the context of SDN configuration.With the tremendous growth of the Internet and the emerging software-defined networks, there is an increasing need for rigorous and scalable network management methods and tool support. In [WMLTS13] we propose a synthesis approach for managing software-defined networks. We formulate the construction of network control logic as a reactive synthesis problem which is solvable with existing synthesis tools. The key idea is to synthesize a strategy that manages control logic in response to network changes while satisfying some network-wide specification. Finally, we investigate network abstractions for scalability. For large networks, instead of synthesizing control logic directly, we use its abstraction — a smaller network that simulates its behavior for synthesis, and then implement the synthesized control on the original network while preserving the correctness. By using the so-called simulation relations, we also prove the soundness of this abstraction-based synthesis approach.
The performance of networks using the Internet Protocol (IP) stack is sensitive to the precise configuration of many low-level parameters on each network device. These settings govern the action of dynamic routing protocols, which direct the flow of traffic; in order to make sure that the dynamic protocols all converge to produce some ‘optimal’ flow, each parameter must be set correctly. Multiple conflicting optimization objectives, nondeterminism, and the need to reason about different failure scenarios make the task particularly complicated. Mere simulation is certainly not enough to understand trade-offs and guarantee desired outcomes. We have been adopting a synthesis-based approach, that provides a fast and flexible approach to analysis of this management task. The idea is to combine logical satisfiability criteria with traditional numeric optimization, to reach a desired traffic flow outcome subject to given constraints on the routing process. The method can then be used to probe parameter sensitivity, trade-offs in the selection of optimization goals, resilience to failure, and so forth. The theory is underpinned by a rigorous abstraction of the convergence of distributed asynchronous, message-passing protocols, and is therefore generalizable to other scenarios. Our resulting hybrid engine is faster than either a purely logical or purely numeric alternative, making it potentially feasible for interactive production use. We have also developed a declarative domain specific language (DSL) used for programming secure Internet routing protocols [CJXLZL13]. Over the next year, we plan to use this DSL as a basis for synthesizing software-defined networking protocols. To handle potential state explosion problem in synthesis, we have developed an automated tool that allows us to reduce a large Internet graph to a smaller one for analysis [WGHCLTS14].
We address the problem of synthesizing network updates. Given a current network N and a specification of what the new network should satisfy, the problem is to synthesize the new network N0. Specifications of interest include properties such as (a) all packets in a class P of network packets should get delivered to a different node than where they are going now, (b) all packets in a class P should go to their current destinations, but should go through some firewall, etc. Furthermore, in order for the network N0 to be acceptable, we require that N0 be obtained from N using a minimal number of changes.
The space of packets is extremely large in any realistic network, and dealing with this state-space, especially in a synthesis setting, is extremely challenging. The group has developed a synthesis approach that uses novel techniques involving abstractions, static analysis, and SMT solvers, to overcome these difficulties, and built a prototype tool that can synthesize network updates. The key idea is to abstract packets into packet classes symbolically, where packet classes capture equivalence classes of packets that take the same path through the current network N. This is followed by a static pruning of the network to obtain the relevant core of the network that will be affected by the update. An abstract model of the network and the packets it processes is then built, where all header information gets hidden, resulting in a significantly simpler model than the original network. Finally, synthesis is solved using standard SMT solvers where constraints are modeled using uninterpreted functions over a theory of sets.
We are also investigating the problem of synthesizing controllers for software-defined networks, where the software that instructs the various nodes of what to do when a message arrives, is completely synthesized for a given specification of what the network must do. We are currently building a DSL for such controllers and co-designing the synthesis problem for such controllers.
The emergence of programmable interfaces to network controllers offers network administrators the flexibility to implement a variety of policies. We propose NetEgg, a programming framework that allows a network administrator to specify the desired functionality using example behaviors. Our synthesis algorithm automatically infers the state that needs to be maintained to exhibit the desired behaviors along with the rules for processing network packets and updating the state. We report on an initial prototype of NetEgg. Our experiments evaluate the proposed framework based on the number of examples needed to specify a variety of policies considered in the literature, the computational requirements of the synthesis algorithm to translate these examples to programs, and the overhead introduced by the NetEgg interpreter for processing packets [YAL14].
We have focused on the synthesis of structured discrete-time linear controllers that mimic the behavior of non-structured controllers. Our work has been motivated by the Wireless Control Network (WCN) architecture, which employs a fully distributed control scheme that causes the entire network itself to act as a structured linear controller. Our goal has been to derive a procedure that maps existing controllers into this structured computational substrate, which will enable direct use of the well-known controllers (e.g., the algorithms for controller tuning, such as PID tuning), along with the practical integration of the WCN with existing centralized controllers and monitoring networks. Specifically, we have derived algorithms for approximation of linear systems with potentially higher order systems that have some structural constraints. We have considered the general case of structural constraints, which usually means that it is not possible to exactly match the initial and derived controllers. Consequently, we employ techniques used for model reduction to specify an error system, which allows us to formulate the problem as synthesis of an optimal structured linear controller. The difference is that our structured controller (e.g., the WCN) has some freedom in the system dimension to compensate for the structural constraints i.e., to reduce the approximation error we can increase the sizes of states maintained by some nodes in the network. The derived synthesis procedure provides a structured controller implementation that minimizes the \(H_\inf\) norm of the error system [MPMP13].
- Y. Yuan, R. Alur, B. T. Loo. Netegg: Programming network policies by examples. 13th ACM Workshop on Hot Topics in Networks, 2014.
- C. Chen, L. Jia, H. Xu, C. Luo, W. Zhou, and B. T. Loo. A formal framework for secure routing protocols. In USENIX Symposium on Networked Systems Design and Implementation (NSDI) (demonstration), 2013.
- A. J. T. Gurney, X. Han, Y. Li, B. T. Loo: Route shepherd: stability hints for the control plane.SIGCOMM 2012: 91-92
- F. Miao, M. Pajic, R. Mangharam, G. J. Pappas. Networked Realization of Discrete-Time Controllers. In American Control Conference. Washington, DC, June 2013.
- A. Wang, A. Gurney, X. Han, J. Cao, B T. Loo, C. Talcott, and A. Scedrov. A reduction-based approach towards scaling up formal analysis of internet configurations. In 33rd Annual IEEE International Conference on Computer Communications (INFOCOM), 2014.
- A. Wang, S, Moarref, B T. Loo, U. Topcu, and A. Scedrov. Automated synthesis of reactive controllers for software-defined networks. In ICNP, pages 1–6. IEEE, 2013.
- Y. Yuan, A. Wang, R. Alur, and B. T. Loo. On the feasibility of automation for bandwidth allocation problems in data centers. In Formal Methods in Computer-Aided Design, FMCAD 2013, pages 42–45.