DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2026.17

NEST: Network Enforced Session Types

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

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{larsen_et_al:LIPIcs.ECOOP.2026.17,
  author =	{Larsen, Jens Kanstrup and Scalas, Alceste and Amir, Guy and Jacobs, Jules and Wagemaker, Jana and Foster, Nate},
  title =	{{NEST: Network Enforced Session Types}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{17:1--17:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.17},
  URN =		{urn:nbn:de:0030-drops-261137},
  doi =		{10.4230/LIPIcs.ECOOP.2026.17},
  annote =	{Keywords: Session types, runtime verification, P4, programmable data planes}
}

Document

Artifact

DOI: 10.4230/DARTS.12.1.2

NEST: Network Enforced Session Types (Artifact)

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

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract

This artifact contains NEST: a tool for synthesizing network-level runtime monitors from application-level protocols specified as session types. More specifically, NEST takes as input one or more session types, and generates (1) a set of table entries to be uploaded on network switches that support the P4 standard, and (2) a Python API allowing applications to send/receive messages that carry the packet headers required for the network-level monitoring to work. This artifact also contains the code for reproducing the examples and measurements in the companion paper.

Cite as

Jens Kanstrup Larsen, Alceste Scalas, Guy Amir, Jules Jacobs, Jana Wagemaker, and Nate Foster. NEST: Network Enforced Session Types (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{larsen_et_al:DARTS.12.1.2,
  author =	{Larsen, Jens Kanstrup and Scalas, Alceste and Amir, Guy and Jacobs, Jules and Wagemaker, Jana and Foster, Nate},
  title =	{{NEST: Network Enforced Session Types (Artifact)}},
  pages =	{2:1--2:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Larsen, Jens Kanstrup and Scalas, Alceste and Amir, Guy and Jacobs, Jules and Wagemaker, Jana and Foster, Nate},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.2},
  URN =		{urn:nbn:de:0030-drops-261392},
  doi =		{10.4230/DARTS.12.1.2},
  annote =	{Keywords: Session types, runtime verification, P4, programmable data planes.}
}

Search Results

Documents authored by Amir, Guy

NEST: Network Enforced Session Types

Abstract

Cite as

NEST: Network Enforced Session Types (Artifact)

Abstract

Cite as

Thanks for your feedback!

Could not send message