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
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
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.
Project report (submitted for publication)
Riccardo Sisto's Tech Talk given on July 24 at Cisco (San Jose)
Last Update: August 2009