{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T18:32:56Z","timestamp":1754159576680,"version":"3.41.2"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"8","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2025,8]]},"abstract":"<jats:p>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 \u201cis\u201d 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.<\/jats:p>\n          <jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>","DOI":"10.1145\/3706572","type":"journal-article","created":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T14:35:18Z","timestamp":1753281318000},"page":"50-61","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols"],"prefix":"10.1145","volume":"68","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2952-939X","authenticated-orcid":false,"given":"David","family":"Basin","sequence":"first","affiliation":[{"name":"ETH Zurich, Dept. Computer Science, Zurich, Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6557-684X","authenticated-orcid":false,"given":"Nate","family":"Foster","sequence":"additional","affiliation":[{"name":"Cornell University, Computer Science, Ithaca, New York, United States"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-9380-1939","authenticated-orcid":false,"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin, Computer Science, Austin, Texas, United States"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6379-2442","authenticated-orcid":false,"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[{"name":"Nokia Bell Labs, Murray Hill, New Jersey, United States"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9649-6789","authenticated-orcid":false,"given":"Cristina","family":"Nita-Rotaru","sequence":"additional","affiliation":[{"name":"Northeastern University - Boston Campus, Computer Science, Boston, Massachusetts, United States"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3309-6603","authenticated-orcid":false,"given":"Jonathan M.","family":"Smith","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Computer Science, Philadelphia, Pennsylvania, United States"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6568-2052","authenticated-orcid":false,"given":"Pamela","family":"Zave","sequence":"additional","affiliation":[{"name":"Princeton University, Computer Science, Princeton, New Jersey, United States"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3613-1208","authenticated-orcid":false,"given":"Lenore D.","family":"Zuck","sequence":"additional","affiliation":[{"name":"University of Illinois Chicago, Computer Science, Chicago, Illinois, United States"}]}],"member":"320","published-online":{"date-parts":[[2025,7,25]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/65.690959"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/65.690960"},{"key":"e_1_3_1_4_2","doi-asserted-by":"crossref","unstructured":"Alexander D.S. Shaw M. Nettles S.M. and Smith J.M. Active bridging. In Proceedings of the ACM SIGCOMM Conf. on\u00a0Applications Technologies Architectures and Protocols for Computer Communication (1997) \u00a0101\u2013111.","DOI":"10.1145\/263105.263149"},{"key":"e_1_3_1_5_2","doi-asserted-by":"crossref","unstructured":"Anderson C.J. et al. NetKAT: Semantic foundations for networks. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (2014) \u00a0113\u2013126.","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_1_6_2","doi-asserted-by":"crossref","unstructured":"Basin D. et al. A formal analysis of 5G authentication. In Proceedings of the 2018 ACM SIGSAC Conf. on Computer and Communications Security (2018) \u00a01383\u20131396.","DOI":"10.1145\/3243734.3243846"},{"key":"e_1_3_1_7_2","unstructured":"Basin D.A. Sasse R. and Toro-Pozo J. Card brand mixup attack: Bypassing the PIN in non-visa cards by using them for Visa transactions. In Proceedings of the 30th USENIX Security Symp. (2021) \u00a0179\u2013194."},{"key":"e_1_3_1_8_2","doi-asserted-by":"crossref","unstructured":"Basin D.A. Sasse R. and Toro-Pozo J. The EMV standard: Break fix verify. In Proceedings of the IEEE Symp. Security and Privacy (2021) \u00a01766\u20131781.","DOI":"10.1109\/SP40001.2021.00037"},{"key":"e_1_3_1_9_2","doi-asserted-by":"crossref","unstructured":"Bhargavan K. Blanchet B. and Kobeissi N. Verified models and reference implementations for the TLS 1.3 standard candidate. In Proceedings of the IEEE Symp. Security Security and Privacy (2017) \u00a0483\u2013502.","DOI":"10.1109\/SP.2017.26"},{"key":"e_1_3_1_10_2","doi-asserted-by":"crossref","unstructured":"Bhargavan K. et al. Implementing TLS with verified cryptographic security. In Proceedings of the IEEE Symp. Security and Privacy (2013) \u00a0445\u2013459.","DOI":"10.1109\/SP.2013.37"},{"key":"e_1_3_1_11_2","doi-asserted-by":"crossref","unstructured":"Bond G.W. Cheung E. Smith T.M. and Zave P. Specification and evaluation of transparent behavior for SIP back-to-back user agents. In Proceedings of IPTComm (2010) \u00a048\u201358.","DOI":"10.1145\/1941530.1941538"},{"key":"e_1_3_1_12_2","doi-asserted-by":"crossref","unstructured":"Braden R.T. Requirements for Internet Hosts\u2014Communication Layers. RFC 1122 (Oct. 1989).","DOI":"10.17487\/rfc1122"},{"key":"e_1_3_1_13_2","doi-asserted-by":"crossref","unstructured":"Cremers C. et al. A comprehensive symbolic analysis of TLS 1.3. In Proceedings of the 2017 ACM SIGSAC Conf. on Computer and Communications Security \u00a01773\u20131788.","DOI":"10.1145\/3133956.3134063"},{"key":"e_1_3_1_14_2","doi-asserted-by":"crossref","unstructured":"Delignat-Lavaud A. et al. Implementing and proving the TLS 1.3 record layer. In Proceedings of the IEEE Security and Privacy Symp. (2017) \u00a0463\u2013482.","DOI":"10.1109\/SP.2017.58"},{"key":"e_1_3_1_15_2","doi-asserted-by":"crossref","unstructured":"Eddy W. Transmission Control Protocol (TCP). RFC 9293 (Aug. 2022).","DOI":"10.17487\/RFC9293"},{"key":"e_1_3_1_16_2","unstructured":"Fogel A. et al. A general approach to network configuration analysis. In Proceedings of the USENIX Conf. NSDI (2015) \u00a0469\u2013483."},{"key":"e_1_3_1_17_2","doi-asserted-by":"crossref","unstructured":"Hasebe M. et al. Example call flows of race conditions in the Session Initiation Protocol (SIP). RFC 5407 Dec. 2008.","DOI":"10.17487\/rfc5407"},{"key":"e_1_3_1_18_2","unstructured":"Holzmann G.J. The theory and practice of a formal method: NewCoRe. In Proceedings of the\u00a0IFIP World Computer Congress (1994) \u00a035\u201344."},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/383059.383071"},{"key":"e_1_3_1_20_2","unstructured":"Kazemian P. Varghese G. and McKeown N. Header space analysis: Static checking for networks. In Proceedings of the\u00a0USENIX NSDI Symp. (2012) \u00a0113\u2013126."},{"key":"e_1_3_1_21_2","unstructured":"Khurshid A. et al. VeriFlow: Verifying Network-Wide invariants in real time. In Proceedings of the\u00a0USENIX NSDI Symp. (2013) \u00a015\u201327."},{"key":"e_1_3_1_22_2","first-page":"490","article-title":"p4v: practical verification for programmable data planes","author":"Liu J.","year":"2018","unstructured":"Liu, J. et al. p4v: practical verification for programmable data planes. In Proceedings of the\u00a0ACM SIGCOMM Conf. (2018),\u00a0490\u2013503.","journal-title":"Proceedings of the\u00a0"},{"key":"e_1_3_1_23_2","doi-asserted-by":"crossref","unstructured":"Maenpaa J. and Camarillo G. Self-tuning distributed hash table (DHT) for REsource LOcation And Discovery (RELOAD). RFC 7363 (Sept. 2014).","DOI":"10.17487\/rfc7363"},{"key":"e_1_3_1_24_2","doi-asserted-by":"crossref","unstructured":"McMillan K.L. and Zuck L.D. Compositional testing of Internet protocols. In Proceedings of IEEE Cybersecurity Development Conf. (2019) \u00a0161\u2013174.","DOI":"10.1109\/SecDev.2019.00031"},{"key":"e_1_3_1_25_2","doi-asserted-by":"crossref","unstructured":"McMillan K.L. and Zuck L.D. Formal specification and testing of QUIC. In Proceedings of ACM SIGCOMM (2019) \u00a0227\u2013240.","DOI":"10.1145\/3341302.3342087"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_3_1_27_2","doi-asserted-by":"crossref","unstructured":"Pacheco M.L. et al. Automated attack synthesis by extracting finite state machines from protocol specification documents. In Proceedings of the IEEE Security and Privacy Symp. (2022) \u00a051\u201368.","DOI":"10.1109\/SP46214.2022.9833673"},{"key":"e_1_3_1_28_2","unstructured":"Pirelli S. Valentukonyt\u0117 A. Argyraki K. and Candea G. Automated verification of network function binaries. In Proceedings of the USENIX NSDI Symp. (2022) \u00a0585\u2013600."},{"key":"e_1_3_1_29_2","doi-asserted-by":"crossref","unstructured":"Postel J. Transmission Control Protocol. RFC 793 Sept. 1981.","DOI":"10.17487\/rfc0793"},{"key":"e_1_3_1_30_2","doi-asserted-by":"crossref","unstructured":"Renganathan S. et al. Hydra: Effective runtime network verification. In Proceedings of the ACM SIGCOMM Conf. (2023) \u00a0182\u2013194.","DOI":"10.1145\/3603269.3604856"},{"key":"e_1_3_1_31_2","unstructured":"Rescorla E. and Dierks T. The Transport Layer Security (TLS) Protocol Version 1.2. RFC 5246\u00a0(Aug. 2008)."},{"key":"e_1_3_1_32_2","doi-asserted-by":"crossref","unstructured":"Rosenberg J. A hitchhiker\u2019s guide to the Session Initiation Protocol (SIP). RFC 5411\u00a0(Jan. 2009).","DOI":"10.17487\/rfc5411"},{"key":"e_1_3_1_33_2","doi-asserted-by":"crossref","unstructured":"Rosenberg J. et al. SIP: Session Initiation Protocol. RFC 3261 June 2002.","DOI":"10.17487\/rfc3261"},{"key":"e_1_3_1_34_2","doi-asserted-by":"crossref","unstructured":"Ruffy F. et al. P4testgen: An extensible test oracle for p4. In Proceedings of the ACM SIGCOMM Conf. (2023) \u00a0136\u2013151.","DOI":"10.1145\/3603269.3604834"},{"key":"e_1_3_1_35_2","doi-asserted-by":"crossref","unstructured":"Xie G.G. et al. On static reachability analysis of IP networks. In Proceedings of the IEEE Joint Conf. INFOCOMM (2005) \u00a02170\u20132183.","DOI":"10.1109\/INFCOM.2005.1498492"},{"key":"e_1_3_1_36_2","doi-asserted-by":"crossref","unstructured":"Yang H. and Lam S.S. Real-time verification of network properties using atomic predicates. In IEEE\/ACM Trans. Networking\u00a0(2013) \u00a01\u201311.","DOI":"10.1109\/ICNP.2013.6733614"},{"key":"e_1_3_1_37_2","doi-asserted-by":"crossref","unstructured":"Zave P. Understanding SIP through model-checking. In Proceedings of Principles Systems and Applications of IP Telecommunications: IPTComm 2008 \u00a0256\u2013279.","DOI":"10.1007\/978-3-540-89054-6_13"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/2185376.2185383"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2655056"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-66673-5_15"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-75778-5_16"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3706572","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,25]],"date-time":"2025-07-25T14:17:20Z","timestamp":1753453040000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3706572"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,25]]},"references-count":40,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2025,8]]}},"alternative-id":["10.1145\/3706572"],"URL":"https:\/\/doi.org\/10.1145\/3706572","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"type":"print","value":"0001-0782"},{"type":"electronic","value":"1557-7317"}],"subject":[],"published":{"date-parts":[[2025,7,25]]},"assertion":[{"value":"2024-06-07","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-07-25","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}