Document Open Access Logo

NEST: Network Enforced Session Types

Authors Jens Kanstrup Larsen , Alceste Scalas , Guy Amir , Jules Jacobs , Jana Wagemaker , Nate Foster

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2026.17.pdf
  • Filesize: 1.97 MB
  • 31 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
Keywords
  • Session types
  • runtime verification
  • P4
  • programmable data planes

Metrics

Abstract

This paper introduces NEST (Network Enforced Session Types), a runtime verification framework that moves application-level protocol monitoring into the network fabric. Unlike prior work that instruments or wraps application code, we synthesise packet-level monitors that enforce protocols directly in the data plane. We develop algorithms to generate network-level monitors from session types and extend them to handle packet loss and reordering. We implement NEST in P4 and evaluate it on applications including microservice and network-function models, showing that network-level monitors can enforce realistic non-trivial protocols.

Cite As Get BibTex

Jens Kanstrup Larsen, Alceste Scalas, Guy Amir, Jules Jacobs, Jana Wagemaker, and Nate Foster. NEST: Network Enforced Session Types. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 17:1-17:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ECOOP.2026.17

Author Details

Jens Kanstrup Larsen
  • Technical University of Denmark, Copenhagen, Denmark
Alceste Scalas
  • Technical University of Denmark, Copenhagen, Denmark
Guy Amir
  • Cornell University, Ithaca, NY, USA
Jules Jacobs
  • Cornell University, Ithaca, NY, USA
Jana Wagemaker
  • Radboud University, Nijmegen, The Netherlands
Nate Foster
  • EPFL, Lausanne, Switzerland

Funding

Research partially supported by: the DTU Nordic Five Tech Alliance grant "Safe and secure software-defined networks in P4"; the Horizon Europe grant no. 101093006 "TaRDIS"; the Independent Research Fund Denmark project "Hyben"; the DARPA grant no. W912CG-23-C-0032 "LANCER"; and the Dutch research council (NWO) under grant no. VI.Veni.242.134 (VerHyp). The work of Amir was partially supported by a Rothschild Fellowship from Yad Hanadiv (The Rothschild Foundation).

Supplementary Materials

