Trustworthy Systems

Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations

Authors

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

University of Cambridge

NICTA

Australian National University

Abstract

The TCP/IP protocols and Sockets API underlie much of modern computation, but their semantics have historically been very complex and ill-defined. The real standard is the de facto one of the common implementations, including, for example, the 15000–20000 lines of C in the BSD implementation. Dealing rigorously with the behaviour of such bodies of code is challenging.

We have recently developed a post-hoc specification of TCP, UDP, and Sockets that is rigorous, detailed, readable, has broad coverage, and is remarkably accurate. In this paper we describe the novel techniques that were required.

Working within a general-purpose proof assistant (HOL), we developed language idioms (within higher-order logic) in which to write the specification: operational semantics with nondeterminism, time, system calls, monadic relational programming, etc. We followed an experimental semantics approach, validating the specification against several thousand traces captured from three implementations (FreeBSD, Linux, and WinXP). Many differences between these were identified, and a number of bugs. Validation was done using a special-purpose symbolic model checker programmed above HOL.

We suggest that similar logic engineering techniques could be applied to future critical software infrastructure at design time, leading to cleaner designs and (via specification-based testing using a similar checker) more predictable implementations

BibTeX Entry

  @inproceedings{Bishop_FNSSW_06,
    address          = {Charleston, South Carolina, USA},
    author           = {Bishop, Steve and Fairbairn, Matthew and Norrish, Michael and Sewell, Peter and Smith, Michael and
                        Wansbrough, Keith},
    booktitle        = {ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
    doi              = {10.1145/1111037.1111043},
    editor           = {{Simon Peyton Jones}},
    keywords         = {network protocols, tcp/ip, sockets, api, specification, conformance testing, higher-order logic,
                        hol, operational semantics},
    month            = jan,
    pages            = {55---66},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/7529.pdf},
    publisher        = {ACM},
    title            = {Engineering with Logic: {HOL} Specification and Symbolic-evaluation Testing for {TCP}
                        Implementations},
    year             = {2006}
  }

Download