SEFL v2.0

What is network verification and why we need it?

In the last 10 years the scale and complexity of networks has grown exponentially (datacenters are one example). However, the production tools for ensuring network correctness (such as traceroute or tcpdump) are outdated.

There has been a current trend in applying software verification techniques to networks. Unlike testing which validates an implementation against specific inputs, verification relies on formal methods to prove correctness w.r.t. all possible inputs.

SEFL & Symnet

SEFL & Symnet follow this very same trend. A network topology, together with all its switching, routing, or more advanced boxes, is modelled as a single program. Program inputs are packets which can be sent on any device interface from the topology. The output is the set of interfaces which the packet may reach. The modelling (programming) language is SEFL (Symbolic-Execution-Friendly Language) and was specifically designed for this task.

The verification technique employed to guarantee network correctness is symbolic execution and has been implemented as part of the Symnet tool. Symbolic execution allows exploring all possible execution paths of a program.

About the project: SEFL 2.0

SEFL was designed to ensure fast symbolic execution and lacks support for reasoning about more complicated network behaviours such as:

  • Packet duplication
  • Packet reordering
  • The correctness of stateful network devices (NATs, Intrusion Detection Systems, etc.)

The aim of the project is to develop SEFL 2.0 - an extension to the SEFL language as well as an execution engine capable of addressing the above issues.

First steps

  • Read the first 7 section of the Symnet paper.
  • Get yourself familiar with Monads in Haskell and programming in the monadic style

Required knowledge

  • Experience with Haskell and Scala
  • Basic knowledge about switching and routing in conventional networks

Partners

Bloomberg Wyliodrin

Organizers

ROSEdu Logo

This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 3.0 Unported License.
Creative Commons License