38 entries tagged with #Libraries
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 Fabien Chouteau
Ada/SPARK Crate Of The Year 2022 Winners Announced!
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.
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 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 Fabien Chouteau
A New Era For Ada/SPARK Open Source Community
Today we have two exciting announcements for the future of the Ada/SPARK ecosystem.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.by Manuel Hatzl
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 libraryby Quentin Ochem , Florian Gilcher
AdaCore and Ferrous Systems Joining Forces to Support Rust
For over 25 years, AdaCore has been committed to supporting the needs of safety- and mission-critical industries. This started with an emphasis on the Ada programming language and its toolchain, and over the years has been extended to many other technologies. AdaCore’s product offerings today include support for the Ada language and its formally verifiable SPARK subset, C and C++, and Simulink and Stateflow models. We have accomplished this while addressing the requirements of various safety standards such as DO-178B/C, EN 50128, ECSS-E-ST-40C / ECSS-Q-ST-80C, IEC 61508 and ISO 26262.
by Fabien Chouteau
An Embedded USB Device stack in Ada
A couple years ago I started to tackle what was probably my most daunting project at the time, an embedded USB Device stack written 100% in Ada.by Kyriakos Georgiou
Security-Hardening Software Libraries with Ada and SPARK
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”.
by Fabien Chouteau
AdaCore at FOSDEM 2021
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.by Fabien Chouteau
Ada on any ARM Cortex-M device, in just a couple minutes
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.by Paul Butcher
Finding Vulnerabilities using Advanced Fuzz testing and AFLplusplus v3.0
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.
by Juliana Silva

Make with Ada 2020: The autonomous firetruck
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.by Juliana Silva

Make With Ada 2020: High Integrity Sumobot
Blaine Osepchuk'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.
by Johannes Kliemann
Ada on the ESP8266
Not long ago, AdaCore published its LLVM frontend for GNAT. Also quite recently Espressif updated their LLVM backend to LLVM 9 which also happens to be the LLVM version of GNAT. This gave me to the idea to try out if LLVMs promise of providing modular and reusable toolchain technologies is true.by Martyn Pike
A Trivial File Transfer Protocol Server written in Ada
For an upcoming project, I needed a simple way of transferring binary files over an Ethernet connection with minimal (if any at all) user interaction. A protocol that's particularly appropriate for this kind of usage is the Trivial File Transfer Protocol (TFTP).by Fabien Chouteau
AdaCore at FOSDEM 2020
Like last year and the year before, AdaCore will participate to the celebration of Open Source software at FOSDEM. It is always a key event for the Ada/SPARK community and we are looking forward to meet Ada enthusiasts. You can check the program of the Ada/SPARK devroom here.
by Paul Butcher
AdaCore for HICLASS - Enabling the Development of Complex and Secure Aerospace Systems
What's changed?In 2019 AdaCore created a UK business unit and embarked on a new and collaborative venture researching and developing advanced UK aerospace systems. This blog introduces the reader to ‘HICLASS’, describes our involvement and explains how participation in this project is aligned with AdaCore’s core values.
by Isabelle Vialard
Secure Use of Cryptographic Libraries: SPARK Binding for Libsodium
The challenge faced by cryptography APIs is to make building functional and secure programs easy for the user. In this blog post I will present you how I created a SPARK binding for Libsodium, using strong typing and preconditions/postconditions to enforce a safe and functional use of basic cryptographic primitives.by Juan Zamorano
Using Ada for a Spanish Satellite Project
I am an Associate Professor at Polytechnic University of Madrid’s (Universidad Politécnica de Madrid / UPM) in the Department of Architecture and Technology of Computer Systems. For the past several years I have been directing a team of colleagues and students in the development of a UPMSat-2 microsatellite. The project originally started in 2013 as a follow-to the UPM-SAT 1, launched by an Ariane-4 in 1995.
by Boran Car

