Recent verification work has made advances in finding bugs in P4 programs before deployment, but it requires that the programmer specifies table rules that are possible at runtime[32, 24, 27]. This imposes a specification burden on the programmer, while at the same time failing to guarantee that bugs will not be inserted at runtime by faulty controllers. We present bf4, a novel verification approach for P4 programs that uses a mix of static verification, code changes and runtime checks to ensure that the deployed P4 program is bug free. To achieve this, bf4 uses static analysis to find all possible bugs in the P4 program; for each possible bug, bf4 attempts to find predicates that, when applied to table rules inserted by the controller, make that bug unreachable. If such predicates do not exist, bf4 can change the P4 code and re-run the procedure above. We applied bf4 to a wide range of P4 programs; for all these, bf4 is able to generate controller assertions and propose fixes that guarantee no controller-induced bug is reachable. At runtime, bf4 checks that the controller does not insert faulty rules; when it does, it throws an exception which helps troubleshoot the bug.

We present Vera, a tool that verifies P4 programs using symbolic execution. Vera automatically uncovers a number of common bugs including parsing/deparsing errors, invalid memory accesses, loops and tunneling errors, among others. Vera can also be used to verify user-specified properties in a novel language we call NetCTL. To enable scalable, exhaustive verification of P4 program snapshots, Vera automatically generates all valid header layouts and uses a novel data-structure for match-action processing optimized for verification. These techniques allow Vera to scale very well: it only takes between 5s-15s to track the execution of a purely symbolic packet in the largest P4 program currently available (6KLOC) and can compute SEFL model updates in milliseconds. Vera can also explore multiple concrete dataplanes at once by allowing the programmer to insert symbolic table entries; the resulting verification highlights possible control plane errors. We have used Vera to analyze many P4 programs including the P4 tutorials, P4 programs in the research literature and the switch code from https://p4.org. Vera has found several bugs in each of them in seconds/minutes.

Neutron is the OpenStack component that implements networking and it has been mocked and derided the weakest line in OpenStack [11]. We propose to use network symbolic execution to improve Neutron's ability to correctly implement tenant policies and to provide tenant traffic isolation. We propose to apply symbolic execution on two different OpenStack layers: the tenant view of the network and the actual deployment. Analyzing the tenant view is useful in many ways; first, it helps the tenant better understand its configuration's behavior before deployment. Secondly, its outputs can be compared to the analysis of the deployment to check if they are equivalent. We have built a prototype implementation and conducted preliminary evaluation, finding that we can verify our department's OpenStack deployment in seconds and detect certain common Neutron problems.

We present SymNet, a network static analysis tool based on symbolic execution. SymNet injects symbolic packets and tracks their evolution through the network. Our key novelty is SEFL, a language we designed for expressing data plane processing in a symbolic-execution friendly manner. SymNet statically analyzes an abstract data plane model that consists of the SEFL code for every node and the links between nodes. SymNet can check networks containing routers with hundreds of thousands of prefixes and NATs in seconds, while verifying packet header memory-safety and covering network functionality such as dynamic tunneling, stateful processing and encryption. We used SymNet to debug mid- dlebox interactions from the literature, to check properties of our department’s network and the Stanford backbone. Modeling network functionality is not easy. To aid users we have developed parsers that automatically generate SEFL models from router and switch tables, firewall configura- tions and arbitrary Click modular router configurations. The parsers rely on prebuilt models that are exact and fast to an- alyze. Finally, we have built an automated testing tool that combines symbolic execution and testing to check whether the model is an accurate representation of the real code.

Network Function Virtualization is pushing network operators to deploy commodity hardware that will be used to run middlebox functionality and processing on behalf of third parties: in effect, network operators are slowly but surely becoming in-network cloud providers. The market for innetwork clouds is large, ranging from content providers, mobile applications and even end-users.