AdaCore’s RecordFlux Technology Enables the Development of Provable, Secure Communication Protocols

May 16, 2023

Blog

AdaCore, a provider of software development and verification tools, recently launched its RecordFlux technology, designed to ease the development and security of binary communication protocols.

The technology comprises a Domain Specific Language (DSL) to precisely describe complex binary data formats and communication protocols, and a toolset to verify specifications and generate provable SPARK code that can be executed on a target CPU.

Through RecordFlux, users can define and implement complex communication protocols and prove security properties, such as memory safety, with lower costs and less effort than would be possible with a manual approach. The tool’s precision ensures that the specifications are unambiguous, and the high-level nature of the DSL makes the specifications easily understandable by domain experts. In addition, the expressive power of the DSL can capture the most complex real-world protocols. Because the RecordFlux code generator produces source code in the formal methods-based SPARK language, users can obtain automated proofs of a wide range of security properties in the resulting software.

RecordFlux is part of AdaCore’s tool stack for creating high-assurance implementations of binary data formats and communication protocols. The technology includes a DSL, a comprehensive toolset, and customized expert support. By using SPARK Pro, developers can take the SPARK code generated from RecordFlux specifications and automatically prove that the code is free of run-time errors and respects the original specification.

Code generated by RecordFlux is also compatible with GNAT Pro Assurance, AdaCore’s solution for projects with stringent requirements for reliability, long-term maintenance, or certification. The compiler-hardening options provided by GNAT Pro Assurance can be used to mitigate further attacks on network-facing protocol-handling code.