Validating Network Semantics
This project developed a formal specification for the important TCP/IP protocols that underlie the modern internet. Because of the size of the specification, it was important that it be validated, which means confirming that it really did describe the behaviour of the existing implementations.
In the course of the project, we wrote low-level and high-level specifications of the protocols (together with the Sockets API for controlling them), and validated these against experimentally gathered traces. We mainly focussed on various BSD implementations, but we also tested a few traces gathered from Linux and Windows XP machines.
At NICTA, the project was led by Michael Norrish. At the University of Cambridge, work was led by Peter Sewell.
The VNS project finished in mid 2007.
Outcomes
The main outcomes for the VNS project were research papers, published at major international conferences:
- Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough. Rigorous Specification and Conformance Testing Techniques for Network Protocols, as applied to TCP, UDP, and Sockets. Proceedings of SIGCOMM, Philadelphia, 2005. pp265–276. (BibTeX)
- Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough. Engineering with Logic: HOL Specification and Symbolic-evaluation Testing for TCP Implementations. Proceedings of POPL, Charleston, 2006. pp55–66. (BibTeX)
- Tom Ridge, Michael Norrish and Peter Sewell. A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service. 15th International Symposium on Formal Methods: 2008 Proceedings, Turku, 2008. LNCS 5014, pp294–309. (BibTeX) (Slides)
The project also maintained links with a strong research group at the University of Cambridge.