NEST: Network Enforced Session Types

NEST-generated monitors decide whether to accept or reject a packet by processing a dedicated session header (Fig. 7). Each monitored-session packet must carry this header; others are rejected by default. The P4 monitoring logic is implemented by the table monitor_table (Fig. 8), which extracts from the session header the sender role, message label ID, receiver role – and obtains the current state from the stateful register on the switch – to decide whether to accept or reject the packet..³³3The session header currently used by NEST (depicted in Fig. 7) supports protocols with up to 15 distinct roles and up to 63 distinct message labels. This bound can be increased if needed, although doing so may be constrained by packet size and the memory available on the P4 switch. The monitor_table matches extracted session-header fields against entries generated by NEST from a session-type MAT such as Fig. 6. Each packet can match at most one monitor_table entry – and if so, the packet is accepted; otherwise, the default reject action drops the packet (line 13 in Fig. 8).

The accept action of monitor_table also inspects the session ID, allowing one device to distinguish and track many sessions in parallel: if a packet with session ID $s$ is accepted, accept uses $s$ to index a P4 register and update that session’s state. The session header also carries a session sequence number, used to handle retransmissions (discussed in Section 3.3).

Although Fig. 1 shows one switch per end host, NEST also supports multiple end hosts per switch, even with different roles. This raises a practical challenge: how can one device monitor multiple roles concurrently? Suppose a device must monitor roles $𝚙$ and $𝚚$ in session types $T_{𝚙}$ and $T_{𝚚}$. Let $⟦T_{𝚙}⟧$ and $⟦T_{𝚚}⟧$ be the monitors synthesised when these roles are monitored separately. We build one monitor from these two using standard process-calculus techniques:

1. 1.

   Compute the labelled transition system (LTS) of the parallel composition $⟦T_{𝚙}⟧\parallel ⟦T_{𝚚}⟧$ in the style of CCS [50], allowing synchronisation when the monitor $⟦T_{𝚙}⟧$ accepts an outgoing message to $⟦T_{𝚚}⟧$ (or vice versa).

2. 2.

   Prune non-synchronising transitions where the monitor $⟦T_{𝚙}⟧$ accepts a message to/from $⟦T_{𝚚}⟧$ (or vice versa); in CCS terms, apply restriction $(\nu 𝚙,𝚚)(⟦T_{𝚙}⟧\parallel ⟦T_{𝚚}⟧)$.

3. 3.

   Deploy on the P4 device a monitor state machine matching this restricted composition, so the device can monitor $T_{𝚙}$ and $T_{𝚚}$ together.⁴⁴4With a minor extension of the formal model introduced later in Section 4, the behaviour of a network using this joint monitor for $T_{𝚙}$ and $T_{𝚚}$ can be proven bisimilar to a network where the end hosts of $𝚙$ and $𝚚$ are connected to different devices, matching the premises of our monitor correctness result (Theorem 4.18).

So far, NEST-generated monitor state machines and MATs (Figures 9(b) and 6) cover the “core logic” from Section 3.1: for a session type $T$, they distinguish violating packets from out-of-order but valid packets. This is also the focus of the formal synthesis in Section 4. The result is a P4 monitor that works on reliable networks.

However, such monitors would often behave incorrectly in real-world networks, where packets may be lost, duplicated, and reordered (even when they have the same sender). To address these issues, transport protocols such as TCP add transmission logic to packets and may adjust their sending order to guarantee reliable delivery. Therefore, NEST is designed to be flexible with respect to transport protocols between end hosts. In particular, NEST can generate TCP-oriented P4 monitors for session types by augmenting a “core” monitor state machine and MAT (like those in Figures 9(b) and 6, which follow Def. 4.10) with transitions and checks for TCP socket setup/teardown, packet acknowledgements, and retransmissions within a TCP connection. E.g., Fig. 10 depicts the TCP-oriented monitor obtained from the state machine in Fig. 9(b) by adding TCP-specific transitions (dashed arrows) and checks.

• $\mathrm{■}$

  The TCP-oriented monitor always accepts packets related to TCP connection setup and teardown (i.e., TCP headers with the SYN or FIN flag set) without changing its state. It also accepts pure TCP acknowledgements (i.e., TCP headers with ACK) unless the ACK is piggybacked with a session header, in which case normal monitoring applies.

