arxiv: 2604.21795 · v1 · submitted 2026-04-23 · 💻 cs.PL

Recognition: unknown

NEST: Network Enforced Session Types (Technical Report)

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

Authors on Pith no claims yet

Pith reviewed 2026-05-08 12:47 UTC · model grok-4.3

classification 💻 cs.PL

keywords session typesruntime verificationnetwork monitoringdata planeP4protocol enforcementmicroservicespacket loss

0 comments

The pith

Session types can generate packet-level monitors that enforce protocols directly in the network data plane.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces NEST as a way to move protocol checking from application code into the network itself. It provides algorithms that convert session types into monitors running in programmable switches, with extensions that keep the checks accurate even when packets are lost or arrive out of order. A sympathetic reader would care because this separation means applications no longer need to be rewritten or wrapped to guarantee correct communication patterns. The evaluation on microservice and network-function examples shows the monitors can handle realistic protocols while staying inside the data plane.

Core claim

NEST develops algorithms to synthesize packet-level monitors from session types, extends those monitors to tolerate packet loss and reordering, implements the result in P4, and demonstrates on microservice and network-function models that the resulting network monitors can enforce non-trivial protocols without instrumenting or wrapping the application code.

What carries the argument

The synthesis algorithms that translate session types into P4 programs for data-plane monitors, extended with logic to track protocol state across lost and reordered packets.

If this is right

Application code can remain unchanged while the network still guarantees protocol compliance.
Protocol enforcement becomes possible for microservices and network functions without adding software instrumentation layers.
Monitors continue to work correctly when packets are lost or reordered, matching conditions in real networks.
The same synthesis approach scales to other session-typed protocols beyond the evaluated cases.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Placing enforcement in the data plane could let operators add protocol checks to existing deployments without redeploying applications.
The approach might combine with existing network telemetry to give operators both enforcement and diagnostic traces from the same hardware.
If the synthesis is compositional, it could support incremental addition of new protocol constraints without regenerating the entire monitor.

Load-bearing premise

The translation from session types to packet monitors produces correct detectors that catch every violation without false positives or prohibitive overhead under realistic loss and reordering.

What would settle it

An observed protocol violation that the generated monitor fails to report, or a report of violation on traffic that actually follows the session type, or measured P4 resource usage that exceeds switch limits on the evaluated applications.

Figures

Figures reproduced from arXiv: 2604.21795 by Alceste Scalas, Guy Amir, Jana Wagemaker, Jens Kanstrup Larsen, Jules Jacobs, Nate Foster.

**Figure 2.** Figure 2: Global session type for BookInfo. Meanwhile, Review first queries the internal Ratings service and then replies with reviews and ratings. The behavior of BookInfo is captured by the global session type in view at source ↗

read the original 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 synthesize 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

NEST synthesizes session types into P4 data-plane monitors that handle loss and reordering, which is a genuine shift from code-level approaches, but the translation lacks visible formal semantics or validation.

read the letter

The main point on this paper is that it takes session types and turns them into monitors that run straight in the network fabric with P4, instead of instrumenting or wrapping the applications. They also extend the monitors to cope with packet loss and reordering, then show an implementation and some tests on microservice and network-function models. That combination is what stands out as new: a direct path from protocol descriptions to data-plane enforcement without code changes on the endpoints. The algorithms for monitor generation and the handling of impairments are presented as concrete steps, and the evaluation indicates they can cover non-trivial protocols with reasonable overhead. That practical angle is worth credit, especially since it builds on existing session-type foundations rather than starting from scratch. The P4 implementation and the reported tests on realistic setups give some evidence that the idea is workable in current network hardware. The soft spot is the soundness of the synthesis under realistic network conditions. The claim that the generated monitors correctly enforce the original types even when packets are lost or reordered rests on the algorithms, but the description stays at a high level without spelling out the exact semantics that map session types to the network automaton or how reordering buffers and loss detection are encoded. No proofs, machine-checked results, or systematic checks on small session types are referenced, so it remains possible that the monitors either let invalid traces through or reject valid ones under interleavings. This is the central technical risk. The paper is aimed at people working on runtime verification, network programming languages, or distributed systems who want protocol enforcement at the wire level. A reader already familiar with session types or P4 would pick up the synthesis technique and the implementation details quickly. It deserves a serious referee because the idea is distinct from prior work and the implementation shows feasibility, even if the formal grounding needs to be tightened in revision. I would send it out for review with a clear request for the missing semantics and validation.

