In a previous post we presented the RecordFlux specification language and toolset, illustrating how to design and generate formally proven binary protocol parsers and serializers. In this follow-up we will look at the protocol session part of RecordFlux.
How we're using Libadalang to create an automated Ada code reducer.
SPARK already allows you to specify functional contracts by cases, and soon it will allow you to specify cases that lead to an exception. But what about all the other cases? Should we put all our eggs in the same case? Discover what's cooking up for you on the side of language evolution.
This week we announced a new tool called 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.
The VSS (as an abbreviation for Virtual String Subsystem) library is designed to provide advanced string and text processing capabilities. It offers a convenient and robust API that allows developers to work with Unicode text, regardless of its internal representation. In this article, we will introduce you to the library and explain its purpose, highlighting its usefulness for developers working in this area.
This blog describes the concept and benefits of differential fuzz testing. In addition, the post describes setting up, executing and analyzing the results of a differential fuzzing campaign for the Libkeccak and XKCP cryptographic libraries.
Writing secure software in C is hard. It takes just one missed edge case to lead to a serious security vulnerability, and finding such edge cases is difficult. This blog post discusses a recent vulnerability in a popular SHA-3 library and how the same problems were avoided in my own SHA-3 library written in SPARK.
While implementing application logic in Ada or SPARK is an improvement over a pure C project, its weakest link is still the C code in the SDK. On the other hand, there are many libraries, board support packages, and SDKs written in Rust, easily usable with Cargo. So instead of building the Ada application on top of a C base, one could use a Rust base instead to combine the large catalog of ready-to-use software with Rust's safety features, providing a much more solid base for an Ada project.
Security is only as strong as its strongest link. That's important to keep in mind for software security, with its long chain of links, from design to development to deployment. Last year, members of NVIDIA's Offensive Security Research team (aka "red team") presented at DEF CON 29 their results on the evaluation of the security of a firmware written in SPARK and running on RISC-V. The ended up not finding vulnerabilities in the code, but in the RISC-V ISA instead. This year, the same team presented at DEF CON 30 a retrospective on the security evaluation of 17 high-impact projects since 2020. TL;DR: using SPARK makes a big difference for security, compared to using C/C++.
Fuzzing Out Bugs in Safety-Critical Embedded Software: Paul Butcher from AdaCore talks to Brandon Lewis from Embedded Toolbox
For years in this blog my colleagues and I have published examples, demos, and how-to’s on Ada/SPARK embedded (as in bare-metal) development. Most of the time, if not always, we focused on one way of doing things: to start from scratch and write everything in Ada/SPARK, from the low level drivers to the application. While this way of doing Ada/SPARK embedded will yield the best results in terms of software quality, it might not be the most efficient in all cases. In this blog post I want to present an alternative method to introduce Ada/SPARK into your embedded development projects.
We are pleased to announce the publication of the initial draft of the Ferrocene Language Specification (FLS) - a qualification-oriented document that details the Rust language as it specifically relates to Ferrocene.
When an enthusiastic Ada programmer and a SPARK expert pair up to prove the most "stupid" sorting algorithm, lessons are learned! Join us in this eye-opening journey.
A retrospective on learning Ada and developing a tool with it in 2021 from 2021 Ada Crate of the Year Winner Paul Jarrett.
A few weeks ago a piece of code went viral in the online dev community. The “Quite OK Image Format” (QOI) is a fast, lossless image compression designed to have a very simple implementation (about 300 lines of C). Shortly, a few alternative implementations popped up here and there, and in this kind of situation we are eager to show what Ada/SPARK can bring to the table.
In this second post of the Ada GameDev series we will see how to create game maps and export them to a format that is compatible with the GESTE library.
Manuel Hatzl is the winner of the 2021 SPARK Crate of the year! In this blog post he shares his experience using Ada/SPARK and how he created the spark_unbound library
In this first entry of the series, I want to present my GEneric Sprite and Tile Engine (GESTE) project. The goal of GESTE is to bring the rendering and anesthetic of 8bit era game consoles to modern microcontrollers.
The GNAT light runtime library is a version of the runtime library targeted at embedded platforms and certification, which has been certified for use at the highest levels of criticality in several industrial domains. It contains around 180 units focused mostly on I/O, numerics, text manipulation, memory operations. We have used SPARK to prove the correctness of 40 of them: that the code is free of runtime errors, and that it satisfies its functional specifications.
SPARKNaCl is a SPARK version of the TweetNaCl cryptographic library, developed by formal methods and security expert Rod Chapman. For two years now, Rod has been developing and optimizing this open-source cryptographic library while preserving the automatic type-safety proof across code changes and tool updates. He has recently given a talk about this experience that I highly recommend.