[e2e] Rigorous specification for TCP, UDP, and Sockets

[Peter Sewell]

We would like to announce the technical reports

  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

and the summary paper

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

available from <http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html>.

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


%%%%%%%%%%%%%%

Abstract

We have developed a mathematically rigorous and
experimentally-validated post-hoc specification of the behaviour of
TCP, UDP, and the Sockets API. It characterises the API and
network-interface interactions of a host, using operational semantics
in the higher-order logic of the HOL automated proof assistant. The
specification is detailed, covering almost all the information of the
real-world communications: it is in terms of individual TCP segments
and UDP datagrams, though it abstracts from the internals of IP. It
has broad coverage, dealing with arbitrary API call sequences and
incoming messages, not just some well-behaved usage. It is also
accurate, closely based on the de facto standard of (three of) the
widely-deployed implementations. To ensure this we have adopted a
novel experimental semantics approach, developing test generation
tools and symbolic higher-order-logic model checking techniques that
let us validate the specification directly against several thousand
traces captured from the implementations.

The resulting specification, which is annotated for the
non-HOL-specialist reader, may be useful as an informal reference for
TCP/IP stack implementors and Sockets API users, supplementing the
existing informal standards and texts. It can also provide a basis for
high-fidelity automated testing of future implementations, and a basis
for design and formal proof of higher-level communication layers. More
generally, the work demonstrates that it is feasible to carry out
similar rigorous specification work at design-time for new
protocols. We discuss how such a design-for-test approach should
influence protocol development, leading to protocol specifications
that are both unambiguous and clear, and to high-quality
implementations that can be tested directly against those
specifications.

Volume 1 gives an overview of the project, discussing the goals and
techniques and giving an introduction to the specification. The
specification itself is given in the companion Volume 2, which is
automatically typeset from the (extensively annotated) HOL source. As
far as possible we have tried to make the work accessible to four
groups of intended readers: workers in networking (implementors of
TCP/IP stacks, and designers of new protocols); in distributed systems
(implementors of software above the Sockets API); in distributed
algorithms (for whom this may make it possible to prove properties
about executable implementations of those algorithms); and in
semantics and automated reasoning.

--  
Peter Sewell  
University of Cambridge Computer Laboratory