Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Computer Laboratory
Thursday Feb 3rd, 2005 - 4:30pm
Computer Laboratory > Research > Systems Research Group > NetOS > Seminars > Thursday Feb 3rd, 2005 - 4:30pm

Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets

Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, and Keith Wansbrough.

Network protocols are typically described in RFCs using informal prose and pseudocode. That informality has benefits, but inevitably these descriptions are somewhat ambiguous and incomplete. The protocols are hard to design and implement correctly; testing conformance against the standards is challenging; and understanding the many obscure corner cases requires considerable expertise. Ideally we would have the best of both worlds: protocol descriptions that are simultaneously:

  1. clear, accessible to a broad community and easy to modify;
  2. unambiguous, characterising exactly what behaviour is specified;
  3. sufficiently loose, characterising exactly what is not specified (especially, permitting high-performance implementations without over-constraining their structure); and
  4. directly usable as a basis for conformance testing, not read-and-forget documents.
In this work we have established a practical technique for rigorous protocol specification, in HOL, that makes this ideal attainable for protocols as complex as TCP. To develop the technique, and to demonstrate its feasibility, we have produced a post-hoc specification of existing protocols: a mathematically rigorous and experimentally-validated characterisation of the behaviour of TCP, UDP, and the Sockets API, as implemented in practice. The specification has been extensively annotated to make it usable as a reference for TCP/IP stack implementors and Sockets API users. It can also provide a basis for high-fidelity conformance testing of future implementations. Perhaps more significantly, the work demonstrates that it would be feasible and desirable to carry out similar rigorous specification work for new protocols, in a tolerably light-weight style, both at design-time and during standardisation. We discuss some simple ways in which protocols could be designed to make testing computationally straightforward.

Further details are available from the Netsem page.