The Transmission Control Protocol (TCP) at the heart of TCP/IP protocol stacks is a critical part of our current digital infrastructure. In this article, we show how an existing professional-grade open source embedded TCP/IP library can benefit from a formally verified TCP reimplementation. Our approach is to apply formal verification to the TCP layer only, relying on validated models of the lower layers on which it depends. We translated the TCP user functions into SPARK and modeled asynchronous events with ghost code. This enabled the detection of two bugs in the original C implementation related to memory management and concurrency. The translated code has been proven to be free of run-time errors and to respect the transitions of the TCP state machine, specified in RFC 793. For the lower layers, we used symbolic execution with KLEE to formally verify the contracts used in SPARK to model the corresponding behavior. This work is a step towards a more secure implementation for TCP.
This paper is copyrighted by IEEE, and reproduced here with their permission.