Formal Methods for Protocol Classification Software


This project is partially funded by a gift awarded to prof. Riccardo Sisto in 2008 from The Cisco University Research Program Fund, a corporate advised fund of  Silicon Valley Community Foundation.

Project Summary
Safety is a fundamental quality in network software, because the possibility of unforeseen runtime errors impairs reliability, availability and security. Of course, safety can be enforced by introducing proper run-time checks, which however has a negative impact on performance. Therefore, the ability to develop code whose safety can be formally and automatically established at compile time rather than checked at run time is highly valuable, especially in high-speed packet processing applications, which are tied to work within strict time and resource bounds.
Research on formal methods and static program analysis has made much progress in the last years, and these disciplines have now reached the maturity level needed for several real-world applications (e.g. the java bytecode verifier or the formal verification of smartcard software), where the language features to be checked enable formal checks to be carried out automatically and efficiently.
This research project aims at investigating how the recent progress in formal methods for automated program verification can be leveraged in the specific field of high speed protocol classification and packet processing software, by exploiting the specific characteristics of this software (e.g. the heavily data-oriented paradigm and the light restrictions on compile-time and load-time resources).
The proposed approach is based on the model-driven software development paradigm, where code is automatically generated from descriptions given in protocol description languages (PDL). By appropriately designing how code is generated, we expect to be able to get software safety properties by construction, or at least the possibility to generate code in a form that favors the application of already existing automatic formal analysis techniques.
Automation is a fundamental key issue for acceptability of techniques based on formal methods, because software developers are normally not skilled in formal methods, and the proposed approach goes exactly in this direction, and opens the possibility to finally get formal safety guarantees on packet processing code without introducing runtime overhead or additional software developer work.
The research is being carried over by Riccardo Sisto's research group, in collaboration with the NetGroup at the Politecnico di Torino.
The main expected result of this research work is to define an improved code generation scheme for packet classification that uses the NetPDL language as input and enables the emission of code on which a predefined set of safety properties is either formally guaranteed to hold by construction, or can be automatically checked at compile time. The new scheme will then be implemented in a proof-of-concept prototype.

Investigators
Riccardo Sisto
Fulvio Risso
Pierluigi Rolando


Project report (submitted for publication)

Riccardo Sisto's Tech Talk given on July 24 at Cisco (San Jose)

Last Update: August 2009