Referee Report

2 major / 1 minor

Summary. The paper introduces NEST, a runtime verification framework that synthesizes packet-level monitors from session types to enforce protocols directly in the network data plane using P4. It develops algorithms to generate these monitors, extends them to handle packet loss and reordering, implements the system in P4, and evaluates it on microservice and network-function models to demonstrate enforcement of realistic non-trivial protocols.

Significance. If the synthesis algorithms are sound, this could meaningfully advance the application of session types to programmable networks by moving enforcement into the fabric without application changes. The P4 implementation and evaluation on practical models are strengths that support the practicality claim. However, the central contribution hinges on correct handling of network impairments, and the absence of detailed formal semantics or validation for the loss/reordering extensions limits the assessed impact.

major comments (2)

[Abstract and monitor synthesis section] The abstract and monitor synthesis description claim algorithms that correctly translate session types into P4 monitors detecting violations under loss and reordering, but no explicit semantics relating the original session type to the network-level automaton (including reordering buffers or loss timers) is provided; this is load-bearing for the correctness claim and leaves open the possibility of accepting invalid traces or rejecting valid ones under realistic interleavings.
[Evaluation section] The evaluation on microservice and network-function models reports enforcement but does not include quantitative data on false-positive rates, detection latency, or behavior under controlled loss/reordering scenarios; without this, the claim that monitors enforce protocols 'even under packet loss and reordering' cannot be fully assessed.

minor comments (1)

Notation for session types and their network encoding could be clarified with a small example showing the mapping from a simple protocol to P4 tables.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive review and for recognizing the potential impact of moving session-type enforcement into the data plane. We address each major comment below, indicating the revisions we will make to strengthen the manuscript.

read point-by-point responses

Referee: [Abstract and monitor synthesis section] The abstract and monitor synthesis description claim algorithms that correctly translate session types into P4 monitors detecting violations under loss and reordering, but no explicit semantics relating the original session type to the network-level automaton (including reordering buffers or loss timers) is provided; this is load-bearing for the correctness claim and leaves open the possibility of accepting invalid traces or rejecting valid ones under realistic interleavings.

Authors: We agree that the absence of an explicit formal semantics relating session types to the network-level automaton (including reordering buffers and loss timers) weakens the correctness argument. The manuscript describes the synthesis algorithms and their extensions but relies on informal justification for the correspondence under loss and reordering. In the revised version we will add a new subsection that defines the network-level semantics, models the buffers and timers explicitly, and states the soundness property with respect to the original session-type traces. revision: yes
Referee: [Evaluation section] The evaluation on microservice and network-function models reports enforcement but does not include quantitative data on false-positive rates, detection latency, or behavior under controlled loss/reordering scenarios; without this, the claim that monitors enforce protocols 'even under packet loss and reordering' cannot be fully assessed.

Authors: The present evaluation shows that the P4 monitors successfully enforce realistic protocols on microservice and network-function models. We acknowledge that quantitative metrics would allow a more rigorous assessment of the loss/reordering extensions. We will extend the evaluation section with additional experiments that report detection latency, false-positive rates, and behavior under controlled packet-loss and reordering traces. revision: yes

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper introduces NEST as a new runtime verification framework that synthesizes packet-level monitors from session types, with extensions for loss and reordering implemented in P4. No equations, fitted parameters, or self-referential definitions appear in the provided abstract or description that reduce any central claim to its own inputs by construction. The algorithms are presented as a novel construction building on prior session-type literature, without load-bearing self-citations or ansatzes that collapse the result. This is the expected outcome for a systems paper describing a new implementation and evaluation.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Abstract-only view shows reliance on standard session type semantics and network packet models; no explicit free parameters, new physical entities, or ad-hoc axioms are stated.

axioms (1)

domain assumption Session types have a direct correspondence to sequences of network packets that can be monitored at the data plane
Core premise for generating monitors from types, invoked implicitly when claiming synthesis is possible.

pith-pipeline@v0.9.0 · 5387 in / 1196 out tokens · 64042 ms · 2026-05-08T12:47:00.548001+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

10 extracted references · 3 canonical work pages

[1]

32 Keigo Imai, Nobuko Yoshida, and Shoji Yuen

Association for Computing Machinery.doi:10.1145/3289602.3293924. 32 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. 33Keigo Imai, Shoji Yuen, and Kiyoshi Agusa. Session Type Inference in Haskell. InProc. 3rd Workshop on Programming Language Ap...

