Traditional computer networks require manual configuration of potentially hundreds of forwarding devices.To ease this configuration burden, software-defined networking (SDN) provides centralized, programmatic control of switch data planes in the form of applications, or control modules.This modular design simplifies development, and allows network operators to leverage a potentially vast library of open source SDN applications.However, configuring an SDN is still prone to misconfigurations, software bugs, and unexpected behavior.An operator must reason about the configuration on at least three planes in the network: the management plane, the control plane, and the data plane.At the control plane, an operator must ensure the applications driving the network are correct, or free of software bugs.At the management plane, an operator must determine how to compose together multiple applications to create a coherent forwarding behavior.This requires reasoning about inter-application interactions and how to resolve conflicts between them.Finally, she must understand the execution of the applications on top of the controller, and how any bugs in the controller's implementation may introduce unexpected behavior.This thesis explores techniques in verification and synthesis to ease the burden of configuring of an SDN and provide techniques to automatically search for unpredictable behavior.We present three primitives to search program behavior at the management plane, control plane, and data plane, without the need to understand the implementation details of the controller or applications.Specifically, we design primitives for orchestration, fast-forwarding, and autocorrect.First, to tackle the problem of SDN application correctness, we introduce a fast-forwarding primitive to verify and explore future behaviors of a control plane application.Unlike traditional approaches to software verification, this primitive faithfully models time --- an important source of complexity in control programs.We implement this idea in a model checker called DeLorean, and develop techniques to speed up the exploration of control programs.As a result, DeLorean can explore the future behavior of programs faster than they occur.Next, to reduce the complexity of composing together multiple, independent applications, we provide an orchestration primitive.This technique automatically discovers dependencies between applications and can suggest conflict-free composition plans to operators.With this primitive, we adopt a relational representation of the network and use a standard PostgreSQL database to develop a controller called Ravel.In addition to logic-based reasoning of inter-application dependencies, Ravel enables ad-hoc creation of new programming abstractions.Furthermore, Ravel can act as a runtime on which different abstractions or controllers can execute using translations to Ravel’s schema.Finally, to reduce the operator's burden of understanding the low-level implementation details of an application or controller, we introduce an autocorrection primitive with NEAt (Network Error Autocorrection).NEAt builds on synthesis techniques to prevent applications or a controller from installing policy-violating updates, ensuring the behavior of the network is correct and predictable at the data plane.NEAt allows backward-compatibility with existing SDN deployments and acts as a transparent layer between the network and controller, enforcing correctness by repairing updates that violate the network policy.We test our primitives on real-world datasets and applications.With DeLorean and Neat, we find bugs in real configurations running on deployed systems.
【 预 览 】
附件列表
Files
Size
Format
View
Toward predictable control of software-defined networks
PDF
download
878987797
028-85220240
