Stenning's protocol implemented in UDP and verified in Isabelle

摘要

This paper is about the mechanical verification of UDP based network programs. It uses the UDP portion of a formal model of the Internet protocols TCP (Transmission Control Protocol) and UDP (User Datagram Protocol). The model includes asynchronous message passing, message loss and host failure. The model is based around the sockets library, the primary API used for writing UDP and TCP based applications. This paper demonstrates that formal, machine-checked, proof is possible in the UDP model by presenting the proof of a safety property for an implementation of Stenning's Protocol. The protocol is implemented in a fragment of the OCaml language, using the sockets library for UDP network communication. The entire development including the safety proof is carried out in the proof assistant Isabelle; this assures soundness. Thus this paper demonstrates that it is possible to machine verify very concrete representations of distributed programs in a detailed semantics that accurately reflects the programs execution environment. Previously only abstract representations of this protocol have been machine verified. The proof, based on an implementation, provides a contrast to other verifications.