Verified Network Data Structures

 Cool logo. e.g. something lightweight, but reliable as hell.

A joint project of NAL and DSLAB. More breathtaking prose and buzzwords here!

Overview

Context

Last decade is marked by a second coming of virtualization. The birth of cloud put a great demand on systems to be portable and replaceable. Now entire networks follow computing nodes and become virtualizable. That is how the SDN was born. As it advances more and more originally hardware functions move to the portable and flexible software domain.

However, the software development methods do not keep up with the raising responsibility. It is traditionally difficult to develop a reliable software implementation of an originally hardware component.

On the other side, formal verification techniques have grown strong enough to certify complete and practical systems. Such systems as a compiler, an operating system kernel, a distributed key value store or a file system.

 context picture

Networking

 networking picture

The low level high speed network functions together are called dataplane. Coming from hardware circuits historically they feature some design rules that help verification. The code is usually small and execution path length is limited. It is modular with a well defined interface - a frame (or a packet).

We follow the previous work[1] that succeeded in applying symbolic execution method to stateless dataplane modules. Such modules as a packet classifier, a checker or an Ethernet encapsulation. However, due to symbolic execution limitations it can not deal with a mutable state. And it is difficult to find a practical application that would not have it.

Method

In order to handle stateful modules, we plan to encapsulate the state into a set of common data structures. We then implement and certify them with a different approach. Finally, we extend the symbolic engine with theories incorporating specifications of that data structures.

We start with a dynamic NAT box as a simple stateful application. We hope then to generalize the developed approach to a comprehensive class in network software.

 method picture

Code

We host our code on github.

Recent Commits

Contact

Arseniy Zaostrovnykh, Volodymyr Kusnetsov, Katerina Argyraki, George Candea.

References

[1] Dobrescu, Mihai, and Katerina Argyraki. “Software dataplane verification.” Proceedings of the 11th Symposium on Networked Systems Design and Implementation (NSDI), Seattle, WA. 2014.