References

  1. Hitesh Ballani, Yatin Chawathe, Sylvia Ratnasamy, Timothy Roscoe, and Scott Shenker. Off by Default! In ACM Workshop on Hot Topics in Networks (HotNets), 2005. URL: https://conferences.sigcomm.org/hotnets/2005/papers/ballani.pdf.
  2. Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. Introduction to runtime verification. In Lectures on Runtime Verification - Introductory and Advanced Topics, volume 10457 of Lecture Notes in Computer Science, pages 1-33. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-75632-5_1.
  3. Massimo Bartoletti, Alceste Scalas, Emilio Tuosto, and Roberto Zunino. Honesty by typing. Logical Methods in Computer Science, 12(4), 2016. URL: https://doi.org/10.2168/LMCS-12(4:7)2016.
  4. Adam D. Barwell, Alceste Scalas, Nobuko Yoshida, and Fangyi Zhou. Generalised multiparty session types with crash-stop failures. In International Conference on Concurrency Theory (CONCUR), volume 243 of LIPIcs, pages 35:1-35:25. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.35.
  5. Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, and Keith Wansbrough. Engineering with logic: Rigorous test-oracle specification and validation for TCP/IP and the sockets API. Journal of the ACM, 66(1):1:1-1:77, 2019. URL: https://doi.org/10.1145/3243650.
  6. Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida. Monitoring networks through multiparty session types. Theoretical Computer Science, 669:33-58, 2017. URL: https://doi.org/10.1016/j.tcs.2017.02.009.
  7. Pat Bosshart, Dan Daly, Glen Gibb, Martin Izzard, Nick McKeown, Jennifer Rexford, Cole Schlesinger, Dan Talayco, Amin Vahdat, George Varghese, and David Walker. P4: programming protocol-independent packet processors. ACM SIGCOMM Computer Communications Review (CCR), 44(3):87-95, 2014. URL: https://doi.org/10.1145/2656877.2656890.
  8. Christian Bartolo Burlò, Adrian Francalanza, and Alceste Scalas. On the monitorability of session types, in theory and practice. In European Conference on Object-Oriented Programming (ECOOP), volume 194 of LIPIcs, pages 20:1-20:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2021.20.
  9. Christian Bartolo Burlò, Adrian Francalanza, Alceste Scalas, Catia Trubiani, and Emilio Tuosto. Towards probabilistic session-type monitoring. In Coordination Models and Languages (COORDINATION), volume 12717 of Lecture Notes in Computer Science, pages 106-120. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-78142-2_7.
  10. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In International Conference on Concurrency Theory (CONCUR), volume 6269 of Lecture Notes in Computer Science, pages 222-236. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_16.
  11. David Castro-Perez, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. Distributed programming using role-parametric session types in Go: Statically-typed endpoint APIs for dynamically-instantiated communication structures. Proceedings of the ACM on Programming Languages (PACMPL), 3(POPL):29:1-29:30, 2019. URL: https://doi.org/10.1145/3290342.
  12. Ruofei Chen, Stephanie Balzer, and Bernardo Toninho. Ferrite: A judgmental embedding of session types in Rust. In European Conference on Object-Oriented Programming (ECOOP), volume 222 of LIPIcs, pages 22:1-22:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2022.22.
  13. P4 Language Consortium. BMv2: P4 reference software switch. Available at https://github.com/p4lang/behavioral-model, 2017.
  14. P4 Language Consortium. P4runtime v1.5.0 specification. Available at https://p4lang.github.io/p4runtime/spec/v1.5.0/P4Runtime-Spec.html, 2026.
  15. Zak Cutner and Nobuko Yoshida. Safe session-based asynchronous coordination in Rust. In Coordination Models and Languages (COORDINATION), volume 12717 of Lecture Notes in Computer Science, pages 80-89. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-78142-2_5.
  16. Zak Cutner, Nobuko Yoshida, and Martin Vassor. Deadlock-free asynchronous message reordering in Rust with multiparty session types. In ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), pages 246-261, 2022. URL: https://doi.org/10.1145/3503221.3508404.
  17. Romain Demangeon, Kohei Honda, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Practical interruptible conversations: Distributed dynamic verification with multiparty session types and Python. Formal Methods in Systems Design, 46(3):197-225, 2015. URL: https://doi.org/10.1007/s10703-014-0218-8.
  18. Romain Demangeon and Nobuko Yoshida. On the expressiveness of multiparty sessions. In Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS), volume 45 of LIPIcs, pages 560-574. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2015.560.
  19. Simon J. Gay and Vasco Thudichum Vasconcelos. Linear type theory for asynchronous session types. Journal of Functional Programming, 20(1):19-50, 2010. URL: https://doi.org/10.1017/S0956796809990268.
  20. Craig Gentry. A fully homomorphic encryption scheme. PhD thesis, Stanford University, USA, 2009. URL: https://searchworks.stanford.edu/view/8493082.
  21. Silvia Ghilezan, Jovanka Pantovic, Ivan Prokic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for asynchronous multiparty sessions. ACM Transactions on Computational Logic, 24(2):14:1-14:73, 2023. URL: https://doi.org/10.1145/3568422.
  22. Saverio Giallorenzo, Jacopo Mauro, Andrea Melis, Fabrizio Montesi, Marco Peressotti, and Marco Prandini. Choreography-defined networks: A case study on DoS mitigation. In Walid Gaaloul, Michael Sheng, Qi Yu, and Sami Yangui, editors, International Conference on Service-Oriented Computing (ICSOC), volume 15405 of Lecture Notes in Computer Science, pages 243-259. Springer, 2024. URL: https://doi.org/10.1007/978-981-96-0808-9_18.
  23. Karuna Grewal, Philip Brighten Godfrey, and Justin Hsu. Expressive policies for microservice networks. In ACM Workshop on Hot Topics in Networks (HotNets), pages 280-286, 2023. URL: https://doi.org/10.1145/3626111.3628181.
  24. Frederik Hauser, Marco Häberle, Mark Schmidt, and Michael Menth. P4-IPsec: Site-to-site and host-to-site VPN with IPsec in P4-based SDN. IEEE Access, 8:139567-139586, 2020. URL: https://doi.org/10.1109/ACCESS.2020.3012738.
  25. Frederik Hauser, Mark Schmidt, Marco Häberle, and Michael Menth. P4-MACsec: Dynamic topology monitoring and data layer protection with MACsec in P4-based SDN. IEEE Access, 8:58845-58858, 2020. URL: https://doi.org/10.1109/ACCESS.2020.2982859.
  26. Kohei Honda. Types for dyadic interaction. In International Conference on Concurrency Theory (CONCUR), volume 715 of Lecture Notes in Computer Science, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  27. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 273-284. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328472.
  28. Raymond Hu, Dimitrios Kouzapas, Olivier Pernet, Nobuko Yoshida, and Kohei Honda. Type-safe eventful sessions in Java. In European Conference on Object-Oriented Programming (ECOOP), volume 6183 of Lecture Notes in Computer Science, pages 329-353. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14107-2_16.
  29. Raymond Hu, Nobuko Yoshida, and Kohei Honda. Session-based distributed programming in Java. In European Conference on Object-Oriented Programming (ECOOP), volume 5142 of Lecture Notes in Computer Science, pages 516-541. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70592-5_22.
  30. Stephen Ibanez, Gordon J. Brebner, Nick McKeown, and Noa Zilberman. The P4->NetFPGA workflow for line-rate packet processing. In ACM SIGDA International Symposium on Field-Programmable Gate Arrays (FPGA), pages 1-9, 2019. URL: https://doi.org/10.1145/3289602.3293924.
  31. Keigo Imai, Nobuko Yoshida, and Shoji Yuen. Session-ocaml: A session-based library with polarities and lenses. Science of Computer Programming, 172:135-159, 2019. URL: https://doi.org/10.1016/j.scico.2018.08.005.
  32. Keigo Imai, Shoji Yuen, and Kiyoshi Agusa. Session type inference in Haskell. In Workshop on Programming Language Approaches to Concurrency and communication-cEntric Software (PLACES), volume 69 of Electronic Proceedings in Theoretical Computer Science, pages 74-91. Open Publishing Association, 2010. URL: https://doi.org/10.4204/EPTCS.69.6.
  33. Istio. Architecture. Available at https://istio.io/latest/docs/ops/deployment/architecture/, 2025.
  34. Istio. Bookinfo Application. Available at https://istio.io/latest/docs/examples/bookinfo/, 2025.
  35. Jana Iyengar and Martin Thomson. QUIC: A UDP-Based Multiplexed and Secure Transport. RFC 9000, May 2021. URL: https://doi.org/10.17487/RFC9000.
  36. Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. Multiparty GV: functional multiparty session types with certified deadlock freedom. Proceedings of the ACM on Programming Languages (PACMPL), 6(ICFP):466-495, 2022. URL: https://doi.org/10.1145/3547638.
  37. Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen. Session types for Rust. In ACM SIGPLAN Workshop on Generic Programming (WGP), pages 13-22, 2015. URL: https://doi.org/10.1145/2808098.2808100.
  38. Xin Jin, Xiaozhou Li, Haoyu Zhang, Robert Soulé, Jeongkeun Lee, Nate Foster, Changhoon Kim, and Ion Stoica. NetCache: Balancing key-value stores with fast in-network caching. In ACM SIGOPS Symposium on Operating Systems Principles (SOSP), pages 121-136, 2017. URL: https://doi.org/10.1145/3132747.3132764.
  39. Andrew Johnson, Ryan Beckett, Xiaoqi Chen, Ratul Mahajan, and David Walker. Sequence abstractions for flexible, line-rate network monitoring. In USENIX Symposium on Networked Systems Design and Implementation (NSDI), pages 1593-1620, 2024. URL: https://www.usenix.org/conference/nsdi24/presentation/johnson.
  40. Malleswar Kalla, Randall R. Stewart, Tom Taylor, Dr. Vern Paxson, Chip Sharp, Ken Morneault, Dr. HannsJuergen Schwarzbauer, Qiaobing Xie, Ian Rytina, and Lixia Zhang. Stream Control Transmission Protocol. RFC 2960, October 2000. URL: https://doi.org/10.17487/RFC2960.
  41. Wen Kokke. Rusty variation: Deadlock-free sessions with failure in Rust. In Interaction and Concurrency Experience (ICE), volume 304 of Electronic Proceedings in Theoretical Computer Science, pages 48-60. Open Publishing Association, 2019. URL: https://doi.org/10.4204/EPTCS.304.4.
  42. James F. Kurose and Keith W. Ross. Computer Networking: A Top-Down Approach. Pearson, 2021. Google Scholar
  43. Julien Lange and Nobuko Yoshida. Verifying asynchronous interactions via communicating session automata. In International Conference on Computer Aided Verification (CAV), volume 11561 of Lecture Notes in Computer Science, pages 97-117. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25540-4_6.
  44. Bob Lantz, Brandon Heller, and Nick McKeown. A network in a laptop: Rapid prototyping for software-defined networks. In Geoffrey G. Xie, Robert Beverly, Robert Morris, and Bruce Davie, editors, ACM Workshop on Hot Topics in Networks (HotNets), page 19, 2010. URL: https://doi.org/10.1145/1868447.1868466.
  45. Jens Kanstrup Larsen, Roberto Guanciale, Philipp Haller, and Alceste Scalas. P4R-type: A verified API for P4 control plane programs. Proceedings of the ACM on Programming Languages (PACMPL), 7(OOPSLA2):1935-1963, 2023. URL: https://doi.org/10.1145/3622866.
  46. Jens Kanstrup Larsen, Alceste Scalas, Guy Amir, Jules Jacobs, Jana Wagemaker, and Nate Foster. NEST: Network Enforced Session Types (Technical Report), 2026. URL: https://doi.org/10.48550/arXiv.2604.21795.
  47. Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. Complete multiparty session type projection with automata. In International Conference on Computer Aided Verification (CAV), volume 13966, pages 350-373. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-37709-9_17.
  48. Sam Lindley and J. Garrett Morris. Embedding session types in Haskell. In International Symposium on Haskell, pages 133-145, 2016. URL: https://doi.org/10.1145/2976002.2976018.
  49. Lars Lockefeer, David M. Williams, and Wan J. Fokkink. Formal specification and verification of TCP extended with the window scale option. Science of Computer Programming, 118:3-23, 2016. URL: https://doi.org/10.1016/j.scico.2015.08.005.
  50. Robin Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989. Google Scholar
  51. Mininet. Mininet: Rapid Prototyping for Software Defined Networks. Available at https://mininet.org/, 2022.
  52. John G. Myers. POP3 AUTHentication command. RFC 1734, December 1994. URL: https://doi.org/10.17487/RFC1734.
  53. Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. Timed runtime monitoring for multiparty conversations. Formal Aspects of Computing, 29(5):877-910, 2017. URL: https://doi.org/10.1007/s00165-017-0420-8.
  54. Rumyana Neykova, Nobuko Yoshida, and Raymond Hu. SPY: local verification of global protocols. In International Conference on Runtime Verification (RV), volume 8174 of Lecture Notes in Computer Science, pages 358-363. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40787-1_25.
  55. Nicholas Ng and Nobuko Yoshida. Static deadlock detection for concurrent Go by global session graph synthesis. In International Conference on Compiler Construction (CC), pages 174-184, 2016. URL: https://doi.org/10.1145/2892208.2892232.
  56. Dominic A. Orchard and Nobuko Yoshida. Effects as sessions, sessions as effects. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 568-581, 2016. URL: https://doi.org/10.1145/2837614.2837634.
  57. Luca Padovani. A simple library implementation of binary sessions. Journal of Functional Programming, 27:e4, 2017. URL: https://doi.org/10.1017/S0956796816000289.
  58. Ivan Prokić, Simona Prokić, Silvia Ghilezan, Alceste Scalas, and Nobuko Yoshida. On asynchronous multiparty session types for federated learning. In International Conference on Theoretical Aspects of Computing (ICTAC), pages 164-182, 2025. URL: https://doi.org/10.1007/978-3-032-11176-0_11.
  59. Riccardo Pucella and Jesse A. Tov. Haskell session types with (almost) no class. In ACM SIGPLAN Symposium on Haskell, pages 25-36, 2008. URL: https://doi.org/10.1145/1411286.1411290.
  60. Sundararajan Renganathan, Benny Rubin, Hyojoon Kim, Pier Luigi Ventre, Carmelo Cascone, Daniele Moro, Charles Chan, Nick McKeown, and Nate Foster. Hydra: Effective runtime network verification. In ACM SIGCOMM Conference (SIGCOMM), pages 182-194, 2023. URL: https://doi.org/10.1145/3603269.3604856.
  61. Marshall T. Rose and John G. Myers. Post Office Protocol - Version 3. RFC 1939, May 1996. URL: https://doi.org/10.17487/RFC1939.
  62. Alceste Scalas and Nobuko Yoshida. Lightweight session programming in Scala. In European Conference on Object-Oriented Programming (ECOOP), volume 56 of LIPIcs, pages 21:1-21:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2016.21.
  63. Alceste Scalas and Nobuko Yoshida. Less is more: multiparty session types revisited. Proceedings of the ACM on Programming Languages (PACMPL), 3(POPL):30:1-30:29, 2019. URL: https://doi.org/10.1145/3290343.
  64. Eve Schooler, Jonathan Rosenberg, Henning Schulzrinne, Alan Johnston, Gonzalo Camarillo, Jon Peterson, Robert Sparks, and Mark J. Handley. SIP: Session Initiation Protocol. RFC 3261, July 2002. URL: https://doi.org/10.17487/RFC3261.
  65. Justine Sherry, Shaddi Hasan, Colin Scott, Arvind Krishnamurthy, Sylvia Ratnasamy, and Vyas Sekar. Making middleboxes someone else’s problem: Network processing as a cloud service. In Lars Eggert, Jörg Ott, Venkata N. Padmanabhan, and George Varghese, editors, ACM SIGCOMM Conference (SIGCOMM), pages 13-24, 2012. URL: https://doi.org/10.1145/2342356.2342359.
  66. Felix Stutz and Damien Zufferey. Comparing channel restrictions of communicating state machines, high-level message sequence charts, and multiparty session types. In Pierre Ganty and Dario Della Monica, editors, International Symposium on Games, Automata, Logics and Formal Verification (GandALF), volume 370 of Electronic Proceedings in Theoretical Computer Science, pages 194-212. Open Publishing Association, 2022. URL: https://doi.org/10.4204/EPTCS.370.13.
  67. Steve Vinoski. Advanced message queuing protocol. IEEE Internet Computing, 10(6):87-89, 2006. URL: https://doi.org/10.1109/MIC.2006.116.
  68. Philip Wadler. Propositions as sessions. In International Conference on Functional Programming (ICFP), pages 273-286, 2012. URL: https://doi.org/10.1145/2364527.2364568.
  69. Nobuko Yoshida. Programming language implementations with multiparty session types. In Active Object Languages: Current Research Trends, volume 14360 of Lecture Notes in Computer Science, pages 147-165. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-51060-1_6.
  70. Nobuko Yoshida and Ping Hou. Less is more revisited: Association with global multiparty session types. In The Practice of Formal Methods: Essays in Honour of Cliff Jones, Part II, volume 14781 of Lecture Notes in Computer Science, pages 268-291. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-66673-5_14.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact