Specifying and Verifying a Real-World Packet Error-Correction System

Automated and semi-automated formal methods have been widely employed to verify properties of network models and per-packet network functions, which operate on single packets in the middle of a network (firewall, NAT, etc.). But these methods do not extend to end-to-end network functions, those whose specification relates a stream of packets sent at one endpoint of the network with a stream received at the other end. Among other complications, such specifications must account for the network's behavior, including packet reordering, duplication, delay, and loss. We develop a methodology for formally specifying and verifying such code, demonstrating our techniques on a real-world packet error-correction system that encounters all of these challenges and whose specification had been highly unclear. We prove a close model of this system correct in the Coq proof assistant; along the way, we formalize more general networking constructs including IP/UDP packets, a metric for packet reordering, and sequence number comparison. Finally, through our specification, we develop an improved version of the error-correction system, giving a more predictable, provably correct program that recovers more packets. We show that formal specification and verification can be powerful tools to clarify assumptions, improve code quality, and find and fix bugs in complex, real-world systems.