This week we announced a new tool RecordFlux. The goal of RecordFlux is to address one of the most critical parts of the software stack in terms of se

The End of Binary Protocol Parser Vulnerabilities | The AdaCore Blog

submited by
Style Pass
2023-04-02 00:30:02

This week we announced a new tool RecordFlux. The goal of RecordFlux is to address one of the most critical parts of the software stack in terms of security, binary protocol parsers/serializers.

From a protocol specification written in the RecordFlux Domain Specific Language (DSL), the tool can generate provable SPARK code. This means memory safety (no buffer overruns), absence of integer overflow errors, and even proof of functional properties. In this blog post I will try to explain how this is a game changer for cybersecurity.

We will invent a trivial protocol for a remote service to push opaque data (i.e., “raw” bytes that will be appropriately interpreted by application code) onto a stack in a remote server, and then see how you can use RecordFlux to generate binary communication protocol parsers/synthesizes and prove the correct usage with SPARK. Our trivial protocol will be aptly named Remote Stack Protocol (RSP).

The examples I am going to show here require recent GNAT Pro compiler and SPARK Pro releases as RecordFlux is using bleeding edge features from both technologies.

Leave a Comment