Bringing Ada To MultiZone
C is the dominant language of the embedded world, almost to the point of exclusivity. Due to its age, and its goal of being a “portable assembler”, it deliberately lacks type-safety, opening up exploit vectors. Proposed solutions are partitioning the application into smaller intercommunicating blocks, designed with the principle of least privilege in mind; and rewriting the application in a type-safe language. We believe that both approaches are complementary and want to show you how to combine separation and isolation provided by MultiZone together with iteratively rewriting parts in Ada. We will take the MultiZone SDK demo and rewrite one of the zones in Ada.by Yannick Moy , Nicolas Roche , Pierre-Marie de Rodat , Fabien Chouteau
AdaCore at FOSDEM 2019
Like last year, we've sent a squad of AdaCore engineers to participate in the celebration of Open Source software at FOSDEM. Like last year, we had great interactions with the rest of the Ada and SPARK Community in the Ada devroom on Saturday. That's what we have to say about it.by Rob Tice
AdaFractal Part1: Ada with a Portable GUI
The is the first part of a multiple part post that covers the development of the AdaFractal project. The idea was to create fractals in Ada. Here we will cover how to use AWS to create a flexible and portable way to display the generated fractals without using bulky graphics libraries.by Rob Tice

SPARKZumo Part 2: Integrating the Arduino Build Environment Into GPS
This is part #2 of the SPARKZumo series of blog posts. This post covers the build system that was used to build the SPARKZumo project and how to automate the process in GPS.by Felix Krause
The Road to a Thick OpenGL Binding for Ada: Part 2
This blog post is part two of a tutorial based on the OpenGLAda project and will cover implementation details such as a type system for interfacing with C, error handling, memory management, and loading functions.by Felix Krause

The Road to a Thick OpenGL Binding for Ada: Part 1
This blog post is part one of a tutorial based on the OpenGLAda project and will cover some the background of the OpenGL API and the basic steps involved in importing platform-dependent C functions.
by Lionel Matias
Leveraging Ada Run-Time Checks with Fuzz Testing in AFL
Fuzzing is a very popular bug finding method. The concept, very simple, is to continuously inject random (garbage) data as input of a software component, and wait for it to crash. If, like me, you find writing robustness test tedious and not very efficient in finding bugs, you might want to try fuzzing your Ada code.Here's a recipe to fuzz-test your Ada code, using American Fuzzy Lop and all the runtime checks your favorite Ada compiler can provide.Let's see (quickly) how AFL works, then jump right into fuzzing 3 open-source Ada libraries: ZipAda, AdaYaml, and GNATCOLL.JSON.by Manuel Iglesias Abbatermarco
Make with Ada 2017- Ada Based IoT Framework
SummaryThe Ada IoT Stack consists of an lwIp (“lightweight IP”) stack implementation written in Ada, with an associated high-level protocol to support embedded device connectivity nodes for today’s IoT world. The project was developed for the Make With Ada 2017 competition based on existing libraries and ported to embedded STM32 devices.
by Rob Tice
The Adaroombot Project
The Adaroombot project consists of an iRobot CreateⓇ 2 and Ada running on a Raspberry Pi with a Linux OS. This is a great Intro-to-Ada project as it focuses on a control algorithm and a simple serial communications protocol. The iRobot CreateⓇ 2 platform was originally design for STEM education and has great documentation and support - making it very easy to create a control application using Ada. This blog looks at the creation of the project and some cool features of Ada that were learned along the way.by Pat Rogers
Getting started with the Ada Drivers Library device drivers
The Ada Drivers Library (ADL) is a collection of Ada device drivers and examples for ARM-based embedded targets. The library is maintained by AdaCore, with development originally (and predominantly) by AdaCore personnel but also by the Ada community at large. It is available on GitHub and is licensed for both proprietary and non-proprietary use.
by Emmanuel Briot
GNAT On macOS Sierra
GNAT and all the tools work great on the newly released macOS Sierra, but gdb needs some tweaking of the system.by Quentin Ochem

Unity & Ada
Using Ada technologies to develop video games doesn’t sound like an an obvious choice - although it seems like there could be an argument to be made. The reverse, however, opens some more straightforward perspectives.by Emmanuel Briot

GNAT Programming Studio (GPS) on GitHub
The GPS source repository has been published on GitHub. This post briefly describes how you can access it, and hopefully contribute.by Emmanuel Briot
Traits-Based Containers
This post describes the design of a new containers library. It highlights some of the limitations of the standard Ada containers, and proposes a new approach using generic packages as formal parameters to make these new containers highly configurable at compile time.by Emmanuel Briot
Larger than it looks (storage pools)
This post shows how to implement a special storage pool that allocates an extra header every time it allocates some memory. This can be used to store type specific information, outside of the type itself.by Yannick Moy
