If Layering is useful, why not Sublayering?

The Internet's success arose from classical layering: protocols like TCP and Ethernet can be independently understood, changed, debugged, verified, and offloaded to hardware using a clean service interface between layers. To accrue the same benefits at a finer grain, we suggest sublayering, i.e., layering recursively within each layer. We show that the data link and routing layers have natural sublayers. However, while TCP intuitively decomposes into sub-functions (connection management, reliable delivery, congestion control) common state variables like sequence numbers and window sizes entangle these functions, making sublayering difficult. We propose an alternate sublayered TCP with equivalent functionality which enables easily changing congestion control and connection management. We also argue that sublayering can help create robust and verified Internet protocol implementations akin to seL4 for Operating Systems. To this end, we describe early experiments with a verified sublayered implementation of a simple bit-stuffing protocol using Coq, and a verified monolithic implementation of a lightweight TCP using Dafny. We end with a set of challenges for sublayered protocols.