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 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.
SEFL was designed to ensure fast symbolic execution and lacks support for reasoning about more complicated network behaviours such as:
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.