Workshop on
Network Verification

Registration

Update: We have reserved a larger room, and registration has been reopened. Participants on the waitlist have been registered.

The workshop is open to researchers in both industry and academia at no cost; however space is limited and will be allocated on a first-come, first-serve basis. Please, register here by April 21st.

Overview

The Workshop on Network Verification highlights new problems and research at the intersection of networking and formal methods, with an emphasis on bringing work in this area to the attention of audiences beyond the traditional networking research community, including researchers in formal methods and programming languages and industry groups focused on networking, security, and verification.

Time

WNV will be held on Friday, April 28th.

Location

The workshop will be held in the Vasa Elastic Sky conference room in the Hilltop-A building on the VMWare campus.

Directions and parking information.

Please sign in for a visitor pass in Hilltop-A.

Organizers

Leonid RyzhykVMWare Research
Cole SchlesingerBarefoot Networks

Program

Opening Session
8:30amBreakfast
9:00am Introduction and Welcome
Cole Schlesinger (Barefoot Networks)
The Good Stuff
9:05am Toward SDN Programming Language for the Real World
Leonid Ryzhyk (VMWare Research)
Abstract
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.
9:35am Delta-net: Real-time Network Verification Using Atoms
Alex Horn (Fujitsu Labs. of America)
Abstract
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:05amCoffee
10:45amA General Approach to Network Configuration Verification
Ryan Beckett (Princeton University)
Abstract
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:15amNetwork-wide Configuration Synthesis
Ahmed El-Hassany (ETH Zurich)
Abstract
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:45amNetwork Verification from Algorithms to the Real World
Brighten Godfrey (Veriflow and UIUC)
Abstract
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.
12:15pmLunch
2:15pmWelcome, from VMWare Research
David Tennenhouse (Chief Research Officer, VMWare Research)
2:30pmHeader Space Analysis
Peyman Kazemian (Forward Networks)
Abstract
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:00pmStochastic Superoptimization for Network Hardware
George Varghese (UCLA)
Abstract
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.
3:30pmCoffee
4:00pmProbabilistic Network Verification
Nate Foster (Barefoot Networks/Cornell University)
Abstract
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:30pmddNF: An Efficient Data Structure for Header Spaces
Nikolaj Bjorner (Microsoft Research)
Abstract
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.
Closing Session
5:00pmWrap-up
Cole Schlesinger (Barefoot Networks)
Cocktail Reception