Guided synthesis of network behavior

In the past decades, the world has witnessed how essential modern networks, such as data centers and enterprise networks, have become in our daily lives. However, on the other hand, configuring and maintaining a modern network, is a challenging and error-prone process. Administrators must often consider security policies from a variety of sources simultaneously, including regulatory requirements, industry standards, to mitigate attack vectors. Erroneous implementation of a policy, however, can result in costly data breaches and intrusions. Relying on humans to discover and troubleshoot violations is slow and prone to error, considering the speed at which new attack vectors propagate and the increasing network dynamics, partly an effect of SDN. To ensure the network is always in a state consistent with the desired policies, administrators need frameworks to automatically diagnose and repair violations as the network evolves. To address this problem, in this dissertation, we present a system automatically synthesizing network changes that meets a network correctness specification given as a policy. If we consider a network as a distributed program, the problem here is essentially a program synthesis problem. Recent work on program synthesis illustrates many benefits of allowing the user to augment the correctness specification with some guidance. We adopt a similar philosophy: our system is guided by user instructions to constrain the space of allowed implementations in order to keep pace with network dynamics. As the foundation of our system, we first develop a verification technique that detects network-wide invariant violations responsively. Based on the verification results, our core algorithm repairs network updates in two aspects. If an update violates a policy defined by an administrator, such as reachability or segmentation, our algorithm transforms the update into one that complies with the policy. In addition, given two correct network states, our algorithm synthesizes a feasible and efficient update ordering to migrate the network from one to the other. With our prototype implementation, we tested our system on physical testbed, emulated SDN networks, and a large enterprise network’s operational traces. We demonstrated that it is practical and efficient to use user instructions as guidance to incrementally build/maintain a network state, where desirable properties are automatically preserved all the time