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.
According to AdaCore, 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.
Since the RecordFlux code generator produces source code in the formal methods-based SPARK language, users will also be able to obtain automated proofs of a wide range of security properties in the resulting software. The net effect is said to be more secure and reliable code, at lower cost.
“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.”
Code generated by RecordFlux is compatible with GNAT Pro Assurance, AdaCore’s 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.
