Rigorous specification for TCP, UDP, and Sockets

[Peter Sewell]

[apologies to anyone who has seen this on the end-to-end list]


Our recent technical reports may be of interest to BSD TCP/IP developers:

  TCP, UDP, and Sockets: rigorous and experimentally-validated
  behavioural specification.

  Volume 1: Overview               UCAM-CL-TR-624
  Volume 2: The Specification      UCAM-CL-TR-625

They are available from <http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html>
together with the summary paper:

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


These give a detailed and precise specification of the behaviour of
three common TCP/IP stacks - versions of FreeBSD, Linux, and Windows
XP - as seen from socket calls and the wire interface.  The
specification has been validated through extensive testing (primarily
against FreeBSD for the TCP aspects).  It models the actual observed
behaviour, bugs and all, rather than an idealisation of the RFCs.

The specification is annotated for the non-specialist reader, and we
hope that it will be useful as an informal reference for stack
implementors and for sockets users (supplementing the existing RFCs
and books), as well as supporting automated conformance testing.  Our
techniques may be useful in the development of new protocols and
extensions.

We would greatly appreciate feedback, on both content and usability.


Peter, for the Netsem team:

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