标题： 需要一个村庄：弥合协议当前规范与正式规范之间的差距 显示英文标题

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

摘要： 形式规范对网络协议的设计者和使用者都有许多好处。它们提供了清晰、无歧义的表示，这些表示作为文档和测试很有用。它们可以帮助揭示关于协议“是什么”的分歧，并确定需要进一步工作以解决模糊性或内部不一致的领域。它们还为形式推理提供了基础，使得可以在所有输入和每个环境中建立重要的安全性和正确性保证。尽管有这些优势，但目前形式化方法并未广泛用于设计、实现和验证网络协议。相反，互联网协议通常在非正式文档中描述，例如IETF请求评论（RFC）或IEEE标准。这些文档主要由冗长的文本描述组成，配有伪代码、头描述、状态机图和参考实现，这些用于互操作性测试。因此，尽管RFC和参考实现原本只是为了帮助指导协议设计者使用的社会过程，但它们已经演变为互联网社区中最接近形式规范的东西。在本文中，我们讨论了规范在网络和形式化方法社区中的不同作用。然后，我们展示了形式化指定协议的潜在好处，并介绍了几个最近成功案例的亮点。最后，我们指出了两个社区对形式规范的不同理解，并提出了可能的策略来弥合这些差距。 显示英文摘要

摘要： 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.