Bridging the Gap between Protocol Specification and Program Verification

ABSTRACT

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 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. Valid sequences of messages in protocol exchanges depend on the values of exchanged messages and vice versa. Message formats and protocol behavior 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.

As a result, we developed RecordFlux [1], a domain-specific language and open-source [2] toolset to formally specify binary communication protocols, generate provable SPARK code and validate formal specifications against existing implementations. Messages are modeled as directed acyclic graphs and protocol behavior 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 [3] where it was used to formally verify the SPDM security protocol targeting multiple tightly resource-constrained embedded secure elements. We would like to take the opportunity to discuss possible future directions of our technology with the HCSS community, in particular ways to integrate with model-checking, cryptography proofs and different target languages.

[1] https://www.adacore.com/recordflux

[2] https://github.com/AdaCore/RecordFlux

[3] https://www.adacore.com/papers/nvidia-using-recordflux-and-spark-to-implement-spdm-for-secure-computing

Author

Alexander Senier leads the RD group and the RecordFlux team at AdaCore. He has a background in high-security and mobile security. Since he first started programming more than 30 years ago, he has been wondering how software can be made such that it is guaranteed to behave as desired. Consequently, he is a proponent of practical formal verification and a user of the SPARK language for almost 15 years. In 2017, he founded Componolit, the company which created the RecordFlux technology to extend the industrial verification capabilities of SPARK to communication protocols. Today, the RecordFlux team is part of AdaCore and the technology is helping customers to realize formally-verified high-assurance systems.