• $\mathrm{■}$

  As mentioned in Section 3.1, the session header carries a session sequence number (SSN) field, which records the total number of messages sent by the sender so far. These sequence numbers are tracked by our TCP-oriented monitors. The TCP-oriented monitor uses a detailed decision procedure based on SSNs; the details of this decision procedure are simplified away for the transitions shown in Fig. 10, but are explained in Fig. 11 (essentially, the end states in Fig. 11 correspond to transitions that each state in Fig. 10 can take). We explain the decision procedure:

  1. 1.

     If an incoming packet’s SSN is less than or equal to the monitor’s stored SSN for that sender, the packet is accepted as a retransmission and does not update monitor state.

  2. 2.

     Otherwise (SSN greater), the packet is first matched on sender and recipient only.⁵⁵5Step 2 ignores the packet label because if the monitor were to match simultaneously on sender, recipient, and label at this step, then a failed match would be ambiguous and would not allow the monitor to distinguish between two cases: truly invalid packets that must cause the session to be dropped (handled in step 4), or possibly out-of-order packets that must be dropped to be later retransmitted (handled in step 3). To match packets only on sender and recipient, the TCP-oriented monitor uses an additional table, receiver_table, a partial version of monitor_table that ignores the packet label.

  3. 3.

     If both sender and recipient match, the monitor then matches the packet label. If that matches, there are two cases. Suppose that the monitor is guarding the network border for end host $𝚙$:

     • –

       For each outgoing packet sent by $𝚙$, if the packet SSN matches the next expected value (i.e., the stored SSN plus one), the monitor accepts the packet and updates its state. On the other hand, if the SSN is too high, the monitor drops the packet: this is because the SSN being too high means that some packets were lost, hence the monitor awaits their retransmission with the correct SSN.

     • –

       For each incoming packet towards $𝚙$, the monitor trusts the SSN as-is and updates its state without further checks: the monitor assumes that the SSN was already checked and accepted by the border monitor on the sender side.

  4. 4.

     If both sender and recipient match but the label does not, the packet is rejected. Moreover, if the monitor is guarding end host $𝚙$ and the packet is sent by $𝚙$ with an SSN that is exactly one higher than the stored SSN, the monitor rejects the packet and permanently closes the session – because this indicates a session violation (not mere packet retransmission or reordering).⁶⁶6Closing the session ensures the bad message is not later accepted as a retransmission after SSN advances.

With this approach, our TCP-enabled monitors can handle packet loss (since TCP eventually retransmits lost and unacknowledged packets), duplication (treated as a special case of retransmission), and reordering of packets from the same sender (by simply ignoring out-of-order packets and waiting for their retransmission).

Because our monitors require packets to carry the session header described in Sections 3.1 and 3.3, NEST generates an API for writing monitor-compliant applications. The API hides session-header details and exposes human-readable message-label constants derived from the input session type, rather than numeric label IDs. Our current prototype targets Python and supports the send/receive style in Fig. 4. By design, the API generated by NEST is minimalistic and does not enforce the ordering of send/receive operations specified in the input session type. We take advantage of this in our evaluation (Section 5.2) to write programs that do not follow a session type and show that NEST monitors correctly reject their messages.

The generated API is based on a SessionManager class that instantiates Session objects, each representing one session. Each Session is created with a protocol and a session ID. The API also maintains a queue of incoming messages, from which Session objects dequeue via recvMsg(). This prevents the host program from incorrectly dropping messages (e.g., when a message is delivered earlier than expected).

In Definitions 4.1 and 4.3 we model a network end host as a (local) session type with a multi-input queue that stores incoming messages from multiple senders, while preserving the order of messages from each sender [18]. The idea is that the session type models the behaviour of a message-passing program, while the queue models the end host’s ability to buffer incoming messages (e.g. in its network stack). This modelling is standard in the session-types literature, except that multi-output queues are often used instead of input queues.

The type ${\sum }_{i\in I}{𝚙}_i\oplus {𝚖}_i(S_i).T_i$ is an internal choice where the end host selects one recipient role ${𝚙}_i$ and sends a message with label ${𝚖}_i$ carrying payload type $S_i$; then, the interaction continues as specified in $T_i$. Dually, is an external choice where the end host awaits a message ${𝚖}_i$ with payload type $S_i$ from sender $𝚙$; then, the interaction continues as $T_i$. The lists of possible roles $𝚙,𝚚,𝚛$ and payload types $S$ are examples that can be extended as needed. The type $\mathrm{𝐞𝐧𝐝}$ represents a terminated session, while $\mu 𝐭.T$ and $𝐭$ represent recursion. We define $T⟨|\sigma$ as the pairing of a session type with a multi-input queue $\sigma$, where each element $𝚙⊳𝚖(S)$ represents a message $𝚖$ sent by role $𝚙$ with payload type $S$.

