AdaCore Blog

Enhancing the Security of a TCP Stack with SPARK

by Yannick Moy

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.

Posted in #SPARK    #Security    #Formal Verification   

About Yannick Moy

Yannick Moy

Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.