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:
- clear, accessible to a broad community and easy to modify;
- unambiguous, characterising exactly what behaviour is specified;
- sufficiently loose, characterising exactly what is not specified
(especially, permitting high-performance implementations without
over-constraining their structure); and
- 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.
|