Software enables provably secure communication protocols
AdaCore has developed technology to ease the development and security of binary communication protocols and tackle the most common security vulnerabilities in embedded devices.
RecordFlux uses 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 processor or microcontroller.
- Securing the world of electronics
- AdaCore teams for safety-critical Rust toolchain
- AdaCore opens new centre-of-excellence in UK
The software allows developers to 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 comes form Adacore’s experience with formal languages and ensures that the specifications are unambiguous while making the specifications easily understandable by domain experts.
The RecordFlux code generator produces source code in the formal methods-based SPARK language so that users can obtain automated proofs of a wide range of security properties in the resulting software. The result is secure and reliable code at lower cost.
“Logic errors and critical flaws are often poorly mitigated by the widespread use of unsafe programming languages, resulting in severe security vulnerabilities,” said Alex Senier, AdaCore’s RecordFlux Team Lead, Lead of Research Directions and Managing Director at AdaCore GmbH. “Unfortunately, most specification documents are complex texts written in English which need to be translated to software implementations manually, leaving room for human error.”
“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,” he said.
This means many implementations with 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 compiler hardening options provided by GNAT Pro Assurance can be used to further mitigate attacks on network-facing protocol handling code. This proves memory safety and absence of low-level vulnerabilities like buffer overflows, which rank high in the Common Weakness Enumeration (CWE) and the Top 25 Most Dangerous Software Errors.
Buffer overflows occur 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.
The SPARK code 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 de-referencing of null pointers.
www.adacore.com/recordflux; blog.adacore.com/the-end-of-binary-protocol-parser-vulnerabilities
If you enjoyed this article, you will like the following ones: don't miss them by subscribing to :
