Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Session Types for the Transport Layer: Towards an Implementation of TCP

Samuel Cavoj, Ivan Nikitin, Colin Perkins, Ornela Dardha

TL;DR

This paper tackles bringing multiparty session types (MPST) to transport-layer protocols by implementing a core subset of TCP in Rust and verifying interoperability against the Linux TCP stack. The authors design MPST-based Rust libraries to encode both the network and application interfaces, and they demonstrate correct behavior through hands-on testing, including scenarios with misbehaving networks. Key contributions include the session-type Rust libraries, a proof-of-concept TCP subset implementation, and an evaluation showing practical interoperation with real protocol stacks, while highlighting gaps between MPST theory and transport-layer realities such as timeouts. The work shows the feasibility of formally verifying transport-layer protocols with MPST and identifies concrete avenues for future extensions like timeouts, congestion control, and richer modeling of transport behavior. Overall, this represents a first step toward formally verified transport-layer protocols with tangible interoperability implications.

Abstract

Session types are a typing discipline used to formally describe communication-driven applications with the aim of fewer errors and easier debugging later into the life cycle of the software. Protocols at the transport layer such as TCP, UDP, and QUIC underpin most of the communication on the modern Internet and affect billions of end-users. The transport layer has different requirements and constraints compared to the application layer resulting in different requirements for verification. Despite this, to our best knowledge, no work shows the application of session types at the transport layer. In this work, we discuss how multiparty session types (MPST) can be applied to implement the TCP protocol. We develop an MPST-based implementation of a subset of a TCP server in Rust and test its interoperability against the Linux TCP stack. Our results highlight the differences in assumptions between session type theory and the way transport layer protocols are usually implemented. This work is the first step towards bringing session types into the transport layer.

Session Types for the Transport Layer: Towards an Implementation of TCP

TL;DR

This paper tackles bringing multiparty session types (MPST) to transport-layer protocols by implementing a core subset of TCP in Rust and verifying interoperability against the Linux TCP stack. The authors design MPST-based Rust libraries to encode both the network and application interfaces, and they demonstrate correct behavior through hands-on testing, including scenarios with misbehaving networks. Key contributions include the session-type Rust libraries, a proof-of-concept TCP subset implementation, and an evaluation showing practical interoperation with real protocol stacks, while highlighting gaps between MPST theory and transport-layer realities such as timeouts. The work shows the feasibility of formally verifying transport-layer protocols with MPST and identifies concrete avenues for future extensions like timeouts, congestion control, and richer modeling of transport behavior. Overall, this represents a first step toward formally verified transport-layer protocols with tangible interoperability implications.

Abstract

Session types are a typing discipline used to formally describe communication-driven applications with the aim of fewer errors and easier debugging later into the life cycle of the software. Protocols at the transport layer such as TCP, UDP, and QUIC underpin most of the communication on the modern Internet and affect billions of end-users. The transport layer has different requirements and constraints compared to the application layer resulting in different requirements for verification. Despite this, to our best knowledge, no work shows the application of session types at the transport layer. In this work, we discuss how multiparty session types (MPST) can be applied to implement the TCP protocol. We develop an MPST-based implementation of a subset of a TCP server in Rust and test its interoperability against the Linux TCP stack. Our results highlight the differences in assumptions between session type theory and the way transport layer protocols are usually implemented. This work is the first step towards bringing session types into the transport layer.
Paper Structure (16 sections, 1 equation, 2 figures)

This paper contains 16 sections, 1 equation, 2 figures.

Table of Contents

  1. Introduction
  2. Session types
  3. Transmission Control Protocol (TCP)
  4. Implementation
  5. Defining session types
  6. Multi-way Offer branching
  7. Recursive session types
  8. Using session types
  9. Establishing a Connection
  10. Data Transmission and Re-transmission
  11. Closing the connection
  12. Evaluation
  13. Related Work and Conclusion
  14. Appendix
  15. Three-way handshake
  16. ...and 1 more sections

Figures (2)

  • Figure 1: The state transition diagram of TCP in RFC9293 rfc9293. We annotate the diagram with the messages and transitions modelled in our implementation. Note that we do not model timeouts as part of the type system, hence, the TIME-WAIT to CLOSED transition is not implemented using session types. Additionally, we do not implement the active OPEN case of the handshake for simplicity (as this would not demonstrate any new modelling or implementation techniques), this is however possible using our implementation.
  • Figure 2: TCP three-way Handshake with all roles.