Engineering TCP/IP with logic
TCP/IP is a complex protocol, which is specified in a series of RFCs. Each RFC is written in English prose, and interpreted differently by different people. Nevertheless, TCP/IP is a widely deployed network protocol nowadays, a lot of people depend on it.
In this talk, I will present a formal model of TCP/IP (developed 2000-2009 and refurbished since 2016), how it can be used to validate the FreeBSD TCP/IP stack, and what we learned while writing it. It is modelled as a label transition system, including timers, retransmission, etc. Hundreds of transition rules are defined to cope with the little details of TCP/IP. We use symbolic execution to validate a trace, which is produced by running a test on a TCP/IP stack, using backtracking which is required to validate some traces.
While formalising TCP in HOL4, roughly 3 dozen anomalies have been discovered, and partially reported upstream. The development of the formal model also lead to an extended and more correct state machine on top of the initial TCP/IP RFC 793.
The resulting model spans over 350 pages, and contains lots of documentation. The pdf is rendered directly from the HOL4 source, the tool HOLDoc was engineered which combined the transition rules and comments into latex code. A recent draft is available at http://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf.
This is joint work with Peter Sewell, Michael Norrish, Tom Ridge, earlier contributors are Steve Bishop, Matthew Fairbairn, Michael Smith, and Keith Wansbrough. The model is available under the 2 clause BSD license at https://github.com/PeterSewell/netsem.
The project website is http://www.cl.cam.ac.uk/~pes20/Netsem/index.html
This session is held on