Trustworthy Systems

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

Authors

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

University of Cambridge

NICTA

Australian National University

Abstract

Network protocols are hard to implement correctly. Despite the existence of RFCs and other standards, implementations often have subtle differences and bugs. One reason for this is that the specifications are typically informal, and hence inevitably contain ambiguities. Conformance testing against such specifications is challenging.

In this paper we present a practical technique for rigorous protocol specification that supports specification-based testing. We have applied it to TCP, UDP, and the Sockets API, developing a detailed ‘post-hoc’ specification that accurately reflects the behaviour of several existing implementations (FreeBSD 4.6, Linux 2.4.20-8, and Windows XP SP1). The development process uncovered a number of differences between and infelicities in these implementations.

Our experience shows for the first time that rigorous specification is feasible for protocols as complex as TCP. We argue that the technique is also applicable ‘pre-hoc’, in the design phase of 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.

BibTeX Entry

  @inproceedings{Bishop_FNSSW_05,
    address          = {Philadelphia},
    author           = {Bishop, Steve and Fairbairn, Matthew and Norrish, Michael and Sewell, Peter and Smith, Michael and
                        Wansbrough, Keith},
    booktitle        = {ACM Conference on Communications},
    doi              = {10.1145/1080091.1080123},
    editor           = {{Ramesh Govindan and Greg Minshall}},
    keywords         = {network protocols, tcp/ip, sockets, api, specification, conformance testing, higher-order logic,
                        hol, operational semantics},
    month            = aug,
    pages            = {265--276},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/7530.pdf},
    publisher        = {ACM},
    title            = {Rigorous Specification and Conformance Testing Techniques for Network Protocols, as applied to
                        {TCP}, {UDP}, and Sockets},
    year             = {2005}
  }

Download