In Def. 4.3, a session type $T$ transitions by emitting labels representing an internal choice $𝚙\oplus 𝚖(S)$ or an external choice , by rules S-IntC, S-ExtC, and S-Rec. For instance, for the session type $T_{\text{Info}}$ in Example 4.2, these rules yield the transition system in Fig. 9(a).

When $T$ is composed with a multi-input queue, rule SQ-Send says that internal choices of $T$ enable a “send” action $𝚙!𝚖(S)$. Rule SQ-Deq uses a standard queue congruence $\equiv$ allowing for swapping two queued messages with different senders: this enables the selective dequeuing and consumption of the oldest queued message from each sender. Then, rule SQ-Deq says that the session type can consume the oldest message from $𝚙$ (from the queue head, via congruence $\equiv$) with an internal action (a.k.a. “$\tau$-action”) ; this can happen only if $T$ is an external choice that awaits a message $𝚖$ from $𝚙$ with payload type $S$, and the oldest queued message from $𝚙$ satisfies these conditions. Finally, rule SQ-Recv allows an arbitrary message $𝚙⊳𝚖(S)$ to be received from the “outside world” and appended to the queue, via a “receive” action $𝚙\mathrm{?}𝚖(S)$.

We model networks in Def. 4.6 as parallel compositions of roles with an end host behaviour represented as a session type with a multi-input queue.

In Def. 4.6 above, rules Net-$\gamma$ and Net-Deq decorate a transition of a session type with input queue $\ddot{T}$ by including the role $𝚙$ that emitted the transition; specifically, Net-$\gamma$ is used when $\ddot{T}$ emits or enqueues a message (via rules SQ-Send or SQ-Recv in Def. 4.3), while Net-Deq is used when $\ddot{T}$ internally consumes a queued message (via SQ-Deq in Def. 4.3). Rule Net-Comm says that if in the sub-network $N_1$ there is $𝚙$ sending a message to $𝚚$, and in the sub-network $N_2$ there is $𝚚$ that can receive that message, then the network advances with a communication $\tau (𝚙\to 𝚚:𝚖(S))$. The rightmost premise of Net-Comm implies that the message from $𝚙$ is added to $𝚚$’s input queue, by Net-$\gamma$ and SQ-Recv in Def. 4.3. Also, by the same rules, any $N_2$ that includes $𝚚$ can always receive any message from any $𝚙$, i.e., rule Net-Comm allows invalid messages to be sent/received between end hosts; see Example 4.7.

To model the pairing of an end host with a monitor that intercepts all its communications, in Def. 4.8 below we combine a session type with queue $\ddot{T}$ and a generic monitor $M$. For now we only assume that $M$ has an LTS semantics with labels of the form $𝚙!𝚖(S)\mathrm{✓}$ / $𝚙\mathrm{?}𝚖(S)\mathrm{✓}$ to signal that $M$ accepts the corresponding send/receive action by $\ddot{T}$, and $𝚙!𝚖(S)\text{✘}$ / $𝚙\mathrm{?}𝚖(S)\text{✘}$ to signal that $M$ rejects them. (We present a concrete instantiation of $M$ in Def. 4.10 below.)

By rule M-Good in Def. 4.8, the pair $\lceil \ddot{T}\rceil M$ performs a transition $\gamma \mathrm{✓}$ if $M$ explicitly accepts the send/receive action $\gamma$ emitted by $\ddot{T}$. Rule M-BadOut says that $M$ can reject and drop a message sent by $\ddot{T}$. Rule M-BadIn says that $M$ can reject and drop an incoming message before it lands in $\ddot{T}$’s input queue. By rule M-Dequeue, $M$ cannot interfere with the internal action that $\ddot{T}$ performs when consuming a message from its input queue. In Def. 4.9 below we monitor networks (Def. 4.6), by adding a monitor to each end host.

