[TYPES] Rigorous HOL specification for TCP, UDP, and Sockets

[Peter Sewell]

Dear TYPES readers,

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

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

available from <http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html>.  
They give a semantics, expressed in the typed higher-order logic of
the HOL system, for the common real-world network protocols and their
API.  The abstract is below.

That web page also contains a paper demonstrating reasoning about
an executable version of a distributed algorithm, written in an OCaml
fragment, above an earlier version of the specification:

  Stenning's Protocol Implemented in UDP and Verified in Isabelle.
  Michael Compton. The Australasian Theory Symposium, Jan 2005.

Comments and feedback would be very welcome, on both usability and content.

Peter


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

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.