by
Nicolas Setton
–
Reducing Ada code bases with adareducer
How we're using Libadalang to create an automated Ada code reducer.
by
Yannick Moy
–
The Case for SPARK Evolution - an April First Parable
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.
by
Fabien Chouteau
–
The End of Binary Protocol Parser Vulnerabilities
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.
by
Maxim Reznik
–
Introduction to VSS library
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.
by
Paul Butcher
–
Automated Assurance through Differential Fuzzing
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.
by
Daniel King
–
Avoiding Vulnerabilities in Crypto Code with SPARK
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.
by
Johannes Kliemann
–
Adding Ada to Rust
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.
by
Yannick Moy
–
When Formal Verification with SPARK is the Strongest Link
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++.
by
Paul Butcher
–
Fuzzing Out Bugs in Safety-Critical Embedded Software
Fuzzing Out Bugs in Safety-Critical Embedded Software: Paul Butcher from AdaCore talks to Brandon Lewis from Embedded Toolbox
by
Fabien Chouteau
–
Embedded Ada/SPARK, There's a Shortcut
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.
by
Quentin Ochem
–
Announcing Publication of the Draft Ferrocene Language Specification
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.
I can’t believe that I can prove that it can sort
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.
by
Paul Jarrett
–
Ada Crate of the Year: Interactive code search
A retrospective on learning Ada and developing a tool with it in 2021 from 2021 Ada Crate of the Year Winner Paul Jarrett.
Quite Proved Image Format
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.
by
Fabien Chouteau
–
Ada GameDev Part 2: Making 2D maps with Tiled
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.
by
Manuel Hatzl
(B&R)
–
SPARK Crate of the Year: Unbounded containers in SPARK
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
by
Fabien Chouteau
–
Ada GameDev Part 1: GEneric Sprite and Tile Engine (GESTE)
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.
Proving the Correctness of GNAT Light Runtime Library
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.
by
Yannick Moy
–
SPARKNaCl - Two Years of Optimizing Crypto Code in SPARK (and counting)
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.
by
Paul Butcher
–
Fuzz Testing in International Aerospace Guidelines
Through the HICLASS UK research group, AdaCore has been developing security-focused software development tools that are aligned with the objectives stated within the avionics security standards. In addition, they have been developing further guidelines that describe how vulnerability identification and security assurance activities can be described within a Plan for Security Aspects of Certification.