Part of AdaCore's ongoing efforts under the HICLASS project is to demonstrate how the SPARK technology can play an integral part in the security-hardening of existing software libraries written in other non-security-oriented programming languages such as C. This blog post presents the first white paper under this work-stream, “Security-Hardening Software Libraries with Ada and SPARK”.
We're happy to announce our new programming competition, the Ada/SPARK Crate Of The Year Award! We believe the Alire package manager is a game changer for Ada/SPARK, so we want to use this competition to reward the people contributing to the ecosystem.
This post continues our adventures with SPARKNaCl - our verified SPARK version of the TweetNaCl cryptographic library. This time, we'll be looking at yet more performance improvement via proof-driven "operator narrowing", porting the library to GNAT Community 2021, and the effect that has on proof and performance of the code.
Women make up roughly 38% of the global workforce, yet they constitute only 10–20% of the engineering workforce. In the U.S., numbers suggest that 40% of women who graduate with engineering degrees never enter the profession or eventually leave it. Why? The reasons vary but primarily involve socio-economic constraints on women in general, workplace inequities, and lack of support for work-life balance. Sadly, history itself has often failed to properly acknowledge the instrumental contributions of women inventors, scientists, and mathematicians who have helped solve some of our world's toughest challenges. How can young women emulate their successes if they don't even know about them?
As we've seen previously in Ada 2022 support in GNAT, the support for Ada 2022 is now mostly there for everyone to take advantage of. We're now crossing fingers for this new revision to be officially stamped by ISO in 2022.
We are happy to announce that the GNAT Community 2021 release is now available via https://www.adacore.com/download. Here are some release highlights:
The Ada 2022 draft defines a new tasking profile named Jorvik (pronounced “Yourvick”), based directly on the standard Ravenscar profile. Jorvik relaxes certain restrictions in order to increase expressive power for real-time/embedded Ada and SPARK applications. We will explore the details in this blog entry.
I am following the evolution of the embedded Rust community and in particular the work of James Munns from Ferrous-Systems. One of the projects that caught my attention is bbqueue, a single producer, single consumer, lockless, thread safe queue, based on BipBuffers.
Ada has a concurrency construct known as “entry families” that, in some cases, is just what we need to express a concise, clear solution.
In the integrated development environment, GNAT Studio, there is now a plugin that inserts the generated Global contracts inline with the code.
Following my last blog entry, further experiments show how the performance of SPARKNaCl can be doubled (again), plus analysis of worst-case stack usage and code size at all optimization levels.
This blog goes into the details of both measuring and improving the runtime performance of SPARKNaCl on a real "bare metal" embedded target, and comparing results with those for the original "TweetNaCl" C implementation.
Like previous years, AdaCore will participate in FOSDEM. This time the event will be online only, but this won’t prevent us from celebrating Open Source software. AdaCore engineers will give two talks in the Safety and Open Source devroom, a topic at the heart of AdaCore since its inception.
Beyond the great look, the Mini SAM M4 provide a powerful 120 Mhz Microchip SAMD51 Cortex-M microcontroller, a couple of LEDs and a user button. Let's program it with Ada.
Using GNAT Pro with containerization technologies, such as Docker, is so easy, a whale could do it!
In this blog post I want to present a new tool that allows one to very quickly and easily start Ada programming on any ARM Cortex-M or RISC-V microcontroller.
Some of you may recall an AdaCore blog post written in 2017 by Thales engineer Lionel Matias titled "Leveraging Ada Run-Time Checks with Fuzz Testing in AFL". This insightful post took us on a journey of discovery as Lionel demonstrated how Ada programs, compiled using GNAT Pro and an adapted assembler pass can be subjected to advanced fuzz testing. In order to achieve this Lionel demonstrated how instrumentation of the generated assembly code around jump and label instructions, could be subjected to grey-box (path aware) fuzz testing (using the original AFL v2.52b as the fuzz engine). Lionel explained how applying the comprehensive spectrum of Ada runtime checks, in conjunction with Ada's strong typing and contract based programming, enhanced the capabilities of fuzz testing beyond the abilities of other languages. Ada's advanced runtime checking, for exceptions like overflows, and the scrutiny of Ada's design by contract assertions allow corner case bugs to be found whilst also utilising fuzz testing to verify functional correctness.
Charles Villard, Cyril Etourneau, Thomas Delecroix, Louise Flick worked together in the ADArrose project. It won the student prize in the Make with Ada 2019/20 competition. This project was originally posted on Hackster.io here. For those interested in participating in the 2020/21 competition, registration is now open and project submissions will be accepted until Jan 31st 2021, register here.
The AFT (Autonomous FireTruck) is a prototype of an autonomous firetruck that can put out fire without risking people's lives. This project won a finalist prize in the Make with Ada 2019/20 competition.
Guillermo Perez's project won a finalist prize in the Make with Ada 2019/20 competition. This project was originally posted on Hackster.io here. For those interested in participating in the 2020/21 competition, registration is now open and project submissions will be accepted until Jan 31st 2021, register here.
