Towards a Verified Implementation of a Network Stack
We are implementing a pure IPv6 networking stack optimized to run on IoT endpoints connected to a network through an Ethernet interface. Our implementation supports only the minimal set of protocols required to enable efficient UDP-based communication. In particular, it does not include support for specialized operations such as multicasting, routing, load balancing, firewalling, network address translation, and tunneling. We are on track to release our implementation within the December time frame.
Our minimal implementation delivers several important advantages: It minimizes code footprint, shortening execution paths and improving instruction cache locality, thereby improving the memory hierarchy performance. It reduces the attack surface, improving reliability and security. It eases any verification efforts. It allows the implementation to be compiled directly with the target application further improving performance by eliminating some context switches.
We are preparing to formally verify the correctness and characterize the performance of our networking stack. We believe our implementation will provide high performance through a strict application of separation of concerns[Dijkstra1974Separation] and elimination of all unnecessary data copies, while keeping the codebase amenable to verification.