Introduction and Welcome|
Cole Schlesinger (Barefoot Networks)
|The Good Stuff|
Toward SDN Programming Language for the Real World
Leonid Ryzhyk (VMWare Research)
I will talk about Cocoon 2--a new SDN programming language we are developing at VMware Research. Cocoon 2 aims to simplify the development and enable rapid innovation in complex real-world SDN applications. The language combines traditional procedural syntax for expressing packet forwarding behavior with a relational data model used to specify network configuration. The network administrator controls the application via the configuration database. The packet forwarding logic queries the database to make forwarding decisions. The queries are executed ahead of time by the compiler, which generates an OpenFlow program for every switch, eliminating the need for switch-to-controller communication at runtime.
Delta-net: Real-time Network Verification Using Atoms
Alex Horn (Fujitsu Labs. of America)
Real-time network verification promises to automatically detect violations of network-wide reachability invariants on the data plane. To be useful in practice, these violations need to be detected in the order of milliseconds, without raising false alarms. To date, most real-time data plane checkers address this problem by exploiting at least one of the following two observations: (i) only small parts of the network tend to be affected by typical changes to the data plane, and (ii) many different packets tend to share the same forwarding behaviour in the entire network. This paper shows how to effectively exploit a third characteristic of the problem, namely: similarity among forwarding behaviour of packets through parts of the network, rather than its entirety. We propose the first provably amortized quasi-linear algorithm to do so. We implement our algorithm in a new real-time data plane checker, Delta-net. Our experiments with SDN-IP, a globally deployed ONOS software-defined networking application, and several hundred million IP prefix rules generated using topologies and BGP updates from real-world deployed networks, show that Delta-net checks a rule insertion or removal in tens of microseconds on average, a more than 10X improvement over the state-of-the-art. We also show that Delta-net eliminates an inherent bottleneck in the state-of-the-art that restricts its use in answering Datalog-style "what if" queries.
|10:45am||A General Approach to Network Configuration Verification|
Ryan Beckett (Princeton University)
Control planes of traditional (non-SDN) networks are highly complex distributed systems. Network devices use multiple protocols to exchange routing information about available paths to a destination, and how they process this information depends on their local configuration files. These files often have thousands of lines of low-level directives, making it hard for humans to reason about individual device behavior and even harder to reason about the network behavior that emerges through their interactions. In this talk, I will present Minesweeper, a new verification tool that translates unmodified network configurations into logical formulae that capture both the network control plane behavior and its impact on packet forwarding in the data plane. Using an off-the-shelf SMT solver, we show that Minesweeper can verify a wide range of properties including reachability, fault-tolerance, router equivalence, and load balancing, for all possible packets and all possible data planes that might emerge from the control plane. We evaluate Minesweeper on a collection of real and synthetic configurations, showing that it is effective at finding issues in real configurations and verifying rich properties of large networks in minutes.
|11:15am||Network-wide Configuration Synthesis|
Ahmed El-Hassany (ETH Zurich)
Computer networks are hard to manage. Given a set of high-level requirements, operators have to manually figure out the individual configuration of potentially hundreds of devices running complex distributed protocols so that they, collectively, compute a compatible forwarding state. Not surprisingly, operators often make mistakes which can lead to downtimes. In fact, it has been shown that the majority of the network downtimes are due to misconfigurations.
In this talk we present SyNET; a novel synthesis framework that automatically computes correct network configurations that comply with the operator’s requirements. We capture the behavior of existing routers along with the distributed protocols they run in (stratified) Datalog. Our key insight is to reduce the problem of finding correct input configurations to the task of synthesizing inputs for a Datalog program.
SyNET works in practice and can generate network-wide configurations for multiple interacting routing protocols (OSPF and BGP) and static routes in networks with more than 50 routers.
|11:45am||Network Verification from Algorithms to the Real World|
Brighten Godfrey (Veriflow and UIUC)
Enterprise networks have become complex software artifacts weaving together interdependent devices, protocols, virtualization layers, optimizations, software bugs, and security controls. Yet communication is now critical infrastructure. How can we be sure networks are doing the right thing? The fact is, too often, they aren't. Despite enormous amounts of manual effort, outages and security vulnerabilities are common.
Can we prove that a network is correct? This is the goal of the emerging area of network verification. In this talk I'll discuss the original concept of data plane verification, and how it can incorporate advanced capabilities like real-time verification and modeling temporal uncertainty.
Today, verification technology has been deployed in large-scale production environments. Based on our experience at Veriflow, I'll discuss what principles of data plane verification persevered, what surprises we encountered, and how verification is solving problems in the real world.
|2:15pm||Welcome, from VMWare Research|
David Tennenhouse (Chief Research Officer, VMWare Research)
|2:30pm||Header Space Analysis|
Peyman Kazemian (Forward Networks)
It is notoriously hard to ensure that a network is working properly and implementing its intended security and connectivity policies, or when things go wrong, to find the root cause of the problem. In this talk I will explain how we can formally verify and systematically troubleshoot networks using Header Space Analysis. Header Space Analysis (HSA) is a general and protocol-agnostic framework for modeling the forwarding functionality of network. I will show how we can use HSA to statically check network state to identify an important class of failures such as reachability failures, blackholes ,forwarding loops, and violation of isolation policies. I will also show how we can use the same framework to pinpoint the root cause when such failures happen. Finally, I will demo how the productionized version of HSA was used in the core of Forward Networks Platform and share some insights learned along the way.
|3:00pm||Stochastic Superoptimization for Network Hardware|
George Varghese (UCLA)
Link Speeds are going up to 100G to higher, making it hard to design digital circuits for basic router forwarding such as IP lookups and especially for new primitives (measurement, debugging) and flexible primitives as in P4. Designers at Cisco, Arista today use CAD tools based on heuristics but often have to manually bail out the tool by hand for critical paths. Could we build a tool based on search inspired by recent work on network topology design? As a point of departure, observe that generating tight assembler fragments for high-speed tasks is also hard, often done manually. However, recent work uses Search techniques (e.g., stochastic superoptimization as in STOKE) to optimize small loop-free assembler fragments. In this talk we wish to explore the possibility of similar search-based ideas for hardware circuits. To do so, we must generalize earlier ideas based on simple line graphs of assembler instructions to arbitrary DAGs of hardware tiles. This talk is completely speculative and describes a possible new area of research in network verification/synthesis. Joint work with Alex Aiken, Stanford.
|4:00pm||Probabilistic Network Verification|
Nate Foster (Barefoot Networks/Cornell University)
Formal verification of networks has become a reality in recent years, with the rise of software-defined networking (SDN) and domain-specific property checking tools. Unfortunately, existing approaches have a fundamental limitation: they model networks as deterministic packet-processing functions, which means it is impossible to give satisfactory treatments of phenomena such as fault-tolerant and randomized routing schemes. This talk will introduce a new SDN language based on a probabilistic semantics. I will show how to enrich the NetKAT language with new probabilistic primitives, extending the formal semantics from one based on deterministic functions to one based on Markov kernels. I will also present a decision procedure based on an alternative representation as stochastic matrices and discuss applications to several real-world networking problems.
|4:30pm||ddNF: An Efficient Data Structure for Header Spaces|
Nikolaj Bjorner (Microsoft Research)
Network Verification is emerging as a critical enabler to manage large complex networks. In order to scale to data-center networks found in Microsoft Azure we developed a new data structure called ddNF, disjoint difference Normal Form, that serves as an efficient container for a small set of equivalence classes over header spaces. Our experiments show that ddNFs outperform representations proposed in previous work, in particular representations based on BDDs, and is especially suited for incremental verification. The advantage is observed empirically; in the worst case ddNFs are exponentially inferior than using BDDs to represent equivalence classes. We analyze main characteristics of ddNFs to explain the advantages we are observing.
Cole Schlesinger (Barefoot Networks)