AdaCore, a trusted provider of software development and verification tools, today announced the launch of its new 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, at much less cost and effort than would be possible with a manual approach. The precision of the RecordFlux DSL ensures that the specifications are unambiguous, the high-level nature of the DSL makes the specifications easily understandable by domain experts, and the expressive power of the DSL can capture the most complex real-world protocols. And since 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. The net effect is more secure and reliable code, at lower cost.
“With RecordFlux, we aim to provide a solution that saves time and money by automating provable code generation while ensuring the absence of low-level vulnerabilities like buffer overflows that attackers could exploit.”
“Interaction between software components is governed by protocol and format specifications. Unfortunately, most specification documents are complex texts written in English which need to be translated to software implementations manually, leaving room for human error,” said Alex Senier, AdaCore’s RecordFlux Team Lead. “Logic errors and critical flaws are often poorly mitigated by the widespread use of unsafe programming languages, resulting in severe security vulnerabilities. With RecordFlux, we aim to provide a solution that saves time and money by automating provable code generation while ensuring the absence of low-level vulnerabilities like buffer overflows that attackers could exploit.”
About RecordFlux
RecordFlux is part of AdaCore’s tool stack for creating high-assurance implementations of binary data formats and communication protocols. The technology includes a Domain Specific Language, 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 complete solution for projects with the most 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.