Vigor: Trusted Software Networking

As a joint project of NAL and DSLAB, we strive towards enabling the development of trusted and practical software network functions. We use speculative symbolic execution backed up by theorem proving in semi-automatic formal verification of performant network functions.

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

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.

 networking picture

Method

To handle stateful network functions, we encapsulate the state into a set of commonly used data structures, such as a hash table, array or LRU allocator. We implement and certify them using theorem proving engine. To the data structures’ API borderline, we replace them with symbolic-friendly but incomplete models that make exhaustive symbolic execution of the application possible. Our customized symbolic execution engine then verifies the application and generates a corpus of assumptions regarding the data structure contracts admitted in the process. We use our custom tool to prove the assumptions based on the formal API contracts.

We developed a dynamic NAT box as a simple stateful application. We are generalizing the approach starting from similar applications, such as

Results

Contact

Arseniy Zaostrovnykh, Luis Pedrosa, Solal Pirelli, 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.