Correct implementation of network protocols

A number of issues combine to make network protocol development signif- icantly more difficult than other areas of computer programming: problems with time, concurrency, and failures; interactions between the network proto- col and its environment; and obstacles in developing the protocol over time. In order to address these issues, we introduce the Timed Abstract Pro- tocol notation and the Austin Protocol Compiler. The Timed Abstract Pro- tocol, or TAP, notation is a domain-specific formal language for describing asynchronous message-passing network protocols, with two execution models: an abstract execution model and a concrete execution model. The abstract execution model is suited for protocol design, comprehension, and correctness verification. The concrete execution model is suited for protocol implementa- tion. We show that the two models are equivalent: that a protocol interpreted under the concrete model preserves the intended behavior of the protocol in- terpreted under the abstract model. The Austin Protocol Compiler, or APC, is a system that transforms a protocol given in the Timed Abstract Protocol notation into executable C code and provides a runtime environment for the protocol. In order to demonstrate the effectiveness of the TAP notation and APC, we present implementations of a secure encryption key exchange proto- col, a failure discovery protocol, and a Domain Name System server. While discussing the latter, we examine the performance of the APC implementation and show that it is comparable to two other DNS servers. The combination of the Timed Abstract Protocol notation and the Austin Protocol Compiler addresses the issues of network protocol develop- ment by allowing precise and verifiable descriptions of protocols which can be made executable easily, in order both to gain experimental experience and to provide reference implementations.