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 Static Analysis Lead at AdaCore and co-director of the ProofInUse joint laboratory with Inria. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK, a product he presents 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.