Implementing communication protocols correctly remains a huge challenge. Complex message formats and interdependencies paired with imprecise, incomplete or even contradictory English-language specifications make it hard to even define what “correct” means for a given protocol. The use of unsafe programming languages is of no help either and regularly leads to security vulnerabilities affecting millions of devices. At the same time, communication protocols are essential for today's connected world and often exposed to untrusted environments.

AdaCore’s latest version of the SPARK language [https://www.adacore.com/sparkp...] and toolset was used successfully to formally verify critical software in customer projects over the last eight years. The need for trustworthy implementations of communication protocols has come up several times. However, proving functional correctness of hand-written implementations turned out to be very challenging. SPARK contracts were often too low-level and cluttered with implementation details. Relating contracts back to a high-level protocol specification required expertise in the protocol as well as the proof technology.

To make verified communication protocols practical, we identified a number of gaps that had to be bridged. For example, valid sequences of messages in protocol exchanges depend on the values of exchanged messages and vice versa. Message formats and protocol behaviour need to be specified precisely enough to relate the formal model to the final implementation. At the same time, domain experts (who are not necessarily formal verification experts) must be able to understand and write such specifications. There also have to be tools to help them validate a formal specification against informal specifications or existing implementations, ideally before too many resources go into formal proof.

To address these challenges, we developed RecordFlux [https://www.adacore.com/record...], a domain-specific language and open-source [https://github.com/AdaCore/Rec...] toolset to formally specify binary communication protocols, generate provable SPARK code and validate formal specifications against existing implementations. Messages are modelled as directed acyclic graphs and protocol behaviour as communicating finite state machines. We prove various properties at the model level such that the generated SPARK code for message parsing and generation can be automatically proved to contain no runtime errors and adhere to the generated low-level contracts. Protocol designers can load RecordFlux specifications into Python to interact dynamically with existing implementations or validate them against recorded samples before verification.

In this talk we will present the RecordFlux technology and give an insight into a project with NVIDIA [https://www.adacore.com/papers...] where it was used to formally verify the SPDM security protocol targeting multiple tightly resource-constrained embedded secure elements.

Download Slides