|
|
|
 |
|
Overview
Network verification and synthesis has emerged as an exciting area at the intersection of networking, programming languages, and formal methods. Motivated by the high frequency of network outages and security breaches, it aims to formally prove the correctness of certain aspects of the network, raise the level of abstraction for network design, and develop design approaches that are correct by construction. Researchers have developed a range of new techniques in the last few years, several of which have been rapidly put to practice in the world’s largest networks.
This course covers this literature and classify different techniques based on their use cases. We will also cover the foundational tools and results that the literature builds on and discuss problems that are still open.
Pre-requisite knowledge: Students are not expected to know either networking or formal methods. The necessary background will be covered as part of the course.
Meeting time and place
MW 3:30-4:50, MGH 058
Instructors
Ryan Beckett (ryan.andrew.beckett@gmail.com)
Ratul Mahajan (ratul@cs.washington.edu)
Course organization
The course will consist of 1) lectures on background material, 2) reading and discussing papers, and 3) projects. The students may do suggested projects or choosing something of their own (which they should run by the instructors).
Reading schedule (which will likely evolve)
Paper signup (If the direct link does not work, go via Canvas -> Collaborations)
| Sep 25
| Introduction to the course
Background slides: Course introduction, Network layer introduction
| | Sep 30
| Dataplane verification
Paper: Header space analysis
Additional reading: Anteater, Xie et al.
Background slides: SDN brief, Intro to SAT, SMT
| | Oct 2
| Incremental dataplane verification
Paper: VeriFlow
Additional reading: NetPlumber, Delta-net
| | Oct 7
| Scaling dataplane verification
Paper: Validating datacenters at scale
Additional reading: Libra, Atomic Predicates
Background slides: Intro to datacenter networks, packet processing, BDDs
| | Oct 9
| Dataplane verification with packet transformations
Paper: Atomic Predicates with Transformers
| | Oct 14
| Stateful dataplane verification
Paper: Verifying Mutable Networks (VMN)
Background slides: Routing (BGP)
| | Oct 16
| Control plane simulation
Papers: Batfish
Additional reading: FastPlane
Background slides: Stable paths
| | Oct 21
| Control plane verification
Papers: Minesweeper
Additional reading: Bagpipe
Background slides: Multi-protocol routing
| | Oct 23
| Scaling control plane verification
Papers: Arc
Additional reading: Tiramisu
Background slides: Routing algebra, Abstract interpretation
| | Oct 28
| Abstraction in control plane verification
Paper: ShapeShifter
| | Oct 30
| Exploiting symmetries in network verification
Paper: Bonsai
Additional reading: Origami, Surgery and Symmetry
| | Nov 4
| Dataplane synthesis
Paper: NetKAT
Additional reading: Merlin
| | Nov 6
| Control plane synthesis
Paper: Propane
Additional reading: Propane/AT
| | Nov 11
| Veteran's day holiday
| | Nov 13
| Control plane synthesis continued
Paper: SyNet
| | Nov 18
| Control plane repair
Paper: NetComplete
Additional reading: CPR
| | Nov 20
| Verifying software switches
Paper: Software dataplane verification
| | Nov 25
| Verifying programmable switches
Paper: p4v
Additional reading:
| | Nov 27
| Verifying SDN controllers
Paper: NICE
Additional reading: VeriCon
|
Schedule for suggested projects
The schedule to follow for suggested projects is below. If you want to pick alternative project(s), discuss the goals and schedule with the instructors.
Submit projects by emailing a pointer (e.g., GitHub) to the instructors. The pointer should contain the code, instructions on how to run it, and a short report (no more than two pages) that describes the implementation and benchmarks its performacne against networks of varying size.
Project 1
Due: Oct 18
|
Dataplane verification
Implement a basic dataplane verification technique of your choice. The inputs to your verifier is the network dataplane state in our 599n1-dp format and an invariant in 599n1-q format. The output should be a binary value that denotes if the invariant holds. To get you started, we have an example network file and invariants file.
|
Project 2
Due: Nov 1
|
Advanced dataplane verification
Implement an incremental or scalable dataplane verification technique of your choice. The inputs and outputs are similar to those above, except that if you are implementing the incremental verifier, you will need to supply two dataplane state inputs.
|
Project 3
Due: Nov 22 Nov 15
|
Control plane testing
Implement a technique for control plane testing. A common method for that is via a control plane simulator that generates the dataplane which is then verified using a dataplane verifier. The input to the tester is the control plane configuration in our 599n1-cp format and an invariant in 599n1-q format. The output should be a binary value that denotes if the invariant holds.
There are two new examples for the 599n1-cp format: network file and invariants file for the BGP disagree example. And the example from assignment 1 with BGP information: network file and invariants file.
|
Project 4
Due: Dec 13 Dec 6
|
Control plane verification
Implement a control plane verification technique of your choice. Similar to simulation but now must reason about failures. Example network and invariants files.
|
Project 5
Due: Dec 13
|
Control plane synthesis
Implement a control plane synthesizer. The input should be a high-level language for expressing the control plane intent, and the output should be device-level control plane configuration in the 599n1-cp format.
|
|
CSE Home