You've probably never heard of CycloneTCP, an open source dual IPv4/IPv6 stack dedicated to embedded applications. That may be because people don't find and publish vulnerabilities for this stack. The quality of CycloneTCP is even acknowledged by the AMNESIA:33 report, which classifies it as one of the most resilient TCP/IP stacks.

To go beyond the usual best development practices and use of industrial testsuites, the developers of CycloneTCP at Oryx Embedded partnered with AdaCore. We worked together to replace the TCP part of the C codebase with SPARK code, and used the SPARK tools to prove both that the code is not vulnerable to the usual runtime errors (like buffer overflow) and that it correctly implements the TCP automaton specified in RFC 793. As part of this work, we found two subtle bugs related to memory management and concurrency.

For more details, see our article or watch our online presentation on October 20th at IEEE SecDev 2021.