There is no room for complacency in software development! In the OCaml ecosystem, improvements are continuously introduced to optimise existing workflows, introduce new features, and boost performance.

MirageOS is a toolchain for creating unikernels (very small images that embed both an application and the OS components needed to run it) from several libraries written in OCaml. It allows users to create robust, fast, and secure applications.

We invest in the development of MirageOS, supporting great work both internally and at other organisations. One of these projects is Hannes Mehnert’s work at Robur, developing an updated Transmission Control Protocol (TCP) for MirageOS.

Networking in MirageOS

Historically, much work has gone into implementing a complete network stack native to MirageOS. Getting networking right without relying on the Linux stack and in a safe language like OCaml is tremendously important for a tool that aims to build unikernels deployed in a cloud environment. Good network management is paramount for applications with large user bases. Over time, developers have written multiple libraries for MirageOS to handle every layer of the networking stack, from Ethernet to HTTP.

TCP

The TCP protocol, described in Hannes's recent blog post, is a protocol that is a fundamental building block for most of the higher-level protocols and applications. Its role is to handle reliable data delivery from one point to the other so that the rest of the stack can focus on the actual content of that data. The protocol is specified in English in a series of RFCs, and a variety of implementations exist for this specification, with potentially different behaviours depending on their interpretation of (or even compliance with) the specification. This means that TCP traffic in the wild is not uniform, and coping with it means accepting a broad interpretation of the specification and recovering gracefully from non-complying traffic.

The historical library that implements TCP in MirageOS is the widely used mirage-tcpip. Mirage-tcpip is used by thousands of developers every single day in Docker Desktop, where it handles traffic between container and host. While it usually works well under controlled circumstances (well-formed traffic, local networks), this library has some issues that are not easily solved, which Hannes describes in his post (memory leakage, low tolerance to non-ideal traffic, etc).

µTCP and Formal Methods

As part of our mission to build robust and secure systems, we strive to support technology that roots its design in the field of formal methods, a variety of techniques, tools and approaches which provide a rigorous framework for the specification and implementation of software. HOL4 is one such tool, allowing users to formally specify and prove theorems. It can be used as a foundation to define complex specifications that can then serve as a reference to test or prove compliance with implementations.

Peter Sewell et al. used HOL4 to build a semantic model of the TCP specification (by describing the byte-stream service provided to users) that could cope with diverse complying implementations of TCP, as checked by testing it against real traffic. That same model is what Hannes is using to derive an OCaml implementation usable by MirageOS, called µTCP. While there is no formal link between the model and the implementation (the work is primarily manual, and the transposition is not always 1:1), it is a perfect opportunity for a new TCP implementation that copes with more realistic traffic by design, and may avoid some of the other problems of mirage-tcpip such as memory leaks and performance limitations. Eventually, it may become a suitable replacement for mirage-tpcip within MirageOS, where the change should be seamless thanks to the abstract TCP interface of MirageOS.

Next Steps

Keep an eye out for updates from Hannes and Robur, as they will be testing µTCP more to get it ready for public release. The team appreciates feedback, so please check out µTCP on your own and report on your experience in the repo. We are thrilled to see improved features for MirageOS, and hopefully it will bring even more users to the ecosystem.

You can also follow us on X (formerly known as Twitter) and LinkedIN to keep up with our projects. We would love to discuss how MirageOS can benefit you in your projects!