RecordFlux is a technology that enhances the development and security of binary communication protocols. It comprises a Domain Specific Language (DSL) to precisely describe complex binary data formats and communication protocols, and a toolset to formally verify specifications and generate provable SPARK code that can be executed on the target CPU.
When you have a communication protocol to implement, RecordFlux helps you do it faster and enables you to trust the outcome.
Protects against cyber-attacks
Interaction between software components is governed by protocol and format specifications. Unfortunately, most standard specifications are incomplete or need to be translated to software implementations manually, leaving room for human error. In addition, logic errors and critical flaws are often poorly mitigated by the widespread use of unsafe programming languages. Consequently, many implementations contain severe security vulnerabilities that are just waiting to be discovered and exploited by malicious actors. BrakTooth, Infra:Halt, and Heartbleed are just a few high-profile security bugs highlighting severe security breaches resulting from vulnerabilities in communication protocols.
With RecordFlux, protocol specifications can be described formally in the DSL, which can be written and understood by domain experts which are not necessarily programmers or verification engineers. RecordFlux’s DSL is optimized for binary formats and communication protocols, to avoid any compromise on performance. The SPARK code that is generated from a valid RecordFlux specification can automatically be proven at gold level, i.e. it contains no runtime errors and key properties – namely the behavior with respect to the specification – can be shown. Consequently, communication code developed with RecordFlux can be protected against the above vulnerabilities.
The compiler hardening options provided by GNAT Pro Assurance can be used to further mitigate attacks on network-facing protocol handling code.
Proves memory safety and absence of low-level vulnerabilities like buffer overflows.
Buffer overflow ranks high in the Common Weakness Enumeration (CWE) and SANS Top 25 Most Dangerous Software Errors. It occurs when a program or process attempts to write more data to a fixed-length block of memory, or buffer, than the buffer is allocated to hold. Buffers contain a defined amount of data; any extra data will overwrite data values in memory addresses adjacent to the destination buffer. Exploiting a buffer overflow allows an attacker to control or crash a process or to modify its internal variables.
As mentioned above, the SPARK code that is generated from a valid RecordFlux specification can be automatically proven to be free of run-time errors, and thus verifiably free of any buffer overrun/underrun, integer overflow, or dereferencing of null pointers.
Saves time and money by automating provable code generation
The amount of code necessary for real-world data format and protocol implementations can often exceed the limit of what is formally provable and affordable with a manual implementation.
The RecordFlux toolset addresses this challenge by providing a high-level language, tailored towards data formats and communication protocols, that is precise enough to generate complex, formally-provable source code automatically, saving both time and money.
Eases definition and maintenance of in-house protocols
While standard implementations receive at least a certain level of scrutiny by the open source community and independent researchers, the situation is worse for custom data formats and protocol implementations. Specifications (if present at all) and implementations are only reviewed by a few people. Ad hoc design decisions out of urgent project needs complicate parsers and state machine implementations.
With RecordFlux, development of in-house protocols is based on readable, easily comprehensible specifications, which are automatically checked to help guarantee functional correctness.
Provides full stack support, from model to binary codes with high-assurance compilers
RecordFlux is part of AdaCore’s tool stack for creating high-assurance implementations of binary data formats and communication protocols.
Specifications of protocols in RecordFlux’s DSL are automatically checked for determinism (no contradictory conditions), liveness (no cycles), reachability (no unused fields), coherency (no overlaps) and completeness (no holes).
Using SPARK Pro, SPARK code generated from RecordFlux specifications is automatically proven to be free of runtime errors and to respect the original specification.
Code generated by RecordFlux is compatible with GNAT Pro Assurance, AdaCore’s complete solution for projects with the most stringent requirements for reliability, long-term maintenance, or certification. Only a minimum of runtime features are necessary, which allows for using the code from full-blown servers down to embedded bare-metal scenarios. The compiler hardening options provided by GNAT Pro Assurance can be used to further mitigate attacks on network-facing protocol handling code.