work page doi:10.1145/3289602.3293924 2019
[2]

QUIC: A UDP-Based Multiplexed and Secure Transport

URL:https://www.rfc-editor.org/info/rfc9000,doi:10.17487/RFC9000. 37 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom. pages 466–495, 2022. 38 Thomas Jespersen, Philip Munksgaard, and Ken Larsen. Session Types for Rust. InProc. 11th ACM SIGPLAN Workshop on Generic Prog...

work page doi:10.17487/rfc9000 2022
[3]

Yoshida. On Asynchronous Multiparty Session Types for Federated Learning. In Zhiming

Accessed: 2025-03-15. 53John G. Myers. POP3 AUTHentication command, 1994.doi:10.17487/RFC1734. 54 Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. Timed Runtime Mmonitoring for Multiparty Conversations.Formal Aspects of Computing, 29(5):877–910, 2017. doi: 10.1007/S00165-017-0420-8. 55 Rumyana Neykova, Nobuko Yoshida, and Raymond Hu. SPY: Local Verifica...

work page doi:10.17487/rfc1734 2025
[4]

4.3, ¨T =T⟨|σsuch that, for someT′′and σ′, T p&m(S) −−−−→T′′andσ≡q▷m(S)·σ′

By inversion of ruleSQ-Dequeuein Def. 4.3, ¨T =T⟨|σsuch that, for someT′′and σ′, T p&m(S) −−−−→T′′andσ≡q▷m(S)·σ′. 2.Therefore, by ruleSQ-Dequeuein Def. 4.3 we have ¨T′=T ′′⟨|σ′
[5]

4.3,unf(T) must be an external choice fromq including a message with label m and payload typeS

By Item 1 and Def. 4.3,unf(T) must be an external choice fromq including a message with label m and payload typeS. Thus, by Def. 4.10, we haveJTK q?m(S)✓ −−−−−→JT′′K (using ruleSTMon-Recto unfoldTif needed, and thenSTMon-ExtC)
[6]

4.10, and Lemma A.6, q ¨T y = JT⟨|σK= JT′′⟨|σ′K = q ¨T′y

By Item 1, Item 2, Item 3, Def. 4.10, and Lemma A.6, q ¨T y = JT⟨|σK= JT′′⟨|σ′K = q ¨T′y
[7]

4.8 and Item 4, we have ⌈ ¨T ⌉q ¨T y τ(q&m(S)) −−−−−−→ ⌈ ¨T′⌉q ¨T y =⌈ ¨T′⌉q ¨T′y

Hence, by ruleM-Dequeuein Def. 4.8 and Item 4, we have ⌈ ¨T ⌉q ¨T y τ(q&m(S)) −−−−−−→ ⌈ ¨T′⌉q ¨T y =⌈ ¨T′⌉q ¨T′y
[8]

moreover

Thus, by Item 5 and ruleMNet-Dequeuein Def. 4.9 we havep: ⌈ ¨T1 ⌉q ¨T y τ(pi:q&m(S)) −−−−−−−−→ p: ⌈ ¨T′⌉q ¨T′y . Therefore, by Item 6 and Def. 4.14 we obtain the thesis.◀ ▶ Lemma A.9.If mon ( p: ¨T ) τ(p:q&m(S)) −−−−−−−→ˆN′, then∃¨T′such that p: ¨T τ(p:q&m(S)) −−−−−−−→p:¨T′ and ˆN′= mon ( p: ¨T′) . Proof. By inversion of ruleMNet-Dequeuein Def. 4.9, ruleM...
[9]

All the external choices fromp that are reached first inT′cannot syntactically consume the message p▷m(S)from the input queueσ. Observe that, by(2) and Lemma A.14,T consumes its input messagesσby reducing into a session typeT′′reachable fromT′— and therefore, suchT′′also does not syntactically contain any external choice fromp that can consume the message...
[10]

Start", 3IntChoice(Map((a_BookInfo, l_Request) -> 4ExtChoice(a_BookInfo, Map(l_Response -> 5Var(

There are external choices inT′that could consume the messagep▷m(S), but they are prefixed by an internal choice towardsp. Observe that, by (2) and Lemma A.14,T consumes its input messagesσby reducing into a session typeT′′reachable fromT′ by firing the same inputs/outputs ofT′(plus the inputs fromσ) in the same order. Therefore, either before or after re...

2000