Abstract
Despite more then 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and executable code. In part this is because the scale and complexity of these protocols makes them challenging targets for formalization.
In this paper we show how these difficulties can be addressed. We develop a high-level specification for TCP and the Sockets API, expressed in the HOL proof assistant, describing the byte-stream service that TCP provides to users. This complements our previous low-level specification of the protocol internals, and makes it possible for the first time to state what it means for TCP to be correct: that the protocol implements the service. We define a precise abstraction function between the models and validate it by testing, using verified testing infrastructure within HOL. This is a pragmatic alternative to full proof, providing reasonable confidence at a relatively low entry cost.
Together with our previous validation of the low-level model, this shows how one can rigorously tie together concrete implementations, low-level protocol models, and specifications of the services they claim to provide, dealing with the complexity of real-world protocols throughout.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Wang, B.-Y.: Verifying Network Protocol Implementations by Symbolic Refinement Checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 169–181. Springer, Heidelberg (2001)
Biagioni, E.: A structured TCP in Standard ML. In: Proc. SIGCOMM (1994)
Billington, J., Han, B.: On defining the service provided by TCP. In: Proc. ACSC: 26th Australasian Computer Science Conference, Adelaide (2003)
Biltcliffe, A., Dales, M., Jansen, S., Ridge, T., Sewell, P.: Rigorous protocol design in practice: An optical packet-switch MAC in HOL. In: Proc. ICNP (November 2006)
Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., Wansbrough, K.: Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets. In: Proc. SIGCOMM 2005 (August 2005)
Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., Wansbrough, K.: Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations. In: Proc. POPL (2006)
Castelluccia, C., Dabbous, W., O’Malley, S.: Generating efficient protocol code from an abstract specification. IEEE/ACM Trans. Netw. 5(4), 514–524 (1997)
Chkliaev, D., Hooman, J., de Vink, E.: Verification and Improvement of the Sliding Window Protocol. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 113–127. Springer, Heidelberg (2003)
Fersman, E., Jonsson, B.: Abstraction of communication channels in Promela: A case study. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 187–204. Springer, Heidelberg (2000)
Hofmann, R., Lemmen, F.: Specification-driven monitoring of TCP/IP. In: Proc. 8th Euromicro Workshop on Parallel and Distributed Processing (January 2000)
The HOL 4 system, Kananaskis-3 release, http://hol.sourceforge.net
Kohler, E., Kaashoek, M.F., Montgomery, D.R.: A readable TCP in the Prolac protocol language. In: Proc. SIGGCOMM 1999, August 1999, pp. 3–13 (1999)
Li, P., Zdancewic, S.: Combining events and threads for scalable network services. In: Proc. PLDI, pp. 189–199 (2007)
Lynch, N., Vaangdrager, F.: Forward and backward simulations – Part I: Untimed systems. Information and Computation 121(2), 214–233 (1995)
Murphy, S.L., Shankar, A.U.: A verified connection management protocol for the transport layer. In: Proc. SIGCOMM, pp. 110–125 (1987)
Murphy, S.L., Shankar, A.U.: Service specification and protocol construction for the transport layer. In: Proc. SIGCOMM, pp. 88–97 (1988)
Norrish, M., Sewell, P., Wansbrough, K.: Rigour is good for you, and feasible: reflections on formal treatments of C and UDP sockets. In: Proceedings of the 10th ACM SIGOPS European Workshop, September 2002, pp. 49–53 (2002)
Postel, J.: A Graph Model Analysis of Computer Communications Protocols. University of California, Computer Science Department, PhD Thesis (1974)
Schieferdecker, I.: Abruptly-terminated connections in TCP. In: Proc. Int. Workshop on Applied Formal Methods In System Design (1996)
Serjantov, A., Sewell, P., Wansbrough, K.: The UDP calculus: Rigorous semantics for real networking. In: Proc. TACS 2001 (October 2001)
Smith, M.A., Ramakrishnan, K.K.: Formal specification and verification of safety and performance of TCP selective acknowledgment. IEEE/ACM Trans. Netw. 10(2), 193–207 (2002)
Smith, M.A.S.: Formal verification of communication protocols. In: Proc. FORTE IX/PSTV XVI (1996)
The Netsem Project. Web page, http://www.cl.cam.ac.uk/users/pes20/Netsem/
Wansbrough, K., Norrish, M., Sewell, P., Serjantov, A.: Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures. In: Le Métayer, D. (ed.) ESOP 2002 and ETAPS 2002. LNCS, vol. 2305, pp. 278–294. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ridge, T., Norrish, M., Sewell, P. (2008). A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service. In: Cuellar, J., Maibaum, T., Sere, K. (eds) FM 2008: Formal Methods. FM 2008. Lecture Notes in Computer Science, vol 5014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68237-0_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-68237-0_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68235-6
Online ISBN: 978-3-540-68237-0
eBook Packages: Computer ScienceComputer Science (R0)