Ada/SPARK Crate Of The Year 2022 Winners Announced!

by Fabien Chouteau – Jan 31, 2023

In June of 2022 we launched the second edition of the Ada/SPARK Crate Of The Year Awards. We believe the Alire source package manager is a game changer for Ada/SPARK, so we want to use this competition to reward the people contributing to the ecosystem. Today we are pleased to announce the results.

But first, we want to congratulate all the participants, and the Alire community at large, for reaching 320 crates in the ecosystem in January of this year. We truly believe in a bright future for the Ada/SPARK open-source ecosystem with Alire at the forefront. Reaching this milestone is a great sign,both inside and outside the Ada/SPARK community, of the evolution and the energy of the ecosystem.

Without further ado, the winners of the 2022 Ada/SPARK Crate of the Year Awards are:

The SPARK Crate of the Year Prize is awarded to libkeccak by Daniel King.

The security of any system can only be as strong as its weakest links. However, cryptographic libraries often require a higher level of scrutiny because of the complexity of their algorithms and implementations. This is why SPARK’s formal verification approach is a very powerful solution for the development and maintenance of such components.

Daniel King delivers a very good example with the libkeccak project. An implementation of the keccak cryptographic hash which has been selected by the National Institute of Standards and Technology (NIST) for the SHA-3 standard. I am not going to delve into details here because Daniel already published on our blog this article about his project a few months ago.

Daniel published the article a couple weeks after a critical vulnerability in the keccak reference implementation was disclosed: an overflow on integer addition leading to a buffer overflow. This is an example of how memory vulnerabilities are often the result of a computation error beforehand. The vulnerability remained undetected for more than a decade. As mentioned recently in the case study we published with the NVIDIA Security Team, “traditional” means of software validations are not sufficient to ensure security. With SPARK, Daniel was able to prove that none of those run-time errors can occur for any possible input to the library.

The Embedded Crate of the Year Prize is awarded to AVR-Ada by Rolf Ebert.

Despite the arrival of competing 32-bit platforms such as ARM Cortex-M or RISC-V32 years ago, AVR microcontrollers are still widely used in embedded systems and will remain a major platform for years to come. This is why we are very happy to see AVR-Ada making AVR microcontrollers easily accessible via the Alire ecosystem.

AVR-Ada is one of the first, if not the first, open-source low level embedded Ada projects. Rolf, who has been leading the project since the beginning, has now adapted it to the Alire workflow. The result is a collection of crates covering the run-times, access to peripherals, and common features such as time keeping or string manipulation.

One specific challenge addressed by Rolf is the wide variety of devices in the AVR family. There are 94 different microcontrollers supported in AVR-Ada! On the implementation side, the project is using hardware description files provided by the vendor to generate specifications and peripheral representations in Ada. On the user side, an Alire feature provides a way to specify which one of those devices is targeted.

The feature is called “crate configuration”, a way for crates to expose a list of variables that can be set by other crates depending on them. These variables are then converted to constants in Ada and GPR files which in turn alter the behavior/implementation of the crate. This is particularly useful for embedded applications where compile time allocations and optimizations are crucial.

For example, the avr_mcu crate defines the following variables:

[configuration.variables]
AVR_MCU         = { type = "String", default = "atmega328p" }
Sec_Stack_Size  = { type = "Integer", first = 0, last = 1024, default = 63 }
Clock_Frequency = { type = "Integer", first = 0, default = 0 }

As a user, if I want to develop an application for the Arduino UNO which is equipped with an ATmega328P, I only have to set the variable in my crate’s manifest file (alire.toml):

[[depends-on]]
avrada_mcu = “^2.2.0”
avrada_lib = “^2.1.0”

[configuration.values]
avrada_rts.AVR_MCU = “atmega328p”
avrada_rts.Clock_Frequency = 16000000

and all the AVR-Ada libraries will be correctly configured.

There are so many opportunities for interesting projects with AVR, you can expect at least one post using AVR-Ada on this blog.

The Ada Crate of the Year Prize is awarded to Rejuvenation-Ada by Piërre van de Laar and Arjan Mooij.

Rejuvenation is a pattern based code manipulation tool designed to automate the maintenance of Ada projects. It builds on top of Libadalang's general analysis features to create an easy to use interface specialized for implementing code refactorings. At AdaCore, tooling is obviously a topic dear to our heart, so we are really pleased to see this project in the Alire ecosystem.

Rejuvenation provides a familiar interface for its users as the code manipulation patterns are written in Ada. Taking an example from the documentation this is a find pattern:

if $S_Cond then
   $S_Dest := True;
else
   $S_Dest := False;
end if;

And the corresponding replace pattern:

$S_Dest := $S_Cond;

As you can see, it’s fairly easy for any Ada programmer to understand what is going on and in turn implement their own refactoring patterns.

Conclusion

Thanks again to all the participants and stay tuned for more news on the Ada/SPARK Crate Of The Year Awards.

Posted in

About Fabien Chouteau

Fabien joined AdaCore in 2010 after his engineering degree at the EPITA (Paris). He is involved in real-time, embedded and hardware simulation technology. Maker/DIYer in his spare time, his projects include electronics, music and woodworking.