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.

翻译：会话类型是一种类型化规范，用于形式化描述通信驱动的应用，旨在减少软件生命周期后期的错误并简化调试过程。传输层协议（如TCP、UDP和QUIC）支撑着现代互联网上的绝大部分通信，影响着数十亿终端用户。与应用层相比，传输层具有不同的需求和约束条件，从而导致验证要求也有所不同。尽管如此，据我们所知，目前尚无研究展示会话类型在传输层的应用。在本文中，我们探讨了如何将多方会话类型（MPST）应用于TCP协议实现。我们基于MPST在Rust中实现了一个TCP服务器子集，并测试了其与Linux TCP协议栈的互操作性。研究结果揭示了会话类型理论假设与传输层协议常规实现方式之间的差异。本工作是将会话类型引入传输层的初步探索。