TY - GEN
T1 - Engineering with logic
T2 - HOL specification and symbolic-evaluation testing for TCP implementations
AU - Bishop, Steve
AU - Fairbairn, Matthew
AU - Norrish, Michael
AU - Sewell, Peter
AU - Smith, Michael
AU - Wansbrough, Keith
PY - 2006
Y1 - 2006
N2 - 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 15 000-20 000 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.
AB - 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 15 000-20 000 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.
KW - API
KW - Conformance testing
KW - HOL
KW - Higher-order logic
KW - Network protocols
KW - Operational semantics
KW - Sockets
KW - Specification
KW - TCP/IP
UR - http://www.scopus.com/inward/record.url?scp=33745830534&partnerID=8YFLogxK
M3 - Conference contribution
SN - 1595930272
SN - 9781595930279
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 55
EP - 66
BT - Conference Record of POPL 2006
ER -