In Def. 4.9, each end host is modelled as a role $𝚙$ with a session type (with an input queue) representing the end host behaviour, equipped with a monitor. Rules MNet-$\gamma$-Good and MNet-$\gamma$-Bad annotate accepted and rejected actions (with labels $\gamma \mathrm{✓}$ and $\gamma \text{✘}$ from Def. 4.8) with the end host role $𝚙$ where such actions occurred. The rule MNet-Comm is different from Net-Comm in Def. 4.6, because it only allows communications between two end hosts if their respective monitors accept their outgoing and incoming message; this is because the transitions in the premises of rule MNet-Comm (denoting the acceptance of a message send and enqueuing) can only be fired via rule MNet-$\gamma$-Good.

We now provide a concrete instantiation of monitor $M$ from Def. 4.8: in Def. 4.10 we formalise how to synthesise a network-layer monitor state $⟦T⟧$ from a session type $T$. In Section 3.1 (Fig. 9) we anticipated that the monitor state machine $⟦T⟧$ differs from that of $T$. This is because $⟦T⟧$ has to meet several non-trivial requirements:

1. R1.

   $⟦T⟧$ must accept all messages that an end host implementing $T$ may send/receive to/from the network, depending on $T$’s state;

2. R2.

   $⟦T⟧$ should reject invalid messages that an end host implementing $T$ should not send/receive, again depending on $T$’s state;

3. R3.

   $⟦T⟧$ may receive messages from different senders in an order that does not match $T$’s expectations (due to the network semantics),⁹⁹9In Section 3.3 we also addressed the issue of out-of-order delivery of messages from the same sender, which is orthogonal and handled by protocols like TCP. and yet, $⟦T⟧$ must accept the valid (“good”) messages while still rejecting the invalid (“bad”) ones;

4. R4.

   $⟦T⟧$ must decide whether to accept or reject a message immediately, without buffering, to accommodate the limited memory and processing power of most network devices.

By rule STMon-IntC in Def. 4.10, if $T$ is an internal choice, then $⟦T⟧$ accepts the corresponding send actions and updates its state. Dually, by rule STMon-ExtC, if $T$ is an external choice, then $⟦T⟧$ accepts the corresponding receive actions and updates its state. This reflects requirements R 1 and R 4.

Rules STMon-IntPfx and STMon-ExtPfx allow $⟦T⟧$ to accept an incoming message $𝚖$ with payload type $S$ from role $𝚚$, even if the shape of $T$ does not expect a message from $𝚚$ right now. This is necessary to satisfy requirements R 3 and R 4. By the premises of these rules, acceptance is allowed only if role $𝚚$ is not an immediate recipient/sender in the internal/external choice $T$, and at least one monitor $⟦T_k⟧$ (where $T_k$ is a continuation of $T$) can indeed accept that message by firing a transition $⟦T_k⟧\stackrel{𝚚\mathrm{?}𝚖\left(S\right)\mathrm{✓}}{\to }⟦T_k^{\prime }⟧$. If these conditions hold, then after accepting $𝚚\mathrm{?}𝚖(S)$, rules STMon-IntPfx and STMon-ExtPfx “prune” $T$ by removing all the branches that, if taken, could not possibly accept $𝚚\mathrm{?}𝚖(S)$ in their future transitions. More precisely, $⟦T⟧$ performs the same accepting transition $𝚚\mathrm{?}𝚖(S)\mathrm{✓}$ and becomes $⟦T^{\prime }⟧$, where $T^{\prime }$ has the same shape as $T$, except that:

1. 1.

   $T^{\prime }$ keeps all (and only) the branches of $T$ (indexed by the maximal set $K\subseteq I$) that could accept $𝚚\mathrm{?}𝚖(S)$ in their future transitions; and

2. 2.

   The continuation of each kept branch is reduced to $T_k^{\prime }$ (for $k\in K$).

Note that these rules can fire only if $K\ne \mathrm{\varnothing }$: there must therefore be at least one branch of $T$ that can accept $𝚚\mathrm{?}𝚖(S)$ in its future transitions.

Rule STMon-Rec unfolds recursion. Rule STMon-Bad rejects any send/receive action that $⟦T⟧$ does not explicitly accept, per requirements R 2 and R 4. Finally, $⟦T⟨|\sigma ⟧$ represents the monitor state obtained by feeding all messages in $\sigma$ as inputs to $⟦T⟧$, which must accept all of them: i.e., $⟦T⟨|\sigma ⟧$ is undefined if $⟦T⟧$ does not accept some message in $\sigma$.