Enhance the security of networking libraries with formally proven message handling in SPARK

AdaCore: Helping Developers Build Software that Matters

Everything we do at AdaCore is centered around helping developers build safe, secure and reliable software.

For over 25 years, we've worked with global leaders across the military and civil avionics, defense systems, air traffic management/control, space, railway, and financial services industries, building tools and providing services that ease the complex and difficult process of developing high-integrity software. As the need for truly secure and reliable applications expands into industries such as automotive, medical, energy, and IOT, we’re advancing our time-tested technologies to bring expertise and services to help a whole new generation of developers. Through our subscription-based business model and dedicated services arm, we have worked with hundreds of customers over the year on thousands of projects.

Our 120 experts worldwide in the US (New York, Lexington), France (Paris, Toulouse, Grenoble and Vannes), the UK, and Estonia, all play a role in developing state-of-the-art technologies to meet the challenges of building the highest grade of software.

Joining AdaCore is about joining a culture of innovation, openness, collaboration and dependability, which defines how we work together, with our customers and partners.

Enhance the security of networking libraries with formally proven message handling in SPARK

Context:

SPARK is a subset of the Ada programming language, together with formal verification tools which allow giving mathematical guarantees about SPARK programs, from correct data flows to absence of runtime errors to correct implementation of functional requirements. SPARK is open source and freely available to the Community on www.adacore.com/download as well as professionally supported by AdaCore, which co-develops SPARK with Altran and Inria. RecordFlux (https://github.com/Componolit/RecordFlux) is a Domain Specific Language for specifying binary message formats and generating a provably correct implementation of message handling in SPARK. RecordFlux is also developed by AdaCore in open source.  

Goal:

The subject of this internship is to use RecordFlux and SPARK to replace the hand-written message handling code in parts of the CycloneTCP/CycloneSSL open source libraries in C developed by company Oryx Embedded (www.oryx-embedded.com). A previous internship successfully replaced part of the Socket and TCP implementation in C with a manually-written implementation in SPARK, including detailed specification of the underlying state machine of the TCP protocol. This work led to the discovery of subtle bugs in the C implementation, and gave stronger confidence that the resulting SPARK implementation is correctly implementing critical properties of the protocol. The results of this work have been published at IEEE SecDev 2021 conference (https://www.adacore.com/papers/layered-formal-verification-of-a-tcp-stack). This new internship focuses on message handling, which is a known source of security vulnerabilities (e.g. the recent https://www.jsof-tech.com/ripple20/ precisely on TCP implementations) as manually validating the content of binary messages is error-prone. The objective here is twofold: demonstrate that the message handling part of existing protocol implementations can be replaced by code generated from a DSL which is proven to be correct-by-construction; extend the guarantees provided by formal verification to other parts of the libraries that call in the message handling part.

Skills required: The work will require interacting closely with engineers from AdaCore on the language/proof side on and RecordFlux technology, and Oryx Embedded on the library/protocol side.

Timeframe and location:

The internship will take place in the offices of AdaCore in Paris. Trips to Grenoble may be required to work with engineers from Oryx Embedded, in addition to frequent remote interactions.