AdaCore, a 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.
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.
“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 Leader. “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.”
For more information, go to www.adacore.com/recordflux.
© Technews Publishing (Pty) Ltd. | All Rights Reserved.
printer friendly version