No Arabic abstract
SDN controllers must be periodically modified to add features, improve performance, and fix bugs, but current techniques for implementing dynamic updates are inadequate. Simply halting old controllers and bringing up new ones can cause state to be lost, which often leads to incorrect behavior-e.g., if the state represents hosts blacklisted by a firewall, then traffic that should be blocked may be allowed to pass through. Techniques based on record and replay can reconstruct state automatically, but they are expensive to deploy and can lead to incorrect behavior. Problematic scenarios are especially likely to arise in distributed controllers and with semantics-altering updates. This paper presents a new approach to implementing dynamic controller updates based on explicit state transfer. Instead of attempting to infer state changes automatically-an approach that is expensive and fundamentally incomplete-our framework gives programmers effective tools for implementing correct updates that avoid major disruptions. We develop primitives that enable programmers to directly (and easily, in most cases) initialize the new controllers state as a function of old state and we design protocols that ensure consistent behavior during the transition. We also present a prototype implementation called Morpheus, and evaluate its effectiveness on representative case studies.
Programming distributed applications free from communication deadlocks and races is complex. Preserving these properties when applications are updated at runtime is even harder. We present DIOC, a language for programming distributed applications that are free from deadlocks and races by construction. A DIOC program describes a whole distributed application as a unique entity (choreography). DIOC allows the programmer to specify which parts of the application can be updated. At runtime, these parts may be replaced by new DIOC fragments from outside the application. DIOC programs are compiled, generating code for each site, in a lower-level language called DPOC. We formalise both DIOC and DPOC semantics as labelled transition systems and prove the correctness of the compilation as a trace equivalence result. As corollaries, DPOC applications are free from communication deadlocks and races, even in presence of runtime updates.
While SDNs enable more flexible and adaptive network operations, (logically) centralized reconfigurations introduce overheads and delays, which can limit network reactivity. This paper initiates the study of a more distributed approach, in which the consistent network updates are implemented by the switches and routers directly in the data plane. In particular, our approach leverages concepts from local proof labeling systems, which allows the data plane elements to locally check network properties, and we show that this is sufficient to obtain global network guarantees. We demonstrate our approach considering three fundamental use cases, and analyze its benefits in terms of performance and fault-tolerance.
We consider the task of computing (combined) function mapping and routing for requests in Software-Defined Networks (SDNs). Function mapping refers to the assignment of nodes in the substrate network to various processing stages that requests must undergo. Routing refers to the assignment of a path in the substrate network that begins in a source node of the request, traverses the nodes that are assigned functions for this request, and ends in a destination of the request. The algorithm either rejects a request or completely serves a request, and its goal is to maximize the sum of the benefits of the served requests. The solution must abide edge and vertex capacities. We follow the framework suggested by Even for the specification of the processing requirements and routing of requests via processing-and-routing graphs (PR-graphs). In this framework, each request has a demand, a benefit, and PR-graph. Our main result is a randomized approximation algorithm for path computation and function placement with the following guarantee. Let $m$ denote the number of links in the substrate network, $eps$ denote a parameter such that $0< eps <1$, and $opt_f$ denote the maximum benefit that can be attained by a fractional solution (one in which requests may be partly served and flow may be split along multiple paths). Let $cmin$ denote the minimum edge capacity, and let $dmax$ denote the maximum demand. Let $Deltamax$ denote an upper bound on the number of processing stages a request undergoes. If $cmin/(Deltamaxcdotdmax)=Omega((log m)/eps^2)$, then with probability at least $1-frac{1}{m}-textit{exp}(-Omega(eps^2cdot opt_f /(bmax cdot dmax)))$, the algorithm computes a $(1-eps)$-approximate solution.
Software Defined Networking (SDN) promises greater flexibility for directing packet flows, and Network Function Virtualization promises to enable dynamic management of software-based network functions. However, the current divide between an intelligent control plane and an overly simple, stateless data plane results in the inability to exploit the flexibility of a software based network. In this paper we propose SDNFV, a framework that expands the capabilities of network processing-and-forwarding elements to flexibly manage packet flows, while retaining both a high performance data plane and an easily managed control plane. SDNFV proposes a hierarchical control framework where decisions are made across the SDN controller, a host-level manager, and individual VMs to best exploit state available at each level. This increases the networks flexibility compared to existing SDNs where controllers often make decisions solely based on the first packet header of a flow. SDNFV intelligently places network services across hosts and connects them in sequential and parallel chains, giving both the SDN controller and individual network functions the ability to enhance and update flow rules to adapt to changing conditions. Our prototype demonstrates how to efficiently and flexibly reroute flows based on data plane state such as packet payloads and traffic characteristics.
Extended Berkeley Packet Filter (BPF) has emerged as a powerful method to extend packet-processing functionality in the Linux operating system. BPF allows users to write code in high-level languages (like C or Rust) and execute them at specific hooks in the kernel, such as the network device driver. To ensure safe execution of a user-developed BPF program in kernel context, Linux uses an in-kernel static checker. The checker allows a program to execute only if it can prove that the program is crash-free, always accesses memory within safe bounds, and avoids leaking kernel data. BPF programming is not easy. One, even modest-sized BPF programs are deemed too large to analyze and rejected by the kernel checker. Two, the kernel checker may incorrectly determine that a BPF program exhibits unsafe behaviors. Three, even small performance optimizations to BPF code (e.g., 5% gains) must be meticulously hand-crafted by expert developers. Traditional optimizing compilers for BPF are often inadequate since the kernel checkers safety constraints are incompatible with rule-based optimizations. We present K2, a program-synthesis-based compiler that automatically optimizes BPF bytecode with formal correctness and safety guarantees. K2 produces code with 6--26% reduced size, 1.36%--55.03% lower average packet-processing latency, and 0--4.75% higher throughput (packets per second per core) relative to the best clang-compiled program, across benchmarks drawn from Cilium, Facebook, and the Linux kernel. K2 incorporates several domain-specific techniques to make synthesis practical by accelerating equivalence-checking of BPF programs by 6 orders of magnitude.