{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:56:41Z","timestamp":1770296201950,"version":"3.49.0"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"DTU Nordic Five Tech Alliance","award":["Safe and secure software-defined networks in P4"],"award-info":[{"award-number":["Safe and secure software-defined networks in P4"]}]},{"name":"Horizon Europe","award":["101093006 TaRDIS"],"award-info":[{"award-number":["101093006 TaRDIS"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>\n            Software-Defined Networking (SDN) significantly simplifies programming, reconfiguring, and optimizing network devices, such as switches and routers. The\n            <jats:italic>de facto<\/jats:italic>\n            standard for programming SDN devices is the P4 language. However, the flexibility and power of P4, and SDN more generally, gives rise to important risks. As a number of incidents at major cloud providers have shown, errors in SDN programs can compromise the availability of networks, leaving them in a non-functional state. The focus of this paper are errors in control-plane programs that interact with P4-enabled network devices via the standardized P4Runtime API. For clients of the P4Runtime API it is easy to make mistakes that may lead to catastrophic failures, despite the use of Google\u2019s Protocol Buffers as an interface definition language.\n          <\/jats:p>\n          <jats:p>\n            This paper proposes P4R-Type, a novel verified P4Runtime API for Scala that performs static checks for P4 control plane operations, ruling out mismatches between P4 tables, allowed actions, and action parameters. As a formal foundation of P4R-Type, we present the\n            <jats:italic>F<\/jats:italic>\n            <jats:sub>P4R<\/jats:sub>\n            calculus and its typing system, which ensure that well-typed programs never get stuck by issuing invalid P4Runtime operations. We evaluate the safety and flexibility of P4R-Type with 3 case studies. To the best of our knowledge, this is the first work that formalises P4Runtime control plane applications, and a typing discipline ensuring the correctness of P4Runtime operations.\n          <\/jats:p>","DOI":"10.1145\/3622866","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"1935-1963","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["P4R-Type: A Verified API for P4 Control Plane Programs"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-4039-3808","authenticated-orcid":false,"given":"Jens Kanstrup","family":"Larsen","sequence":"first","affiliation":[{"name":"DTU, Kongens Lyngby, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8069-6495","authenticated-orcid":false,"given":"Roberto","family":"Guanciale","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2659-5271","authenticated-orcid":false,"given":"Philipp","family":"Haller","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1153-6164","authenticated-orcid":false,"given":"Alceste","family":"Scalas","sequence":"additional","affiliation":[{"name":"DTU, Kongens Lyngby, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 5th International Workshop on P4 in Europe. 39\u201345","author":"Alshnakat Anoud","year":"2022","unstructured":"Anoud Alshnakat , Didrik Lundberg , Roberto Guanciale , Mads Dam , and Karl Palmskog . 2022 . HOL4P4: semantics for a verified data plane . In Proceedings of the 5th International Workshop on P4 in Europe. 39\u201345 . Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam, and Karl Palmskog. 2022. HOL4P4: semantics for a verified data plane. In Proceedings of the 5th International Workshop on P4 in Europe. 39\u201345."},{"key":"e_1_2_1_2_1","volume-title":"NetKAT: Semantic foundations for networks. Acm sigplan notices, 49, 1","author":"Anderson Carolyn Jane","year":"2014","unstructured":"Carolyn Jane Anderson , Nate Foster , Arjun Guha , Jean-Baptiste Jeannin , Dexter Kozen , Cole Schlesinger , and David Walker . 2014. NetKAT: Semantic foundations for networks. Acm sigplan notices, 49, 1 ( 2014 ), 113\u2013126. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. 2014. NetKAT: Semantic foundations for networks. Acm sigplan notices, 49, 1 (2014), 113\u2013126."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2020.2995849"},{"key":"e_1_2_1_4_1","volume-title":"2021 51st Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN). 101\u2013115","author":"Bhardwaj Ayush","year":"2021","unstructured":"Ayush Bhardwaj , Zhenyu Zhou , and Theophilus A Benson . 2021 . A Comprehensive Study of Bugs in Software Defined Networks . In 2021 51st Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN). 101\u2013115 . Ayush Bhardwaj, Zhenyu Zhou, and Theophilus A Benson. 2021. A Comprehensive Study of Bugs in Software Defined Networks. In 2021 51st Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN). 101\u2013115."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498698"},{"key":"e_1_2_1_6_1","volume-title":"Mohammad Reza Mousavi, and H\u00fcnkar Can Tun\u00e7","author":"Caltais Georgiana","year":"2022","unstructured":"Georgiana Caltais , Hossein Hojjat , Mohammad Reza Mousavi, and H\u00fcnkar Can Tun\u00e7 . 2022 . DyNetKAT: An algebra of dynamic networks. In Foundations of Software Science and Computation Structures: 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2\u20137, 2022, Proceedings . 184\u2013204. Georgiana Caltais, Hossein Hojjat, Mohammad Reza Mousavi, and H\u00fcnkar Can Tun\u00e7. 2022. DyNetKAT: An algebra of dynamic networks. In Foundations of Software Science and Computation Structures: 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2\u20137, 2022, Proceedings. 184\u2013204."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1013"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434322"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498701"},{"key":"e_1_2_1_10_1","volume-title":"12th $USENIX$ symposium on networked systems design and implementation ($NSDI$ 15). 469\u2013483.","author":"Fogel Ari","unstructured":"Ari Fogel , Stanley Fung , Luis Pedrosa , Meg Walraed-Sullivan , Ramesh Govindan , Ratul Mahajan , and Todd Millstein . 2015. A general approach to network configuration analysis . In 12th $USENIX$ symposium on networked systems design and implementation ($NSDI$ 15). 469\u2013483. Ari Fogel, Stanley Fung, Luis Pedrosa, Meg Walraed-Sullivan, Ramesh Govindan, Ratul Mahajan, and Todd Millstein. 2015. A general approach to network configuration analysis. In 12th $USENIX$ symposium on networked systems design and implementation ($NSDI$ 15). 469\u2013483."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TMM.2019.2893549"},{"key":"e_1_2_1_12_1","volume-title":"Presented as part of the 9th $USENIX$ Symposium on Networked Systems Design and Implementation ($NSDI$ 12). 113\u2013126.","author":"Kazemian Peyman","unstructured":"Peyman Kazemian , George Varghese , and Nick McKeown . 2012. Header space analysis: Static checking for networks . In Presented as part of the 9th $USENIX$ Symposium on Networked Systems Design and Implementation ($NSDI$ 12). 113\u2013126. Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header space analysis: Static checking for networks. In Presented as part of the 9th $USENIX$ Symposium on Networked Systems Design and Implementation ($NSDI$ 12). 113\u2013126."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491185.2491199"},{"key":"e_1_2_1_14_1","volume-title":"echnical Report)","author":"Larsen Jens Kanstrup","unstructured":"Jens Kanstrup Larsen , Roberto Guanciale , Philipp Haller , and Alceste Scalas . 2023. P4R-Type: a Verified API for P4 Control Plane Programs ( T echnical Report) . Technical University of Denmark and KTH Royal Institute of Technology . arxiv:2309.03566 Jens Kanstrup Larsen, Roberto Guanciale, Philipp Haller, and Alceste Scalas. 2023. P4R-Type: a Verified API for P4 Control Plane Programs (Technical Report). Technical University of Denmark and KTH Royal Institute of Technology. arxiv:2309.03566"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 2018 Conference of the ACM Special Interest Group on data communication. 490\u2013503","author":"Liu Jed","year":"2018","unstructured":"Jed Liu , William Hallahan , Cole Schlesinger , Milad Sharif , Jeongkeun Lee , Robert Soul\u00e9 , Han Wang , C\u0103lin Ca\u015fcaval , Nick McKeown , and Nate Foster . 2018 . P4v: Practical verification for programmable data planes . In Proceedings of the 2018 Conference of the ACM Special Interest Group on data communication. 490\u2013503 . Jed Liu, William Hallahan, Cole Schlesinger, Milad Sharif, Jeongkeun Lee, Robert Soul\u00e9, Han Wang, C\u0103lin Ca\u015fcaval, Nick McKeown, and Nate Foster. 2018. P4v: Practical verification for programmable data planes. In Proceedings of the 2018 Conference of the ACM Special Interest Group on data communication. 490\u2013503."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1355734.1355746"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the Symposium on SDN Research. 1\u20137.","author":"N\u00f6tzli Andres","year":"2018","unstructured":"Andres N\u00f6tzli , Jehandad Khan , Andy Fingerhut , Clark Barrett , and Peter Athanas . 2018 . P4pktgen: Automated test case generation for p4 programs . In Proceedings of the Symposium on SDN Research. 1\u20137. Andres N\u00f6tzli, Jehandad Khan, Andy Fingerhut, Clark Barrett, and Peter Athanas. 2018. P4pktgen: Automated test case generation for p4 programs. In Proceedings of the Symposium on SDN Research. 1\u20137."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/MCOM.2017.1600935"},{"key":"e_1_2_1_19_1","volume-title":"P4 Language Specification. https:\/\/p4.org\/p4-spec\/docs\/P4-16-v-1.2.3.html [Online","author":"P4.org Working Group","year":"2022","unstructured":"P4.org Working Group . 2020. P4 Language Specification. https:\/\/p4.org\/p4-spec\/docs\/P4-16-v-1.2.3.html [Online ; accessed 2022 -07-11] P4.org Working Group. 2020. P4 Language Specification. https:\/\/p4.org\/p4-spec\/docs\/P4-16-v-1.2.3.html [Online; accessed 2022-07-11]"},{"key":"e_1_2_1_20_1","volume-title":"https:\/\/p4.org\/p4-spec\/p4runtime\/v1.3.0\/P4Runtime-Spec.html [Online","author":"P4.org Working Group","year":"2023","unstructured":"P4.org Working Group . 2020. P4 Runtime Specification . https:\/\/p4.org\/p4-spec\/p4runtime\/v1.3.0\/P4Runtime-Spec.html [Online ; accessed 2023 -04-12] P4.org Working Group. 2020. P4Runtime Specification. https:\/\/p4.org\/p4-spec\/p4runtime\/v1.3.0\/P4Runtime-Spec.html [Online; accessed 2023-04-12]"},{"key":"e_1_2_1_21_1","volume-title":"https:\/\/github.com\/p4lang\/tutorials\/tree\/master\/exercises\/p4runtime [Online","author":"P4.org Working Group","year":"2023","unstructured":"P4.org Working Group . 2023. P4 Tutorial. https:\/\/github.com\/p4lang\/tutorials\/tree\/master\/exercises\/p4runtime [Online ; accessed 2023 -08-10] P4.org Working Group. 2023. P4 Tutorial. https:\/\/github.com\/p4lang\/tutorials\/tree\/master\/exercises\/p4runtime [Online; accessed 2023-08-10]"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575670"},{"key":"e_1_2_1_23_1","volume-title":"The \u03c0 -calculus: a Theory of Mobile Processes","author":"Sangiorgi Davide","unstructured":"Davide Sangiorgi and David Walker . 2001. The \u03c0 -calculus: a Theory of Mobile Processes . Cambridge University Press . Davide Sangiorgi and David Walker. 2001. The \u03c0 -calculus: a Theory of Mobile Processes. Cambridge University Press."},{"key":"e_1_2_1_24_1","unstructured":"Simon Sharwood. 2016. Google cloud wobbles as workers patch wrong routers. https:\/\/www.theregister.com\/2016\/03\/01\/google_cloud_wobbles_as_workers_patch_wrong_routers\/ Accessed 2023-04-11 \t\t\t\t  Simon Sharwood. 2016. Google cloud wobbles as workers patch wrong routers. https:\/\/www.theregister.com\/2016\/03\/01\/google_cloud_wobbles_as_workers_patch_wrong_routers\/ Accessed 2023-04-11"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2020.2999653"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230548"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622866","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622866","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:27Z","timestamp":1750298247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622866"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":26,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622866"],"URL":"https:\/\/doi.org\/10.1145\/3622866","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}