It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols

Abstract

Formal specifications have numerous benefits for both designers and users of network protocols. They provide clear, unambiguous representations, which are useful as documentation and for testing. They can help reveal disagreements about what a protocol "is" and identify areas where further work is needed to resolve ambiguities or internal inconsistencies. They also provide a foundation for formal reasoning, making it possible to establish important security and correctness guarantees on all inputs and in every environment. Despite these advantages, formal methods are not widely used to design, implement, and validate network protocols today. Instead, Internet protocols are usually described in informal documents, such as IETF Requests for Comments (RFCs) or IEEE standards. These documents primarily consist of lengthy prose descriptions, accompanied by pseudocode, header descriptions, state machine diagrams, and reference implementations which are used for interoperability testing. So, while RFCs and reference implementations were only intended to help guide the social process used by protocol designers, they have evolved into the closest things to formal specifications the Internet community has. In this paper, we discuss the different roles that specifications play in the networking and formal methods communities. We then illustrate the potential benefits of specifying protocols formally, presenting highlights from several recent success stories. Finally, we identify key differences between how formal specifications are understood by the two communities and suggest possible strategies to bridge the gaps.