Homepage

Tetris in SPARK on ARM Cortex M4

Tetris is a well-known game from the 80's, which has been ported in many versions to all game platforms since then. There are even versions of Tetris written in Ada. But there was no version of Tetris written in SPARK, so we've repaired that injustice. Also, there was no version of Tetris for the Atmel SAM4S ARM processor, another injustice we've repaired.

Welcome To AdaCore's Blog

I'm proud, if not a bit nervous, to be the one firing the very first post on this brand new blog. Why are we starting a corporate blog at this time? There are many reasons for this. The main one is that there are many things happening at AdaCore and around the GNAT technology and we are seeking better ways to make them widely known while offering interested recipients the possibility to react and interact with us.

A Busy Schedule Ahead!

If you have a passion for Ada, need more information on our technology or would just like to have a chat, there are a couple of upcoming events where we'd love to meet up. What's more, we'll be launching our brand new product QGen at Embedded World!

ProofInUse is coming!

For lovers of verification tools and critical system (we know you're out there!), we are very excited to present ProofInUse!

AdaCore at FOSDEM'15

I was at Bruxelles on January 31st to present the components of GNAT GPL 2015 : SPARK 2014 and GNAT GPL for ARM bare-board. This is not unrelated to a previous blog entry on Tetris in SPARK on ARM Cortex M4, in particular I presented that Tetris demo (I brought some boards with me and despite the simple package, none were broken!). The slides contain technical details on the ravenscar profile (main principles), how to build a program for the stm32f4-discovery board and how to port the runtime. There are also less technical slides such as why we choose the stm32f4 board and photos of some graphical demos. As that could be useful to anyone interested in Ravenscar or in porting the runtime to other boards or other platforms, we've made the slides available here.

Testing, Static Analysis, and Formal Verification

I've recently written an article (in two parts) over at Electronic Design about applying different methods of verification to the same small piece of code. The code in question is an implementation of binary search, and I applied Testing, Static Analysis (using the AdaCore tool CodePeer) and Formal Verification (using the AdaCore tool SPARK 2014).

AdaCore Releases GNAT Pro 7.3, QGen 1.0 and GNATdashboard 1.0

February saw the annual customer release of a number of important products. This is no mean task when you consider the fact that GNAT Pro is available on over 50 platforms and supports over 150 runtime profiles (ranging from Full Ada Support to the very restricted Zero Footprint Profile suitable for safety-critical development). All in all, from the branching of the preview version to the customer release it takes us nearly 4 months to package everything up! Quality is assured through the internally developed AdaCore Factory.

20 years on...

20 Years of AdaCore: Company as Committed as Ever on Safety-Critical Software Solutions

QGen on Embedded News TV

Embedded News TV caught up with our own Matteo Bordin to talk about QGen. Matteo provides a nice overview of QGen and it's position in the industry as the need for safe and secure software becomes increasingly important.

What's in the Box?

Forget about the black box - we want you to see what's in the AdaCore box! Our machine room, the life blood of the company, is centered in the office space in a glass box and is pure eye candy for geeks and cable aficionados. The machine room is 204 sq ft (19 sq meters), contains 73 machines (running the gamut from VxWorks, Linux, Windows, Android and more) 1.5 miles of cables and a state of the art fire suppression mechanism! Oh and the modern air intake system gives it a green energy seal of approval. In the unlikely event of a fire; the smoke detectors allow 30 seconds before dispersing an agent called FM200 which will suppress the fire but not damage the equipment. The economizer takes advantage of winters' freeze and draws cool air from the outside to cool the machine room and the heated air is then spilled to common office areas thus reducing heating costs. We're proud to show-off the hardware side of our software!

A Building Code for Building Code

In a recent article in Communications of the ACM, Carl Landwehr, a renowned scientific expert on security, defends the view that the software engineering community is doing overall a poor job at securing our global information system and that this is mostly avoidable by putting what we know works to work, to the point that most vulnerabilities could be completely avoided by design if we cared enough. Shocking! Or so it should appear.

The latest Mixed Programming with Ada lectures at the AdaCore University

I recently joined AdaCore as a Technical Account Manager with an initial focus on the UK and Scandinavian regions, but for the last 12 months I've been busy working on the AdaCore University. The most recent addition to which is a course on Mixed Language Programming with Ada, and it includes lectures on the integration of Ada with C, C++ and Java. The course covers some advanced topics like mixed language object orientation, techniques for using Ada strong typing to combat known issue with C pointers and the pitfalls that are encountered when mixing native Ada code with Java at runtime. This course clearly demonstrates that Ada has strong support for integration with C, C++ and Java and it proves there are no technical barriers to its adoption in modern mixed language software systems.

The Year for #AdaLove

Despite her famously sharp analytical mind, it’s unlikely Ada Lovelace could have predicted the durability of her legacy as the world’s first computer programmer and pioneer for women in computing.

Verification on Ada code with Static and Dynamic Code Analysis - Webinar

One of the main challenges to get certification in Ada projects is the achievement of 100% code coverage but in most projects an amount of more than 95% structural coverage is hard to achieve. What can you do with the last 5% of code that can't be covered? DO-178C for example, provides a framework for the integration of various techniques in the development process to solve the problem. In this webinar you learn how static analysis and dynamic testing can help complete analysis for pieces of code that are not covered.

Project P Open Workshop

Project-P Open Workshop

Make with Ada: All that is useless is essential

A few weeks ago I discovered the wonderful world of solenoid engines. The idea is simple: take a piston engine and replace explosion with electromagnetic field. In this article I will experiment a solenoid engine using a hacked hard drive and a software controller on a STM32F4 .

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.

How to prevent drone crashes using SPARK

The Crazyflie is a very small quadcopter sold as an open source development platform: both electronic schematics and source code are directly available on their GitHub and its architecture is very flexible. Even if the Crazyflie flies out of the box, it has not been developed with safety in mind: in case of crash, its size, its weight and its plastic propellers won’t hurt anyone! But what if the propellers were made of carbon fiber, and shaped like razor blades to increase the drone’s performance? In theses circumstances, a bug in the flight control system could lead to dramatic events. In this post, I present the work I did to rewrite the stabilization system of the Crazyflie in SPARK 2014, and to prove that it is free of runtime errors. SPARK also helped me to discover little bugs in the original firmware, one of which directly related with overflows. Besides the Crazyflie, this work could be an inspiration for others to do the same work on larger and more safety-critical drones.

Count them all (reference counting)

Reference countingReference counting is a way to automatically reclaim unused memory. An element is automatically deallocated as soon as there are no more references to it in the program.

Farewell Robert...

It is with great sadness that I have to announce the death of Robert Dewar...

Make with Ada: "The Eagle has landed"

July 20, 1969, 8:18 p.m. UTC, while a bunch of guys were about to turn blue on Earth, commander Neil A. Armstrong confirms the landing of his Lunar Module (LM), code name Eagle, on the moon. Will you be able to manually land Eagle on the Sea of Tranquillity?

2015: A Space Ada‑ssey

AdaCore has a long history of providing tools and support to develop mission critical applications for Space. Check out this video we made and showed at the conference to see which ones!

Make with Ada : From bits to music

I started out as an electronic musician, so one of my original motivations when I learnt programming was so that I could eventually *program* the sounds I wanted rather than just use already existing software to do it.

Using reference types to handle persistent objects

The Ada 2012 standard introduced user-defined references. The main idea behind this is simplifying the access to elements in a container. But you can use them to control the life-circle of your persistent objects. Let's see how it could work.

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.

New Book About SPARK 2014

I am very pleased to announce that a book is now available for those who want to learn formal verification with SPARK 2014. This book was written by Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College. We've been interacting a lot with them since they started in 2013, and the result of these interactions is quite satisfying!

AdaCore Tech Days 2015

HIS Conference 2015, Bristol

We are excited to be sponsoring and exhibiting at the 2nd annual High Integrity Software conference, taking place on 5th November 2015 at The Royal Marriott Hotel in Bristol.

Make with Ada: Formal proof on my wrist

When the Pebble Time kickstarter went through the roof, I looked at the specification and noticed the watch was running on an STM32F4, an ARM cortex-M4 CPU which is supported by GNAT. So I backed the campaign, first to be part of the cool kids and also to try some Ada hacking on the device.

ARM TechCon and NBAA Conference 2015

We are continuing to develop tools for use within projects that require reliable and secure embedded software for ARM. Our engineering team have been busy creating demos running on ARM technology, such as Tetris in SPARK on ARM Cortex M4.

Calling inherited subprograms in Ada

This short post describes an idiom that can be used to help maintain complex hierarchies of tagged types, when methods need to call the parent types methods.

Modernizing Adacore's Open-Source Involvement

Through the adoption of GitHub we have taken our first step on the way to having a more collaborative and dynamic interaction with, both our users and open source technologies.

Dissimilar tools: Use cases and impact on tool qualification level

Frederick Pothon of ACG Solutions has recently published a document entitled - Dissimilar tools: Use cases and impact on tool qualification level on the open-DO blog.

Ada Lovelace Bicentennial

The three of us attended the Ada Lovelace Symposium in Oxford (UK). The two days were one fantastic discovery after another about the life, achievements and legacy of Ada Lovelace, the programming pioneer who lent her name to the Ada language.

Porting the Ada Runtime to a new ARM board

A step by step tutorial to adapt the ARM runtime to new MCUs/boards.

ERTS and Embedded World conferences 2016

We are pleased to announce that we will be a major sponsor and exhibitor at ERTS, Toulouse and will be exhibiting at Embedded World, Nuremberg in the coming months!

Formal Verification Made Easy!

We are pleased to announce our latest release of SPARK Pro! A product that has been jointly developed alongside our partner Altran and following the global AdaCore Tech Days, you can now see the SPARK 2014 talk, Formal Verification Made Easy by AdaCore’s Hristian Kirtchev, on YouTube.

QGen 2.1 Release!

Embedded World will see the latest release of QGen, the qualifiable and customisable code generator for Simulink® and Stateflow® models!

Make with Ada: Candy dispenser, with a twist...

A few months ago, my colleague Rebecca installed a candy dispenser in our kitchen here at AdaCore. I don’t remember how exactly, but I was challenged to make it more… fun.

Embedded Product Line Updates

Embedded products are not stand alone, this allows them to have safety, mission critical and real-time requirements that they wouldn’t necessarily have otherwise. The embedded product line provides analyzable, verifiable, and certifiable software for both static and dynamic analysis tools.

CubeSat continues to orbit the Earth thanks to Ada & SPARK!

Dr Carl Brandon of Vermont Technical College and his team of students used SPARK and Ada to successfully launch a satellite into space in 2013 and it has continued to orbit the Earth ever since! At our AdaCore Tech Days in Boston last year Dr Brandon explained further.

Formal Verification of Legacy Code

Just a few weeks ago, one of our partners reported a strange behavior of the well-known function Ada.Text_IO.Get_Line, which reads a line of text from an input file. When the last line of the file was of a specific length like 499 or 500 or 1000, and not terminated with a newline character, then Get_Line raised an exception End_Error instead of returning the expected string. That was puzzling for a central piece of code known to have worked for the past 10 years! But fair enough, there was indeed a bug in the interaction between subprograms in this code, in boundary cases having to do with the size of an intermediate buffer. My colleague Ed Schonberg who fixed the code of Get_Line had nonetheless the intuition that this particular event, finding such a bug in an otherwise trusted legacy piece of code, deserved a more in depth investigation to ensure no other bugs were hiding. So he challenged the SPARK team at AdaCore in checking the correctness of the patched version. He did well, as in the process we uncovered 3 more bugs.

Provably safe programming at Embedded World

AdaCore continues to build reliable and secure software for embedded software development tools. Last month, we attended Embedded World 2016, one of the largest conferences of its kind in Europe, to present our embedded solutions and our expertise for safety, and mission critical applications in a variety of domains.

Simics helps run 60 000 GNAT Pro tests in 24 hours

This post has been updated in March 2017 and was originally posted in March 2016.

Efficient use of Simics for testing

As seen in the previous blog article, AdaCore relies heavily on virtualisation to perform the testing of its GNAT Pro products for VxWorks.

VectorCAST/Ada: Ada 2012 Language Support

We are pleased to announce that on April 27th our partner, Vector, will host a webinar to showcase their latest VectorCAST/Ada release!

Certification and Qualification

AdaCore provides several tools with certification and qualification capabilities, for the rail and avionics industry. Quentin Ochem’s presentation on “Certification and Qualification” at the 2015 AdaCore Tech Days in Boston, Massachusetts provided more information about these two standards, namely DO-178C and EN:50128:2011.

Make with Ada: ARM Cortex-M CNC controller

I started this project more than a year ago. It was supposed to be the first Make with Ada project but it became the most challenging from both, the hardware and software side.

C library bindings: GCC plugins to the rescue

I recently started working on an Ada binding for the excellent libuv C library. This library provides a convenient API to perform asynchronous I/O under an event loop, which is a popular way to develop server stacks. A central part of this API is its enumeration type for error codes: most functions use it. Hence, one of the first things I had to do was to bind the enumeration type for error codes. Believe it or not: this is harder than it first seems!

Introducing the Make With Ada competition!

If you’ve been looking for a way to start your next embedded project in Ada or SPARK. Then, look no further than the Make with Ada competition!

Bookmarks in the GNAT Programming Studio (GPS)

As we improve existing views in GPS, we discover new ways to use them. This post shows some of the improvements done recently in the Bookmarks view, and how you can now use it as a TODO list.

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.

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.

Debugger improvements in GPS 17

The GNAT Programming Studio support for the debugger has been enhanced. This post describes the various changes you can expect in this year's new release of GPS.

Simplifying our product versioning

Looking at the list of product versions that were expected for 2017 it became clear that we had to review the way we were handling product versioning.

Verified, Trustworthy Code with SPARK and Frama-C

Last week, a few of us at AdaCore have attended a one-day workshop organized at Thales Research and Technologies, around the topic of "Verified, trustworthy code - formal verification of software". Attendees from many different branches of Thales (avionics, railway, security, networks) were given an overview of the state-of-practice in formal verification of software, focused on two technologies: the SPARK technology that we develop at AdaCore for programs in Ada, and the Frama-C technology developed at CEA research labs for programs in C. The most interesting part of the day was the feedback given by three operational teams who have experimented during a few months with either SPARK (two teams) or Frama-C (one team). The lessons learned by first-time adopters of such technologies are quite valuable.

Integrate new tools in GPS

This blog, the first in a series, explains the basic mechanisms that GPS (the GNAT Programming Studio) provides to integrate external tools. A small plugin might make your daily workflow more convenient by providing toolbar buttons and menus to spawn your tool and parse its output.

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.

Integrate new tools in GPS (2)

Customizing build target switchesIn the first post in this series (Integrate new tools in GPS) we saw how to create new build targets in GPS to spawn external tools via a menu or toolbar button, and then display the output of that tool in its own console, as well as show error messages in the Locations view.

Driving a 3D Lunar Lander Model with ARM and Ada

One of the interesting aspects of developing software for a bare-board target is that displaying complex application-created information typically requires more than the target board can handle. Although some boards do have amazing graphics capabilities, in some cases you need to have the application on the target interact with applications on the host. This can be due to the existence of special applications that run only (or already) on the host, in particular.

Make With Ada Winners Announced!

Judging for the first annual Make with Ada competition has come to an end and we can now reveal the results.

Make with Ada: DIY instant camera

There are moments in life where you find yourself with an AdaFruit thermal printer in one hand, and an OpenMV camera in the other.

Building High-Assurance Software without Breaking the Bank

AdaCore will be hosting a joint webcast next Monday 12th December 2pm ET/11am PT with SPARK experts Yannick Moy and Rod Chapman. Together, they will present the current status of the SPARK solution and explain how it can be successfully adopted in your current software development processes.

New Year's Resolution for 2017: Use SPARK, Say Goodbye to Bugs

​NIST has recently published a report called "Dramatically Reducing Software Vulnerabilities"​ in which they single out five approaches which have the potential for creating software with 100 times fewer vulnerabilities than we do today. One of these approaches is formal methods. Among formal methods, the report highlights strong suits of SPARK, and cites SPARK projects as example of mature uses of formal methods. NIST is not the only ones to support the use of SPARK. Editor Bill Wong from Electronic Design has included SPARK in his "2016 Gifts for the Techie". So if your new year's resolutions include software without bugs, have a look at SPARK in 2017.

Introducing Libadalang

AdaCore is working on a host of tools that works on Ada code. The compiler, GNAT, is the most famous and prominent one, but it is far from being the only one. At AdaCore, we already have several other tools to process Ada code: the ASIS library, GNAT2XML, the GPS IDE. A realization of the past years, however, has been that we were lacking a unified solution to process code that is potentially evolving, potentially incorrect Ada code. Hence Libadalang.

Going After the Low Hanging Bug

At AdaCore, we have a strong expertise in deep static analysis tools (CodePeer and SPARK), and we have been relying on the compiler GNAT and our coding standard checker GNATcheck to deal with more syntactic or weakly-semantic checks. The recent Libadalang technology, developed at AdaCore, provided us with an ideal basis to develop specialized light-weight static analyzers. As an experiment, we implemented two simple checkers using the Python binding of Libadalang. The results on our own codebase were eye-opening: we found a dozen bugs in the codebases of the tools we develop at AdaCore (including the compiler and static analyzers).

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.

SPARK Tetris on the Arduboy

One of us got hooked on the promise of a credit-card-size programmable pocket game under the name of Arduboy and participated in its kickstarter in 2015. The kickstarter was successful (but late) and delivered  the expected working board in mid 2016. Of course, the idea from the start was to program it in Ada , but this is an 8-bits AVR microcontroller (the ATmega32u4 by Atmel) not supported anymore by GNAT Pro. One solution would have been to rebuild our own GNAT compiler for 8-bit AVR from the GNAT FSF repository and use the AVR-Ada project. Another solution, which we explore in this blog post, is to use the SPARK-to-C compiler that we developed at AdaCore to turn our Ada code into C and then use the Arduino toolchain to compile for the Arduboy board.

AdaCore attends FOSDEM

Earlier this month AdaCore attended FOSDEM in Brussels, an event focused on the use of free and open source software. Two members of our technical team presented.

A Usable Copy-Paste Detector in A Few Lines of Python

After we created lightweight checkers based on the recent Libadalang technology developed at AdaCore, a colleague gave us the challenge of creating a copy-paste detector based on Libadalang. It turned out to be both easier than anticipated, and much more efficient and effective than we could have hoped for. In the end, we hope to use this new detector to refactor the codebase of some of our tools, and we expect to integrate it in our IDEs.

New strings package in GNATCOLL

This post describes the new GNATCOLL.Strings package, and the various optimizations it performs to provide improved performance.

User-friendly strings API

User friendly strings APIIn a previous post, we described the design of a new strings package, with improved performance compared to the standard Ada unbounded strings implementation. That post focused on various programming techniques used to make that package as fast as possible.

Writing on Air

While searching for motivating projects for students of the Real-Time Systems course here at Universitat Politècnica de València, we found a curious device that produces a fascinating effect. It holds a 12 cm bar from its bottom and makes it swing, like an upside-down pendulum, at a frequency of nearly 9 Hz. The free end of the bar holds a row of eight LEDs. With careful and timely switching of those LEDs, and due to visual persistence, it creates the illusion of text... floating in the air!

GNATcoverage moves to GitHub

Following the current trend, the GNATcoverage project moves to GitHub! Our new address is: https://github.com/AdaCore/gnatcoverage

GPS for bare-metal developers

In my previous blog article, I exposed some techniques that helped me rewrite the Crazyflie’s firmware from C into Ada and SPARK 2014, in order to improve its safety.

(Many) More Low Hanging Bugs

We reported in a previous post our initial experiments to create lightweight checkers for Ada source code, based on the new Libadalang technology. The two checkers we described discovered 12 issues in the codebase of the tools we develop at AdaCore. In this post, we are reporting on 6 more lightweight checkers, which have discovered 114 new issues in our codebase. This is definitely showing that these kind of checkers are worth integrating in static analysis tools, and we look forward to integrating these and more in our static analyzer CodePeer for Ada programs.

DIY Coffee Alarm Clock

A few weeks ago one of my colleagues shared this kickstarter project : The Barisieur. It’s an alarm clock coffee maker, promising to wake you up with a freshly brewed cup of coffee every morning. I jokingly said “just give me an espresso machine and I can do the same”. Soon after, the coffee machine is in my office. Now it is time to deliver :)

Ada on the first RISC-V microcontroller

Updated July 2018

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.

GNAT GPL 2017 is out!

For those users of the GNAT GPL edition, we are pleased to announce the availability of the 2017 release of GNAT GPL and SPARK GPL.

Pretty-Printing Ada Containers with GDB Scripts

When things don’t work as expected, developers usually do one of two things: either add debug prints to their programs, or run their programs under a debugger. Today we’ll focus on the latter activity.

Highlighting Ada with Libadalang

While we are working very hard on semantic analysis in Libadalang, it is already possible to leverage its lexical and syntactic analyzers. A useful example for this is a syntax highlighter.

Physical Units Pass the Generic Test

The support for physical units in programming languages is a long-standing issue, which very few languages have even attempted to solve. This issue has been mostly solved for Ada in 2012 by our colleagues Ed Schonberg and Vincent Pucci who introduced special aspects for specifying physical dimensions on types. This dimension system did not attempt to deal with generics though. As was noted by others, handling generics in a dimensional analysis that is, like in GNAT, a compile-time analysis with no impact on the executable size or running time, is the source of the problem of dimension handling. Together with our partners from Technical Universitat München, we have finally solved this remaining difficulty.

There's a mini-RTOS in my language

The first thing that struck me when I started to learn about the Ada programing language was the tasking support. In Ada, creating tasks, synchronizing them, sharing access to resources, are part of the language

Make with Ada 2017: Brushless DC Motor Controller

This project involves the design of a software platform that provides a good basis when developing motor controllers for brushless DC motors (BLDC/PMSM). It consist of a basic but clean and readable implementation of a sensored field oriented control algorithm. Included is a logging feature that will simplify development and allows users to visualize what is happening. The project shows that Ada successfully can be used for a bare-metal project that requires fast execution.

Welcoming New Members to the GNAT Pro Family

As we see the importance of software grow in applications, the quality of that software has become more and more important. Even outside the mission- and safety-critical arena customers are no longer accepting software failures (the famous blue screens of death, and there are many...). Ada has a very strong answer here and we are seeing more and more interest in using the language from a range of industries. It is for this reason that we have completed our product line by including an entry-level offer for C/C++ developers wanting to switch to Ada and reinforced our existing offer with GNAT Pro Assurance for programmers building the most robust software platforms with life cycles spanning decades.

Make with Ada 2017- A "Swiss Army Knife" Watch

SummaryThe Hexiwear is an IoT wearable development board that has two NXP Kinetis microcontrollers. One is a K64F (Cortex-M4 core) for running the main embedded application software. The other one is a KW40 (Cortex M0+ core) for running a wireless connectivity stack (e.g., Bluetooth BLE or Thread). The Hexiwear board also has a rich set of peripherals, including OLED display, accelerometer, magnetometer, gryroscope, pressure sensor, temperature sensor and heart-rate sensor. This blog article describes the development of a "Swiss Army Knife" watch on the Hexiwear platform. It is a bare-metal embedded application developed 100% in Ada 2012, from the lowest level device drivers all the way up to the application-specific code, for the Hexiwear's K64F microcontroller. I developed Ada drivers for Hexiwear-specific peripherals from scratch, as they were not supported by AdaCore's Ada drivers library. Also, since I wanted to use the GNAT GPL 2017 Ada compiler but the GNAT GPL distribution did not include a port of the Ada Runtime for the Hexiwear board, I also had to port the GNAT GPL 2017 Ada runtime to the Hexiwear. All this application-independent code can be leveraged by anyone interested in developing Ada applications for the Hexiwear wearable device.

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.

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.

Cross-referencing Ada with Libadalang

Libadalang has come a long way since the last time we blogged about it. In the past 6 months, we have been working tirelessly on name resolution, a pretty complicated topic in Ada, and it is finally ready enough that we feel ready to blog about it, and encourage people to try it out.

AdaCore at FOSDEM 2018

Every year, free and open source enthusiasts gather at Brussels (Belgium) for two days of FLOSS-related conferences. FOSDEM organizers setup several “developer rooms”, which are venues that host talks on specific topics. This year, the event will happen on the 3rd and 4th of February (Saturday and Sunday) and there is a room dedicated to the Ada programming language.

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.

Bitcoin blockchain in Ada: Lady Ada meets Satoshi Nakamoto

Bitcoin is getting a lot of press recently, but let's be honest, that's mostly because a single bitcoin worth 800 USD in January 2017 was worth almost 20,000 USD in December 2017. However, bitcoin and its underlying blockchain are beautiful technologies that are worth a closer look. Let’s take that look with our Ada hat on!

For All Properties, There Exists a Proof

With the recent addition of a Manual Proof capability in SPARK 18, it is worth looking at an example which cannot be proved by automatic provers, to see the options that are available for proving it with SPARK. We present three ways to complete a proof beyond what automatic provers can do: using an alternative automatic prover, proving interactively inside our GPS IDE, and using an alternative interactive prover.

Tokeneer Fully Verified with SPARK 2014

Tokeneer is a software for controlling physical access to a secure enclave by means of a fingerprint sensor. This software was created by Altran (Praxis at the time) in 2003 using the previous generation of SPARK language and tools, as part of a project commissioned by the NSA to investigate the rigorous development of critical software using formal methods. The project artefacts, including the source code, were released as open source in 2008. Tokeneer was widely recognized as a milestone in industrial formal verification. We recently transitioned this software to SPARK 2014, and it allowed us to go beyond what was possible with the previous SPARK technology. We have also shown how security vulnerabilities introduced in the code can be detected by formal verification.

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.

Ada on the micro:bit

Updated July 2018

Secure Software Architectures Based on Genode + SPARK

​SPARK user Alexander Senier presented recently at BOB Konferenz​ in Germany their use of SPARK for building secure mobile architectures. What's nice is that they build on the guarantees that SPARK provides at software level to create a secure software architecture based on the Genode operating system framework​. They present 3 interesting architectural designs that make it possible to build a trustworthy system out of untrustworthy building blocks. Almost as exciting as Alchemy's goal of transforming lead into gold! Here is the video of that presentation.

Two Days Dedicated to Sound Static Analysis for Security

​AdaCore has been working with CEA, Inria and NIST to organize a two-days event dedicated to sound static analysis techniques and tools, and how they are used to increase the security of software-based systems. The program gathers top-notch experts in the field, from industry, government agencies and research institutes, around the three themes of analysis of legacy code, use in new developments and accountable software quality. Here is why it is worth attending.

SPARK 2014 goes to Space!

David Lesens from Astrium was a member of the Hi-Lite project ("was" because the project is finished now, see the previous post), and has tried GNATprove - the formal verification tool for SPARK 2014 - on space vehicle software as an industrial case study of the project. And it turns out GNATprove performed pretty well!

Project Hi-Lite Wrap-up

After three years of hard work, we have reached last week the end of project Hi-Lite, whose goal was to simplify the use of formal methods. We're proud to publicize the results obtained, in particular the new version of SPARK and the associated tool GNATprove. Here's a summary of the wrap-up meeting.

SPARK 2014 Rationale: Contract Cases

Besides the usual expression of a subprogram contract as a pair of a precondition and a postcondition, SPARK 2014 provides a way to express such a contract by cases. A little history helps understanding how we came up with this new feature.

SPARK 2014 Rationale: Specification Functions

Specifying a program's behavior is seldom expressible in a satisfiable way without the capability of abstraction provided by function calls. Yet, specification functions must obey specific constraints like absence of side-effects and termination, that have led to different solutions in various specification languages. Here is what we did in SPARK 2014.

SPARK 2014 Flow Analysis

We have nearly finished implementing a central component of the SPARK 2014 analysis tools: the flow analysis engine; so this is a good time to introduce some of the analysis it will carry out.

MISRA-C 2012 vs SPARK 2014, the Subset Matching Game

The MISRA C subset of C defines around 150 rules that restrict C programs for critical software development. Of these, 27 rules are classified as undecidable, which means that few MISRA C checkers (if any) will help checking those hardest rules. Here is how SPARK 2014 can help checking similar rules in Ada programs.

SPARK 2014 Rationale: Pre-call and Pre-loop Values

Subprogram contracts are commonly presented as special assertions: the precondition is an assertion checked at subprogram entry, while the postcondition is an assertion checked at subprogram exit. A subtlety not covered by this simplified presentation is that postconditions are really two-state assertions: they assert properties over values at subprogram exit and values at subprogram entry. A special attribute Old is defined in Ada 2012 to support these special assertions. A special attribute Loop_Entry is defined in SPARK 2014 to support similar special assertions for loops.

SPARK 2014 Rationale: Loop Invariants

Formal verification tools like GNATprove rely on two main inputs from programmers: subprogram contracts (preconditions and postconditions) and loop invariants. While the first ones are easy to understand (based on the "contract" analogy, in which a subprogram and its caller have mutual obligations), the second ones are not so simple to grasp. This post presents loop invariants and the choices we made in SPARK 2014.

SPARK 2014 Rationale: Loop Variants

Loop variants are the little-known cousins of the loop invariants, used for proving termination of subprograms. Although they may not look very useful at first, they can prove effective as I show with a simple binary search example. And we came up with both an elegant syntax and a slick refinement for loop variants in SPARK 2014, compared to similar constructs in other languages.

SPARK 2014 Rationale: Mixing SPARK and Ada Code

The first step before any formal verification work with SPARK is to delimitate the part of the code that will be subject to formal verification within the overall Ada application. This post presents the solution we've come up with for SPARK 2014.

SPARK 2014 Rationale: Global State

Global variables are a common source of programming errors: they may fail to be initialized properly, they can be modified in unexpected ways, sequences of modifications may be illegal, etc. SPARK 2014 provides a way to define abstractly the global state of a unit, so that it can be referred to in subprogram specifications. The associated toolset checks correct access to global variables in the implementation.

GNATprove Tips and Tricks: Referring to Input in Contracts

In a previous post about pre-call values, I described how the Ada language rules implemented in the compiler prevent surprises when referring to input values in the postcondition, using the Old attribute. Unfortunately, these rules also make it difficult to express some complex postconditions that may be useful when doing formal verification. In this post, I describe how contract cases allow the expression of these complex contracts, while still detecting potential problems with uses of the Old attribute.

SPARK 2014 Rationale: Formal Containers

SPARK 2014 excludes data structures based on pointers. Instead, one can use the library of formal containers. They are variant of the Ada 2012 bounded containers, specifically designed and annotated to facilitate the proof of programs using them.

Rail, Space, Security: Three Case Studies for SPARK 2014

We will present three case studies using SPARK 2014 at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February 2014, in three different domains: rail, space and security. The lessons learned in those three case studies are particularly interesting. Here is the companion paper that we wrote.

Muen Separation Kernel Written in SPARK

The University of Applied Sciences Rapperswil in Switzerland has released last week an open-source separation kernel written in SPARK, which has been proved free from run-time errors. This project is part of the secure multilevel workstation project by Secunet, a German security company, which is using SPARK and Isabelle to create the next generation of secure workstations providing different levels of security to government employees and military personnel. I present why I think this project is worth following closely.

SPARK 2014 Rationale: Expressing Properties over Formal Containers

We saw in a previous post how formal containers can be used in SPARK code. In this post, I describe how to express properties over the content of these containers, using quantified expressions.

Case Study for System to Software Integrity Includes SPARK 2014

My colleague Matteo Bordin will present at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February a case study showing how formal verification with SPARK can be included in a larger process to show preservation of properties from the system level down to the software level. The case study is based on the Nose Gear challenge from the Workshop on Theorem Proving in Certification.

GNATprove Tips and Tricks: How to Write Loop Invariants

Having already presented in previous posts why loop invariants are necessary for formal verification of programs with loops, and what loop invariants are necessary for various loops, we detail here a methodology for how users can come up with the right loop invariants for their loops. This methodology in four steps allows users to progressively add the necessary information in their loop invariants, with the tool GNATprove providing the required feedback at each step on whether the information provided is sufficient or not.

SPARK 2014 Rationale: Data Dependencies

Programs often use a few global variables. Global variables make passing common information between different parts of a program easier. By reading the specification of a subprogram we are able to see all of the parameters that the subprogram uses and, in Ada, we also get to know whether they are read, written or both. However, no information regarding the use of global variables is revealed by reading the specifications. In order to monitor and enforce which global variables a subprogram is allowed to use, SPARK 2014 has introduced the Global aspect, which I describe in this post.

Information Flo(w): Array Initialization in Loops

SPARK only supported array initialization using aggregates, as array initialization in loops raised a false alarm in flow analysis. Read on to learn how the situation has been improved in SPARK 2014.

A Little Exercise With Strings

I recently looked at string manipulation functions in a library and tried to prove absence of run-time errors of one of them. Although the function and it's proof are quite simple in the end, the process of obtaining the correct code and the proof was interesting enough to write this blog post.

Studies of Contracts in Practice

Two recent research papers focus on how program contracts are used in practice in open source projects, in three languages that support contracts (Eiffel obviously, Java with JML contracts and C# with Code Contracts). I'm reporting what I found interesting (and less so) in these two studies.

Prove in Parallel with SPARK 2014

The article explains how we improved the performance of the SPARK 2014 toolset when multiple CPU cores are available for proof.

Contextual Analysis of Subprograms Without Contracts

We have implemented a new feature in GNATprove for analyzing local subprograms in the context of their calls. This makes it possible to benefit from the most precise analysis for local subprograms, without incurring the cost of adding contracts to these subprograms.

SPARK 2014 Rationale: Information Flow

In a previous blog post we described how aspect Global can be used to designate the specific global variables that a subprogram has to read and write. So, by reading the specification of a subprogram that has been annotated with aspect Global we can see exactly which variables, both local and global, are read and/or written each time the subprogram is called. Based purely on the Global aspect, this pretty much summarizes the full extent of our knowledge about the flow of information in a subprogram. To be more precise, at this point, we know NOTHING about the interplay between the inputs and outputs of the subprogram. For all we know, all outputs could be randomly generated and the inputs might not contribute in the calculation of any of the outputs. To improve this situation, SPARK 2014 uses aspect Depends to capture the dependencies between a subprogram's outputs and inputs. This blog post demonstrates through some examples how aspect Depends can be used to facilitate correct flow of information through a subprogram.

SPARKZumo Part 1: Ada and SPARK on Any Platform

So you want to use SPARK for your next microcontroller project? Great choice! All you need is an Ada 2012 ready compiler and the SPARK tools. But what happens when an Ada 2012 compiler isn’t available for your architecture?

Contracts of Functions in SPARK 2014

In SPARK 2014, we can write a function F and annotate it with a pre and a postcondition. In this post, we explain how the SPARK 2014 proof tool handles a call to such a function.

Use of SPARK in a Certification Context

Using SPARK or any other formal method in a certification requires that the applicant agrees with the certification authority on the verification objectives that this use of formal methods allows to reach, and how this is obtained and documented. In order to facilitate this process, the participants to the workshop on Theorem Proving in Certification have produced a draft set of guidelines, now publicly available.

Short Video Demo of SPARK 2014

New to SPARK? Want to "see" what's new in SPARK 2014? It's all in this 5 mn video demo!

Manual Proof with Ghost Code in SPARK 2014

Guiding automatic solvers by adding intermediate assertions is a commonly used technique. We can go further in this direction, by adding complete pieces of code doing nothing, generally called ghost code, to guide the automated reasoning. This is an advanced feature, for people willing to manually guide proofs. Still, it is all in SPARK 2014 and thus does not require the user to learn a new language. We explain here how we can achieve inductive proofs on a permutation function.

External Axiomatizations: a Trip Into SPARK’s Internals

There are cases expressing all the specification of a package in SPARK is either impossible (for example if you need to link them to elements of the mathematical world, like trigonometry functions), cumbersome (especially if they require concepts that cannot easily be described using contracts, like transitivity, counting, summation...), or simply inefficient, for big and complex data structures like containers for example. In these cases, a user can provide directly a manually written Why3 translation for an Ada package using a feature named external axiomatizations. Coming up with this manual translation requires both a knowledge of the WhyML language and a minimal understanding of GNATprove's mechanisms and is therefore reserved to advanced users.

Explicit Assumptions in SPARK 2014

In this article, we provide a short introduction to our paper at the Test and Proof 2014 conference in York, UK.

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.

Using SPARK to Prove AoRTE in Robot Navigation Software

Correctness of robot software is a challenge. Just proving the absence of run-time errors (AoRTE) in robot software is a challenge big enough that even NASA has not solved it. Researchers have used SPARK to do precisely that for 3 well-known robot navigation algorithms. Their results will be presented at the major robotics conference IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2014) this coming September.

SPARK 15: Errors, Warnings and Checks

The messages issued by the SPARK toolset will change a bit in the next version of both SPARK Pro and SPARK GPL. This post explains the change and the motivation behind it.

Using Coq to Verify SPARK 2014 Code

In the first release of SPARK 2014, GNATprove only provided support for automatic provers, in particular Alt-Ergo. Automatic provers are very handy when it comes to perform a big numberof simple proof. But they can fail to prove valid formulas when the proof involves some advanced reasoning. As mentioned in a previous post, one check left unproved might invalidate assumptions on which are based the proofs of multiple other checks. This is a case where manual proof may be useful for SPARK 2014 users. The development version of GNATprove now supports Coq to perform manual proof.

SPARK 2014 Rationale: Ghost Code

A common situation when proving properties about a program is that you end up writing additional code whose only purpose is to help proving the original program. If you're careful or lucky enough, the additional code you write will not impact the program being verified, and it will be removed during compilation, so that it does not inflate binary size or waste execution cycles. SPARK provides a way to get these benefits automatically, by marking the corresponding code as ghost code, using the new Ghost aspect.

SPARK 2014 Rationale: Object Oriented Programming

Object Oriented Programming is known for making it particularly difficult to analyze programs, because the subprograms called are not always known statically. The standard for civil avionics certification has recognized this specific problem, and defines a specific verification objective called Local Type Consistency that should be met with one of three strategies. SPARK allows using one of these strategies, by defining the behavior of an overridden subprogram using a special class-wide contract and checking that the behavior of the overriding subprogram is a suitable substitution, following the Liskov Substitution Principle.

SPARK 2014 Rationale: Functional Update

While attribute Old allows expressing inside postconditions the value of objects at subprogram entry, this is in general not enough to conveniently express how record and array objects are modified by a procedure. A special attribute Update is defined in SPARK to make it easy to express such properties.

GNATprove Tips and Tricks: Keeping Justifications Up-To-Date

GNATprove supports the suppression of warnings and justification of check messages with pragmas inserted in the source code. But these justifications may become obsolete across time. To help with that, GNATprove now issues a warning on useless justifications.

GNATprove Tips and Tricks: Catching Mistakes in Contracts

Contracts may be quite complex, as complex as code in fact, so it is not surprising that they contain errors sometimes. GNATprove can help by pinpointing suspicious constructs that, although legal, do not make much sense. These constructs are likely to be caused by mistakes made by the programmer when writing the contract. In this post, I show examples of incorrect constructs that are signaled by GNATprove.

GNATprove Tips and Tricks: Bitwise Operations

The ProofInUse joint laboratory is currently improving the way SPARK deals with modular types and bitwise operators. Until now the SPARK tool was trying its best to translate those into equivalent operations on integers. It is now using native theory of smt-solvers when available resulting in much better support, and guaranteeing state of the art handling of bitwise operations. We present some examples in this post.

GNATprove Tips and Tricks: Minimizing Rework

As automatic proof is time consuming, it is important that rework following a change in source code is minimized. GNATprove uses a combination of techniques to ensure that, both for a single user, and when working in a team.

A quick glimpse at the translation of Ada integer types in GNATprove

In SPARK, as in most programming languages, there are a bunch of bounded integer types. On the other hand, Why3 only has mathematical integers and a library for bitvectors. Since bitwise operations can only be done on modular types in Ada, we currently translate arithmetic operations on signed integer types as operations on mathematical integers and arithmetic operations on modular types as operation on bitvectors. The only remaining question now is, how do we encode specific bounds of the Ada types into our Why3 translation ? In this post, I will present three different ways we tried to do this and explain which one we currently use and why.

How Our Compiler Learnt From Our Analyzers

Program analyzers interpret the source code of a program to compute some information. Hopefully, the way they interpret the program is consistent with the way that the compiler interprets it to generate an executable, or the information computed is irrelevant, possibly misleading. For example, if the analyzer says that there are no possible run-time errors in a program, and you rely on this information to compile with dynamic checking off, it is crucial that no run-time error could occur as a result of a divergence of opinion between the analyzer and the compiler on the meaning of an instruction. We recently discovered such an inconsistency in how our compiler and analyzers dealt with floating-point exponentiation, which lead to a change in how GNAT now compile these operations.

SPARKSkein: From tour-de-force to run-of-the-mill Formal Verification

In 2010, Rod Chapman released an implementation in SPARK of the Skein cryptographic hash algorithm, and he proved that this implementation was free of run-time errors. That was a substantial effort with the previous version of the SPARK technology. We have recently translated the code of SPARKSkein from SPARK 2005 to SPARK 2014, and used GNATprove to prove absence of run-time errors in the translated program. The difference between the two technologies is striking. The heroic effort that Rod put in the formal verification of the initial version of SPARKSkein could now be duplicated with modest effort and modest knowledge of the technology, thanks to the much greater proof automation that the SPARK 2014 technology provides, as well as various features that lower the need to provide supporting specifications, most notably contracts on internal subprograms and loop invariants.

SPARK 2014 Rationale: Type Predicates

Preconditions and postconditions define a very strong mechanism for specifying invariant properties over the program's control. What about similar properties for the program's data? It turns out Ada 2012 defined such a construct, type predicates, which was not supported in SPARK until now. And now it is.

The Eight Reasons For Using SPARK

Based on our many years of experience with our customers using SPARK in their projects, we have come up with a list of eight objectives that are most commonly targeted when using SPARK. Most projects only target a few of them, but in theory one could try to achieve all of them with SPARK on a project. This list may be useful for those who want to assess if the SPARK technology can be of benefit in their context, and to existing SPARK users to compare their existing practice with what others do.

SPARK 2014 Rationale: Variables That Are Constant

The SPARK tools now support yet another feature that allows users to better specify the intended behavior of their programs. This new feature enables users to declare that specific variables can only be updated during the elaboration of their enclosing package. Read on if you want to know more...

GNATprove Tips and Tricks: User Profiles

One of the most difficult tasks when using proof techniques is to interact with provers, in particular to progressively increase proof power until everything that should be proved is proved. Until the last release, increasing the proof power meant operating on three separate switches. There is now a simpler solution based on a new switch --level, together with a simpler proof panel in GPS for new users.

SPARK 16: Generating Counterexamples for Failed Proofs

While the analysis of failed proofs is one of the most challenging aspects of formal verification, it would be much easier if a tool would automatically find values of variables showing why a proof fails. SPARK Pro 16, to be released in 2016, is going to introduce such a feature. If a proof fails, it attempts to generate a counterexample exhibiting the problem. This post introduces this new feature, developed in the scope of the ProofInUse laboratory.

SPARK 2016 Supports Ravenscar!

The new big feature of the SPARK 2016 release is the support of the Ravenscar profile. Users can now use protected objects and tasks to write concurrent code. On uniprocessor computers the toolset can ensure that no deadlocks or data races will occur and that no tasks will terminate. Read this blog post to learn more and see the new feature in practice.

SPARK 2014 Rationale: Support for Ravenscar

As presented in a recent post by Pavlos, the upcoming release of SPARK Pro will support concurrency features of Ada, with the restrictions defined in the Ravenscar profile of Ada. This profile restricts concurrency so that concurrent programs are deterministic and schedulable. SPARK analysis makes it possible to prove that shared data is protected against data races, that deadlocks cannot occur and that no other run-time errors related to concurrency can be encountered when running the program. In this post, I revisit the example given by Pavlos to show SPARK features and GNATprove analysis in action.

GNATprove Tips and Tricks: What’s Provable for Real?

SPARK supports two ways of encoding reals in a program: the usual floating-point reals, following the standard IEEE 754, and the lesser known fixed-point reals, called this way because their precision is fixed (contrary to floating-points whose precision varies with the magnitude of the encoded number). This support is limited in some ways when it comes to proving properties of computations on real numbers, and these limitations depend strongly in the encoding chosen. In this post, I show the results of applying GNATprove on simple programs using either floating-point or fixed-point reals, to explain these differences.

AdaCore Tech Days Prez on SPARK

Hristian Kirtchev, who leads the developments of the GNAT compiler frontend, gave a very clear presentation of SPARK at the last AdaCore Tech Days in Boston. This was recorded, here is the video.

SPARK Prez at New Conference on Railway Systems

RSSR is a new conference focused on the development and verification of railway systems. We will present there how SPARK can be used to write abstract software specifications, whose refinement in terms of concrete implementation can be proved automatically using SPARK tools.

Did SPARK 2014 Rethink Formal Methods?

David Parnas is a well-known researcher in formal methods, who famously contributed to the analysis of the shut-down software for the Darlington nuclear power plant and designed the specification method known as Parnas tables and the development method called Software Cost Reduction. In 2010, the magazine CACM asked him to identify what was preventing more widespread adoption of formal methods in industry, and in this article on Really Rethinking Formal Methods he listed 17 areas that needed rethinking. The same year, we started a project to recreate SPARK with new ideas and new technology, which lead to SPARK 2014 as it is today. Parnas's article influenced some critical design decisions. Six years later, it's interesting to see how the choices we made in SPARK 2014 address (or not) Parnas's concerns.

SPARKSMT - An SMTLIB Processing Tool Written in SPARK - Part I

Today I will write the first article in a short series about the development of an SMTLIB processing tool in SPARK. Instead of focusing on features, I intend to focus on the how I have proved absence of run-time errors in the name table and lexer. I had two objectives: show absence of run-time errors, and do not write useless defensive code. Today's blog will be about the name table, a data structure found in many compilers that can map strings to a unique integer and back. The next blog post will talk about the lexical analyzer.

Quantifying over Elements of a Container

Containers holding several items of the same type such as arrays, lists, or sets are a common occurrence in computer programs. Stating a property over such containers often involves quantifying over the elements they contain. The way quantified formulas over containers are translated for proof can be tuned in GNATprove using a specific annotation.

GNATprove Tips and Tricks: Using the Lemma Library

A well-know result of computing theory is that the theory of arithmetic is undecidable. This has practical consequences in automatic proof of programs which manipulate numbers. The provers that we use in SPARK have a good support for addition and subtraction, but much weaker support for multiplication and division. This means that as soon as the program has multiplications and divisions, it is likely that some checks won't be proved automatically. Until recently, the only way forward was either to complete the proof using an interactive prover (like Coq or Isabelle/HOL) or to justify manually the message about an unproved check. There is now a better way to prove automatically such checks, using the recent SPARK lemma library.

Research Corner - Proving Security of Binary Programs with SPARK

Researchers from Dependable Computing and Zephyr Software LLC have presented at the latest NASA Formal Methods conference last week their work on proving security of binary programs. In this work, they use SPARK as intermediate language and GNATprove as proof tool, which is an atypical and interesting use of the SPARK technology.

Research Corner - SPARK 2014 vs Frama-C vs Why3

Ready for a bloody comparison between technologies underlying the tools for SPARK 2014 vs Frama-C vs Why3? Nothing like that in that article we wrote with developers of the Why3 and Frama-C toolsets. In fact, it's a bloody good comparison really, that emphasizes the differences and benefits in each technology.

Automatic Generation of Frame Conditions for Record Components

Formal verification tools like GNATprove rely on the user to provide loop invariants to describe the actions performed inside loops. Though the preservation of variables which are not modified in the loop need not be mentioned in the invariant, it is in general necessary to state explicitly the preservation of unmodified object parts, such as record fields or array elements. These preservation properties form the loop’s frame condition. As it may seem obvious to the user, the frame condition is unfortunately often forgotten when writing a loop invariant, leading to unprovable checks. To alleviate this problem, the GNATprove tool now generates automatically frame conditions for preserved record components. In this post, we describe this new feature on an example.

The Most Obscure Arithmetic Run-Time Error Contest

Something that many developers do not realize is the number of run-time checks that occur in innocent looking arithmetic expressions. Of course, everyone knows about overflow checks and range checks (although many people confuse them) and division by zero. After all, these are typical errors that do show up in programs, so programmers are aware that they should keep an eye on these. Or do they?

SPARK 2014 Rationale: Support for Type Invariants

Type invariants are used to model properties that should always hold for users of a data type but can be broken inside the data type implementation. Type invariant are part of Ada 2012 but were not supported in SPARK until SPARK Pro 17.

Verifying Tasking in Extended, Relaxed Style

Tasking was one of the big features introduced in the previous release of SPARK 2014. However, GNATprove only supported tasking-related constructs allowed by the Ravenscar profile. Now it also supports the more relaxed GNAT Extended Ravenscar profile.

Research Corner - SPARK on Lunar IceCube Micro Satellite

Researchers Carl Brandon and Peter Chapin recently presented during conference HILT 2016 their ongoing work to build a micro satellite called Lunar IceCube that will map water vapor and ice on the moon. In their paper, they explain how the use of proof with SPARK is going to help them get perfect software in the time and budget available.

GNATprove Tips and Tricks: What’s Provable for Real Now?

One year ago, we presented on this blog what was provable about fixed-point and floating-point computations (the two forms of real types in SPARK). Since then, we have integrated static analysis in SPARK, and modified completely the way floating-point numbers are seen by SMT provers. Both of these features lead to dramatic changes in provability for code doing fixed-point and floating-point computations.

Automatic Generation of Frame Conditions for Array Components

One of the most important challenges for SPARK users is to come up with adequate contracts and annotations, allowing GNATprove to verify the expected properties in a modular way. Among the annotations mandated by the SPARK toolset, the hardest to come up with are probably loop invariants. A previous post explains how GNATprove can automatically infer loop invariants for preservation of unmodified record components, and so, even if the record is itself nested inside a record or an array. Recently, this generation was improved to also support the simplest cases of partial array updates. We describe in this post in which cases GNATprove can, or cannot, infer loop invariants for preservation of unmodified array components.

GNATprove Tips and Tricks: a Lemma for Sorted Arrays

We report on the creation of the first lemma of a new lemma library on arrays: a lemma on transitivity of the order in arrays.

SPARK Cheat Sheets (en & jp)

The SPARK cheat sheet usually distributed in trainings has recently been translated to Japanese. Here they are, both in English and in Japanese. My modest Xmas present.

SPARK and CodePeer, a Good Match!

It turns out that the CodePeer engine can be used as a powerful prover for SPARK programs. This feature will be available in the next version of SPARK Pro, make sure you try it out!

Hash it and Cache it

A new feature of SPARK2014 allows to use a memcached server to share proof results between runs of the SPARK tools and even between developers on different machines. Check out this post to see the details.

Proving Tetris With SPARK in 15 Minutes

I gave last week a 15-minutes presentation at FOSDEM conference of how you can prove interesting properties of Tetris with SPARK. Here is the recording.

Rod Chapman on Software Security

Rod Chapman gave an impactful presentation at Bristech conference last year. His subject: programming Satan's computer! His way of pointing out how difficult it is to produce secure software. Of course, it would not be Rod Chapman if he did not have also a few hints at how they have done it at Altran UK over the years. And SPARK is central to this solution, although it does not get mentioned explicitly in the talk! (although Rod lifts the cover in answering a question at the end)

Research Corner - Auto-active Verification in SPARK

GNATprove performs auto-active verification, that is, verification is done automatically, but usually requires annotations by the user to succeed. In SPARK, annotations are most often given in the form of contracts (pre and postconditions). But some language features, in particular ghost code, allow proof guidance to be much more involved. In a paper we are presenting at NASA Formal Methods symposium 2017, we describe how an imperative red black tree implementation in SPARK was verified using intensive auto-active verification.

Two Projects to Compute Stats on Analysis Results

Two projects by Daniel King and Martin Becker facilitate the analysis of GNATprove results by exporting the results (either from the log or from the generated JSON files) to either Excel or JSON/text.

GNATprove Tips and Tricks: Proving the Ghost Common Divisor (GCD)

Euclid's algorithm for computing the greatest common divisor of two numbers is one of the first ones we learn in school, and also one of the first algorithms that humans devised. So it's quite appealing to try to prove it with an automatic proving toolset like SPARK. It turns out that proving it automatically is not so easy, just like understanding why it works is not so easy. In this post, I am using ghost code to prove correct implementations of the GCD, starting from a naive linear search algorithm and ending with Euclid's algorithm.

VerifyThis Challenge in SPARK

This year again, the VerifyThis competition took place as part of ETAPS conferences. This is the occasion for builders and users of formal program verification platforms to use their favorite tools on common challenges. The first challenge this year was a good fit for SPARK, as it revolves around proving properties of an imperative sorting procedure. In this post, I am using this challenge to show how one can reach different levels of software assurance with SPARK.

New Guidance for Adoption of SPARK

While SPARK has been used for years in companies like Altran UK, companies without the same know-how may find it intimidating to get started on formal program verification. To help with that process, AdaCore has collaborated with Thales throughout the year 2016 to produce a 70-pages detailed guidance document for the adoption of SPARK. These guidelines are based on five levels of assurance that can be achieved on software, in increasing order of costs and benefits: Stone level (valid SPARK), Bronze level (initialization and correct data flow), Silver level (absence of run-time errors), Gold level (proof of key properties) and Platinum level (full functional correctness). These levels, and their mapping to the Development Assurance Levels (DAL) and Safety Integrity Levels (SIL) used in certification standards, were presented at the recent High Confidence Software and Systems conference.

Frama-C & SPARK Day Slides and Highlights

The Frama-C & SPARK Day this week was a very successful event gathering the people interested in formal program verification for C programs (with Frama-C) and for Ada programs (with SPARK). Here is a summary of what was interesting for SPARK users. We also point to the slides of the presentations.

Research Corner - Floating-Point Computations in SPARK

It is notoriously hard to prove properties of floating-point computations, including the simpler bounding properties that state safe bounds on the values taken by entities in the program. Thanks to the recent changes in SPARK 17, users can now benefit from much better provability for these programs, by combining the capabilities of different provers. For the harder cases, this requires using ghost code to state intermediate assertions proved by one of the provers, to be used by others. This work is described in an article which was accepted at VSTTE 2017 conference.

Research Corner - FLOSS Glider Software in SPARK

Two years ago, we redeveloped the code of a small quadcopter called Crazyflie in SPARK, as a proof-of-concept to show it was possible to prove absence of run-time errors (no buffer overflows, not division by zero, etc.) on such code. The researchers Martin Becker and Emanuel Regnath have raised the bar by developing the code for the autopilot of a small glider in SPARK in three months only. Their paper and slides are available, and they have released their code as FLOSS for others to use/modify/enhance!

Applied Formal Logic: Searching in Strings

A friend pointed me to recent posts by Tommy M. McGuire, in which he describes how Frama-C can be used to functionally prove a brute force version of string search, and to find a previously unknown bug in a faster version of string search called quick search. Frama-C and SPARK share similar history, techniques and goals. So it was tempting to redo the same proofs on equivalent code in SPARK, and completing them with a functional proof of the fixed version of quick search. This is what I'll present in this post.

Research Corner - Focused Certification of SPARK in Coq

The SPARK toolset aims at giving guarantees to its users about the properties of the software analyzed, be it absence of runtime errors or more complex properties. But the SPARK toolset being itself a complex tool, it is not free of errors. To get confidence in its results, we have worked with academic partners to establish mathematical evidence of the correctness of a critical part of the SPARK toolset. The part on which we focused is the tagging of nodes requiring run-time checks by the frontend of the SPARK technology. This work has been accepted at SEFM 2017 conference.

Proving Loops Without Loop Invariants

For all the power that comes with proof technology, one sometimes has to pay the price of writing a loop invariant. Along the years, we've strived to facilitate writing loop invariants by improving the documentation and the technology in different ways, but writing loops invariants remains difficult sometimes, in particular for beginners. To completely remove the need for loop invariants in simple cases, we have implemented loop unrolling in GNATprove. It turns out it is quite powerful when applicable.

New SPARK Cheat Sheet

Our good friend Martin Becker has produced a new cheat sheet for SPARK, that you may find useful for a quick reminder on syntax that you have not used for some time.

SPARK Tutorial at FDL Conference

Researcher Martin Becker is giving a SPARK tutorial next week at FDL conference. This post gives a link to his tutorial material (cookbook and slides) which I found extremely interesting.

Prove in the Cloud

We have put together a byte (8 bits) of examples of SPARK code on a server in the cloud. The benefit with this webpage is that anyone can now experiment live with SPARK without installing first the toolset. Something particularly interesting for academics is that all the code for this widget is open source. So you can setup your own proof server for hands-on sessions, with your own exercises, in a matter of minutes.

SPARK 2014 Rationale: Verifying Properties over Formal Containers

We saw in a previous post how we could express complex properties over formal containers using quantified expressions. In this post, I present how these properties can be verified by the proof tool called GNATprove.

Getting Rid of Rust with Ada

There are a lot of DIY CNC projects out there (router, laser, 3D printer, egg drawing, etc.), but I never saw a DIY CNC sandblaster. So I decided to make my own.

A Modern Syntax for Ada

One of the most criticized aspect of the Ada language throughout the years has been its outdated syntax. Fortunately, AdaCore decided to tackle this issue by implementing a new, modern, syntax for Ada.

PolyORB now lives on Github

PolyORB, AdaCore's versatile distribution middleware, now lives on Github. Its new home is https://github.com/AdaCore/polyorb

Taking on a Challenge in SPARK

Last week, the programmer Hillel posted a challenge (the link points to a partial postmortem of the provided solutions) on Twitter for someone to prove a correct implementation of three small programming problems: Leftpad, Unique, and Fulcrum.

How Ada and SPARK Can Increase the Security of Your Software

There is a long-standing debate about which phase in the Software Development Life Cycle causes the most bugs: is it the specification phase or the coding phase? A recent study by NIST shows that, in the software industry at large, coding bugs are causing the majority of security issues. Choosing a safer language like Ada or SPARK is a critical component for reducing these vulnerabilities that result from simple mistakes. In a new freely available booklet, we explain how these languages and the associated toolsets can be used to increase the security of software.

GNAT Community 2018 is here!

Calling all members of the Ada and SPARK community, we are pleased to announce that GNAT Community 2018 is here! adacore.com/download

Security Agency Uses SPARK for Secure USB Key

​ANSSI, the French national security agency, has published the results of their work since 2014 on designing and implementing an open-hardware & open-source USB key that provides defense-in-depth against vulnerabilities on the USB hardware, architecture, protocol and software stack. In this project called WooKey, Ada and SPARK are key components for the security of the platform. This is a very compelling demontration of both the usability and the power of safe languages and formal verification to develop secure systems.

Learn.adacore.com is here

We are very proud to announce the availability of our new Ada and SPARK learning platform learn.adacore.com, which will replace AdaCoreU(niversity) e-learning platform. Learn all about it in this blog post.

AdaCore major sponsor at HIS 2018

We are happy to announce that, AdaCore, alongside Altran and Jaguar Land Rover will be major sponsors of the fifth edition of the renowned High Integrity Software Conference on the 6th November in Bristol!

Ada on FPGAs with PicoRV32

When I bought the TinyFPGA-BX board, I thought it would be an opportunity to play a little bit with FPGA, learn some Verilog or VHDL. But when I discovered that it was possible to have a RISC-V CPU on it, I knew I had to run Ada code on it.

Train control using Ada on a Raspberry Pi

I was looking for a topic for my master thesis in embedded systems engineering when one of my advisor proposed the idea of programming a control system for autonomous trains in Ada. Since I am fascinated by the idea of autonomous vehicles I agreed immediately without knowing Ada.

Public Ada Training Paris, France Dec 3 - 7, 2018

This course is geared to software professionals looking for a practical introduction to the Ada language with a focus on embedded systems, including real-time features as well as critical features introduced in Ada 2012. By attending this course you will understand and know how to use Ada for both sequential and concurrent applications, through a combination of live lectures from AdaCore's expert instructors and hands-on workshops using AdaCore's latest GNAT technology. AdaCore will provide an Ada 2012 tool-chain and ARM-based target boards for embedded workshops. No previous experience with Ada is required.

It's time to Make with Ada!

The challengeAre you ready to develop a project to the highest levels of safety, security and reliability? If so, Make with Ada is the challenge for you! We’re calling on embedded developers across the globe to build cool embedded applications using the Ada and SPARK programming languages and are offering over $8000 in total prizes. In addition, eligible students will compete for a reward of an Analog Discovery 2 Pro Bundle worth $299.99!

​Amazon Relies on Formal Methods for the Security of AWS

Byron Cook, who founded and leads the Automated Reasoning Group at Amazon Web Services (AWS) Security, gave a powerful talk at the Federated Logic Conference in July about how Amazon uses formal methods for ensuring the security of parts of AWS infrastructure. In the past four years, this group of 20+ has progressively hired well-known formal methods experts to face the growing demand inside AWS to develop tools based on formal verification for reasoning about cloud security. What is unique so far is the level of investment at AWS in formal verification as a means to radically eliminate some security problems, both for them and for their customers. This is certainly an approach we're eager to support with our own investment in the SPARK technology​.

Proving Memory Operations - A SPARK Journey

The promise behind the SPARK language is the ability to formally demonstrate properties in your code regardless of the input values that are supplied - as long as those values satisfy specified constraints. As such, this is quite different from static analysis tools such as our CodePeer or the typical offering available for e.g. the C language, which trade completeness for efficiency in the name of pragmatism. Indeed, the problem they’re trying to solve - finding bugs in existing applications - makes it impossible to be complete. Or, if completeness is achieved, then it is at the cost of massive amount of uncertainties (“false alarms”). SPARK takes a different approach. It requires the programmer to stay within the boundaries of a (relatively large) Ada language subset and to annotate the source code with additional information - at the benefit of being able to be complete (or sound) in the verification of certain properties, and without inundating the programmer with false alarms.

NVIDIA is joining the Ada and SPARK adopter wave

Over the past several years, a great number of public announcements have been made about companies that are either studying or adopting the Ada and SPARK programming languages. Noteworthy examples include Dolby, Denso, LASP and Real Heart, as well as the French Security Agency.

How Do We Use CodePeer at AdaCore

A question that our users sometimes ask us is "do you use CodePeer at AdaCore and if so, how?". The answer is yes! and this blog post will hopefully give you some insights into how we are doing it for our own needs.

The Power of Technology Integration and Open Source

Part of our core expertise at AdaCore is to integrate multiple technologies as smoothly as possible and make it a product. This started at the very beginning of our company by integrating a code generator (GCC) with an Ada front-end (GNAT) which was then followed by integrating a debugger engine (GDB) and led to today's rich GNAT Pro offering.

Combining GNAT with LLVM

Presenting the GNAT LLVM projectAt AdaCore labs, we have been working for some time now on combining the GNAT Ada front-end with a different code generator than GCC.

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.

AdaFractal Part 2: Fixed Point and Floating Point Math Performance and Parallelization

In Part 1 of this blog post I discussed why I chose to implement this application using the Ada Web Server to serve the computed fractal to a web browser. In this part I will discuss a bit more about the backend of the application, the Ada part.

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.

A Readable Introduction to Both MISRA C and SPARK Ada

MISRA C is the most widely known coding standard restricting the use of the C programming language for critical software. For good reasons. For one, its focus is entirely on avoiding error-prone programming features of the C programming language rather than on enforcing a particular programming style. In addition, a large majority of rules it defines are checkable automatically (116 rules out of the total 159 guidelines), and many tools are available to enforce those. As a coding standard, MISRA C even goes out of its way to define a consistent sub-language of C, with its own typing rules (called the "essential type model" in MISRA C) to make up for the lack of strong typing in C.

Ten Years of Using SPARK to Build CubeSat Nano Satellites With Students

My colleague, Carl Brandon, and I have been running the CubeSat Laboratory at Vermont Technical College (VTC) for over ten years. During that time we have worked with nearly two dozen students on building and programming CubeSat nano satellites. Because of their general inexperience, and because of the high student turnover rate that is natural in an educational setting, our development process is often far from ideal. Here SPARK has been extremely valuable to us. What we lack in rigor of the development process we make up for in the rigor of the SPARK language and tools. In November 2013 we launched a low Earth orbiting CubeSat. The launch vehicle contained 13 other university built CubeSats. Most were never heard from. One worked for a few months. Ours worked for two years until it reentered Earth's atmosphere as planned in November 2015.

Public Ada Training Paris June 3-7, 2019

This course is geared to software professionals looking for a practical introduction to the Ada language with a focus on embedded systems, including real-time features as well as critical features introduced in Ada 2012. By attending this course you will understand and know how to use Ada for both sequential and concurrent applications, through a combination of live lectures from AdaCore's expert instructors and hands-on workshops using AdaCore's latest GNAT technology. AdaCore will provide an Ada 2012 tool-chain and ARM-based target boards for embedded workshops. No previous experience with Ada is required.

Using SPARK to prove 255-bit Integer Arithmetic from Curve25519

In 2014, Adam Langley, a well-known cryptographer from Google, wrote a post on his personal blog, in which he tried to prove functions from curve25519-donna, one of his projects, using various verification tools: SPARK, Frama-C, Isabelle... He describes this attempt as "disappointing", because he could not manage to prove "simple" things, like absence of runtime errors. I will show in this blogpost that today, it is possible to prove what he wanted to prove, and even more.

Winning DTU RoboCup with Ada and SPARK

The Danish Technical University has a yearly RoboCup where autonomous vehicles solve a number of challenges. We participated with RoadRunner, a 3D printed robot with wheel suspension, based on the BeagleBone Blue ARM-based board and the Pixy 1 camera with custom firmware enabling real-time line detection. Code is written in Ada and formally proved correct with SPARK at Silver level.

Using Pointers in SPARK

In this blog post, I will present one of the most interesting additions to the community 2019 version of SPARK: pointer support. One of the core assumption in SPARK has always been the absence of aliasing, so adding pointers without breaking this assumption was quite a challenge. I will explain how this was achieved using an ownership model for pointers (like is done in Rust) through small examples.

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.

GNAT Community 2019 is here!

We are pleased to announce that GNAT Community 2019 has been released! See https://www.adacore.com/download.

RFCs for Ada and SPARK evolution now on GitHub

Interested in participating in the evolution of the Ada or SPARK languages? We have something for you.

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.

Proving a simple program doing I/O ... with SPARK

The functionality of many security-critical programs is directly related to Input/Output (I/O). This includes command-line utilities such as gzip, which might process untrusted data downloaded from the internet, but also any servers that are directly connected to the internet, such as webservers, DNS servers and so on. In this blog post we show an approach that deals with error handling and reasoning about content, and demonstrate the approach using the cat command line utility.

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.

First Ada Virtual Conference organized by and for the Ada community

The Ada Community has gathered recently around a new exciting initiative - an Ada Virtual Conference, to present Ada-related topics in a 100% remote event. The first such conference took place on August, 10th 2019, around the topic of the new features in Ada 202x. Here is what was presented.

The Make with Ada competition is back!

AdaCore’s fourth annual Make with Ada competition launched this week with over $8K in cash and prizes to be awarded for the most innovative embedded systems projects developed using Ada and/or SPARK.

Learning SPARK via Conway's Game of Life

How I learned to write SPARK-provable code using Conway's Game Of Life

Pointer Based Data-Structures in SPARK

As seen in a previous post, it is possible to use pointers (or access types) in SPARK provided the program abides by a strict memory ownership policy designed to prevent aliasing. We will show in this post how to define pointer-based data-structures in SPARK and how to traverse them without breaking the ownership policy.

RecordFlux: From Message Specifications to SPARK Code

Handling binary data is hard. Errors in parsers routinely lead to critical security vulnerabilities. In this post we show how the RecordFlux toolset eases the creation of formally verified binary parsers in SPARK.

An Expedition into Libadalang

I’ve been telling Ada developers for a while now that Libadalang will open up the possibility of more-easily writing Ada source code analysis tools.  (You can read more about Libadalang here and here and can also access the project on Github.)

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).

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.

Ada on a Feather

I was quite happy to see AdaFruit release their first Feather format board including a micro-controller with plenty of Ada support, the STM32F4. I bought a board right away and implemented some support code for it.

Witnessing the Emergence of a New Ada Era

For nearly four decades the Ada language (in all versions of the standard) has been helping developers meet the most stringent reliability, safety and security requirements in the embedded market. As such, Ada has become an entrenched player in its historic A&D niche, where its technical advantages are recognized and well understood. Ada has also seen usage in other domains (such as medical and transportation) but its penetration has progressed at a somewhat slower pace. In these other markets Ada stands in particular contrast with the C language, which, although suffering from extremely well known and documented flaws, remains a strong and seldom questioned default choice. Or at least, when it’s not the choice, C is still the starting point (a gateway drug?) for alternatives such as C++ or Java, which in the end still lack the software engineering benefits that Ada embodies..

Using GNAT-LLVM to target Ada to WebAssembly

The GNAT-LLVM project provides an opportunity to port Ada to new platforms, one of which is WebAssembly. We conducted an experiment to evaluate the porting of Ada and the development of bindings to use Web API provided by the browser directly from Ada applications.

A Further Expedition into Libadalang: Save Time with Libadalang.Helpers.App

Martyn’s recent blog post showed small programs based on Libadalang to find uses of access types in Ada sources. Albeit short, these programs need to take care of all the tedious logistics around processing Ada sources: find the files to work on, create a Libadalang analysis context, use it to read the source files, etc. Besides, they are not very convenient to run:

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.

Making an RC Car with Ada and SPARK

As a demonstration for the use of Ada and SPARK in very small embedded targets, I created a remote-controlled (RC) car using Lego NXT Mindstorms motors and sensors but without using the Lego computer or Lego software. I used an ARM Cortex System-on-Chip board for the computer, and all the code -- the control program, the device drivers, everything -- is written in Ada. Over time, I’ve upgraded some of the code to be in SPARK. This blog post describes the hardware, the software, the SPARK upgrades, and the repositories that are used and created for this purpose.

Proving properties of constant-time crypto code in SPARKNaCl

Over the last few months, I developed a SPARK version of the TweetNaCl cryptographic library. This was made public on GitHub in February 2020, under the 2-clause BSD licence. This blog entry goes into a bit more technical detail on one particular aspect of the project: the challenge of re-writing and verifying "constant time" algorithms using SPARK.

Android application with Ada and WebAssembly

Having previously shown how to create a Web application in Ada, it's not so difficult to create an Android application in Ada. Perhaps the simplest way is to install Android Studio. Then just create a new project and choose "Empty Activity". Open the layout, delete TextView and put WebView instead.

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.

Time travel debugging in GNAT Studio with GDB and RR

Learn how to use GDB and RR's advanced time traveling features in GNAT Studio.

An Introduction to Contract-Based Programming in Ada

One of the most powerful features of Ada 2012* is the ability to specify contracts on your code. Contracts describe conditions that must be satisfied upon entry (preconditions) and upon exit (postconditions) of your subprogram. Preconditions describe the context in which the subprogram must be called, and postconditions describe conditions that will be adhered to by the subprogram’s implementation. If you think about it, contracts are a natural evolution of Ada’s core design principle. To encourage developers to be as explicit as possible with their expressions, putting both the compiler/toolchain and other developers in the best position to help them develop better code.

From Ada to Platinum SPARK: A Case Study for Reusable Bounded Stacks

This blog entry describes the transformation of an Ada stack ADT into a completely proven SPARK implementation that relies on static verification instead of run-time enforcement of the abstraction’s semantics. We will prove that there are no reads of unassigned variables, no array indexing errors, no range errors, no numeric overflow errors, no attempts to push onto a full stack, no attempts to pop from an empty stack, that subprogram bodies implement their functional requirements, and so on. As a result, we get a maximally robust implementation of a reusable stack abstraction providing all the facilities required for production use.

Make with Ada 2020: The SmartBase - IoT Adjustable Bed

John Singleton's The SmartBase makes your existing adjustable bed safer and easier to use by adding voice control and safe (and fun!) LED underbed lighting! Additionally, this project won first place prize in the 2019/20 Make with Ada competition.

GNAT Community 2020 is here!

We are happy to announce that the GNAT Community 2020 release is now available! Read the post for access to download and to find out about this year's release highlights.

CuBit: A General-Purpose Operating System in SPARK/Ada

Last year, I started evaluating programming languages for a formally-verified operating system. I've been developing software for a while, but only recently began work in high integrity software development and formal methods. There are several operating system projects, like the SeL4 microkernel and the Muen separation kernel, that make use of formal verification. But I was interested in using a formally-verified language to write a general-purpose OS - an environment for abstracting the underlying hardware while acting as an arbiter for running the normal applications we're used to.

The FACE™ open systems strategy gaining traction in the avionics industry

The FACE™ approach is a government-industry initiative for reducing defense system life cycle costs through portable and reusable software components. It consists of a technical approach — a software standard based on well-defined common interfaces — and a business strategy for encouraging the development and deployment of FACE conformant products.

Make with Ada 2020: CryptAda - (Nuclear) Crypto on Embedded Device

Team CryptAda's project collects entropy, manages an entropy pool, implements a homemade PRNG, and generates RSA keys directly on the board with an accent on security. Additionally, this project won a finalist prize in the 2019/20 Make with Ada competition.

Make with Ada 2020: Disaster Management with Smart Circuit Breaker

Shahariar's project ensures safety against electrical fire or shock during an earthquake, flood, gas leakage or fire breakout by disconnecting the mains with a smart circuit breaker. Additionally, this project won a finalist prize in the 2019/20 Make with Ada competition.

Relaxing the Data Initialization Policy of SPARK

SPARK always being under development, new language features make it in every release of the tool, be they previously unsupported Ada features (like access types) or SPARK specific developments. However, new features generally take a while to make it into actual user code. The feature I am going to present here is in my experience an exception, as it was used both internally and by external users before it made it into any actual release. It was designed to enhance the verification of data initialization, whose limitations have been a long standing issue in SPARK.

Ada for micro:bit Part 1: Getting Started

Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.

Ada for micro:bit Part 2: Push buttons

Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.

Make with Ada 2020: LoRaDa := Ada + LoRa;

Hedley Rainnie's project combines 6 different SoCs all programmed in Ada performing as a LoRa network. He also showcases a BLE bridge to a LoRa server. His project came about when him and his wife were musing about how to detect and deter unwanted garden visitors. This ongoing project won a finalist prize in the 2019/20 Make with Ada competition.

Introducing source code instrumentation in GNATcoverage

This is the first post of a series about GNATcoverage and source code instrumentation.In order to make GNATcoverage viable in more contexts, we planned several years ago to add instrumentation support in GNATcoverage for Ada sources. This feature reached maturation recently and is available in the last Continuous Release, so it is a good time to present it with a blog series!

GNATcoverage: getting started with instrumentation

This is the second post of a series about GNATcoverage and source code instrumentation. The previous post introduced how GNATcoverage worked originally and why we extended it to support source instrumentation-based code coverage computation. Let’s now see it in action in the most simple case: a basic program running on the host machine, i.e. the Linux/Windows machine that runs GNATcoverage itself.

Ada for micro:bit Part 3: Pin Output

Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.

Ada for micro:bit Part 4: Pin Input

Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.

Ada for micro:bit Part 5: Analog Output

Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.

Ada for micro:bit Part 6: Analog Input

Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.

Ada for micro:bit Part 7: Accelerometer

Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.

Ada for micro:bit Part 8: Music to my ears

Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.

Code Obfuscator for Ada using Libadalang and SPARK

A code obfuscator is a method of sharing coding discussions of real-world examples without giving away proprietary or classified information. This article shows an example of an Ada obfuscator, written in the SPARK language and using the Libadalang library to intelligently hide names and text within the source.

AdaCore Code of Conduct

Starting today, AdaCore has put in place a Code of Conduct (CoC) to ensure a positive environment for everyone willing and wanting to interact with us. With the development of this blog, our twitter accounts, and our GitHub corporate account, there is more and more communication between AdaCore and a number of communities. In this Code of Conduct we want to explain how we are going to moderate the AdaCore-maintained community spaces with the goal of maintaining a welcoming, friendly environment.

Make with Ada 2020: CHIP-8 Interpreter

Laurent Zhu's and Damien Grisonnet's project was accomplished for the EPITA Ada courses and won a finalist prize in the Make with Ada 2019/20 competition.

Ada 202x support in GNAT

News from the Ada front The next revision of the Ada standard is now almost ready, so it's time for a status update on where GNAT and AdaCore stand on this front!

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.

First beta release of Alire, the package manager for Ada/SPARK

A few years ago we realized that having a package manager for the Ada/SPARK community would be a game changer. Since then, AdaCore has been sponsoring and contributing to the Alire project created by Alejandro Mosteo from the Centro Universitario de la Defensa de Zaragoza. With this blog post I want to introduce Alire and explain why this project is important for the `Ada`/`SPARK` community.

Make with Ada 2020: Ada Robot Car With Neural Network

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.

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.

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.

Make with Ada 2020: ADArrose

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.

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.

Mini SAM M4 Ada BSP

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.

How To: GNAT Pro with Docker

Using GNAT Pro with containerization technologies, such as Docker, is so easy, a whale could do it!

Performance analysis and tuning of SPARKNaCl

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.

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.

Doubling the Performance of SPARKNaCl (again...)

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.

Showing Global contracts with GNAT Studio

In the integrated development environment, GNAT Studio, there is now a plugin that inserts the generated Global contracts inline with the code.

On the Benefits of Families ... (Entry Families)

Ada has a concurrency construct known as “entry families” that, in some cases, is just what we need to express a concise, clear solution.

From Rust to SPARK: Formally Proven Bip-Buffers

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.

An Introduction to Jorvik, the New Tasking Profile in Ada 2022

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.

Going beyond Ada 2022

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.

GNAT Community 2021 is here!

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:

SPARKNaCl with GNAT and SPARK Community 2021: Port, Proof and Performance

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.

Celebrating Women Engineering Heroes - International Women in Engineering Day 2021

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?

Announcing The First Ada/SPARK Crate Of The Year Award

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.

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”.

When the RISC-V ISA is the Weakest Link

NVIDIA has been using SPARK for some time now to develop safety- and security-critical firmware applications. At the recent DEF CON 29, hackers Zabrocki and Matrosov presented how they went about attacking NVIDIA firmware written in SPARK but ended up attacking the RISC-V ISA instead!Zabrocki starts by explaining the context for their red teaming exercise at NVIDIA, followed by a description of SPARK and their evaluation of the language from a security attack perspective. He shows how they used an extension of Ghidra to decompile the binary code generated by GNAT and describes the vulnerability they identified in the RISC-V ISA thanks to that decompilation. Matrosov goes on to explain how they glitched the NVIDIA chip to exploit this vulnerability. Finally, Zabrocki talks about projects used to harden RISC-V platforms.

A design pattern for OOP in Ada

When I do Object Oriented Programming with Ada, I tend to follow a design pattern that makes it easier for me and hopefully also for people reading my code.

Task Suspension with a Timeout in Ravenscar/Jorvik

This blog entry shows how to define an abstract data type that allows tasks to block on objects of the type, waiting for resumption signals from other components, for at most a specified amount of time per object. This "timeout" capability has been available in Ada from the beginning, via select statements containing timed entry calls. But what about developers working within the Ravenscar and Jorvik tasking subsets? Select statements and timed calls are not included within either profile. This new abstraction will provide some of the functionality of timed entry calls, with an implementation consistent with the Ravenscar and Jorvik subsets.

Enhancing the Security of a TCP Stack with SPARK

The developers of CycloneTCP library at Oryx Embedded partnered with AdaCore to replace the TCP part of the C codebase by SPARK code, and used the SPARK tools to prove both that the code is not vulnerable to the usual runtime errors (like buffer overflow) and that it correctly implements the TCP automaton specified in RFC 793. As part of this work, we found two subtle bugs related to memory management and concurrency. This work has been accepted for publication at the upcoming IEEE SecDev 2021 conference.

Starting micro-controller Ada drivers in the Alire ecosystem

A few days ago, someone asked on the Ada Drivers Library repository how to add support for the SAMD21 micro-controller. Nowadays, I would rather recommend people to contribute this kind of micro-controller support project to the Alire ecosystem. I started to write a few instructions on how to get started, but it quickly became a blog-worthy piece of text.

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.

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.

SPARKNaCl - Two Years of Optimizing Crypto Code in SPARK (and counting)

SPARKNaCl is a SPARK ver­sion of the Tweet­Na­Cl cryp­to­graph­ic 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.

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.

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.

AdaCore at FOSDEM 2022

Like previous years, AdaCore will participate in FOSDEM. Once again the event will be online only, but this won’t prevent us from celebrating Open Source software and it is an opportunity for even more people to participate around the world.

Ada/SPARK Crate Of The Year 2021 Winners Announced!

In June of 2021 we announced the launch of a new programming competition called 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 200 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, inside and outside the Ada/SPARK community, of the evolution and the energy of the ecosystem.

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.

Announcing Updates to learn.adacore.com

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.

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

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.

Handling Aliasing through Pointers in SPARK

As I explained in a blog post a couple of years ago, pointers are subjected to a strict ownership policy in SPARK. It prevents aliasing and allows for an efficient formal verification model. Of course, it comes at the cost of restrictions which might not be applicable to all usage. In particular, while ownership makes it possible to represent certain recursive data-structures, those involving cycles or sharing are de-facto forbidden. This is a choice, and not every proof tool did the same. For example, the WP plug-in of Frama-C supports pointers with arbitrary aliasing. If some information about the separation of memory cells is necessary to verify a program, then the user shall give the annotation explicitly. I have investigated modeling pointers with aliasing in SPARK as indices in a big memory array. I will present the results of my experiments in this blog post. We will see that, while such a representation is indeed possible modulo some hiding in SPARK, it can quickly become rather heavy in practice.

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.

Announcing The 2022 Ada/SPARK Crate Of The Year Award

We're happy to announce our the second edition of our 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.

A New Era For Ada/SPARK Open Source Community

Today we have two exciting announcements for the future of the Ada/SPARK ecosystem.

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.

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.

Join us at the High Integrity Software (HIS) Conference 2022!

After two years of virtual events, we are very happy to report that the High Integrity Software Conference (HIS) will be making a physical comeback on Tuesday 11th October 2022 at the Bristol Marriott Hotel City Centre, Bristol, UK. Since 2014, AdaCore has been co-organising the event with Capgemini Engineering (previously known as Altran Technologies, SA). The success and growth of the conference have ensured it remains a regular fixture for returning delegates, and the exciting lineup for this year's event will ensure HIS 2022 is no exception!

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.

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

New features for string literals and comments in GNAT Studio

We have added several new convenience features that help work with comments and string literals in Ada code.

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++.

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.

Coroutines in Ada, a Clean but Heavy Implementation

A few months ago I was reading this article about coroutines in game development and how they are great tools for writing scripts (as in movie scripts) in the same language as the game engine. Until then I heard about coroutines but never really gave them a thought, this piqued my curiosity.

Tis the Season to be Giving falalalala lalalala

Every year since 2015, a team of dedicated individuals led by Eric Wastl organizes an online programming challenge called: Advent of Code. The concept is simple yet brilliant: from December 1st to 25th, every day a new small programming exercise is published on the adventofcode.com website. This year we want to join the fun, and bring a little bit of extra motivation for a good cause.

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.

NVIDIA Security Team: “What if we just stopped using C?”

Today I want to share a great story about why many NVIDIA products are now running formally verified SPARK code. This blog post is in part a teaser for the case study that NVIDIA and AdaCore published today. Our journey begins with the NVIDIA Security Team. Like many other security oriented teams in our industry today, they were looking for a measurable answer to the increasingly hostile cybersecurity environment and started questioning their software development and verification strategies.

New Learn Course: Introduction To Embedded Systems Programming

A new online Learn course has been published offering an Introduction To Embedded Systems Programming.

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.

Our Contribution to the Ada Logo Discussion

From time to time we see, here and there, discussions in the Ada community about the design and adoption of a common logo to represent the language. Today we want to bring our contribution to this discussion by offering a logo to the Ada community.

Advent of Ada/SPARK 2022 Results

At the end of November we called the Ada and SPARK programmers community to take on a challenge for a good cause. We are now in January and it is time for the results!

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.

AdaCore at FOSDEM 2023

This year marks the return of the FOSDEM conference as an "in-person" event. As always, AdaCore will participate in this major gathering of the free and open source community.We encourage you to stop by the Ada-Europe booth (Building K, level 2) to have a chat or get answers to any questions regarding Ada, SPARK, or other topics, such as those covered in our blog.

AdaCore joins the Rust foundation

Last year we announced our strategic partnership with Ferrous Systems, a technology company specializing in the Rust programming language. Today we are announcing a new step in our involvement with the Rust ecosystem and community

Introduction to VSS library

The VSS (as an abbre­vi­a­tion for Vir­tu­al String Sub­sys­tem) library is designed to pro­vide advanced string and text pro­cess­ing capa­bil­i­ties. It offers a con­ve­nient and robust API that allows devel­op­ers to work with Uni­code text, regard­less of its inter­nal rep­re­sen­ta­tion. In this arti­cle, we will intro­duce you to the library and explain its pur­pose, high­light­ing its use­ful­ness for devel­op­ers work­ing in this area.

GNAT Pro 21.6 for LYNX MOSA.ic for Avionics (MfA)

AdaCore has partnered closely with Lynx to deliver Ada language support alongside its LYNX MOSA.ic software framework that comprises a real-time operating system (LynxOS-178), Linux and hypervisor (LynxSecure) technology.

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.

Explainable Program Proofs

Ever wanted to understand why program proof is not as easy as telling ChatGPT "can you prove that program <code>stuff</code> is correct for me?" A new book from top-notch programmer and program proof expert Rustan Leino answers all your questions. Or at least a good batch.

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.

Reducing Ada code bases with adareducer

How we're using Libadalang to create an automated Ada code reducer.

Building a GNAT SAS analysis pipeline on GitLab

This is the first part of a series in which we’ll implement a GNAT SAS analysis pipeline for Ada code on GitLab by making use of GNAT SAS 24 new features. We are focusing on getting a pipeline that "Just Works(tm)", leaving more advanced issues such as scalability, improvement of user experience, or maintainability for later.

From Desert Dunes to Humanitarian Aid: Inside the Epic Journey of the 4L Trophy Rally

Back in February 2023, my friend David and I embarked on an exciting journey for a worthy cause. We finally got our old Renault 4l fully restored by ourselves and heard the engine revving for the first time one week before the departure.

RecordFlux State Machines

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.

Advanced Journey with Ada: A Flight in Progress

We are thrilled to announce the launch of our highly anticipated course, "Advanced Journey with Ada: A Flight in Progress," which explores the advanced concepts of Ada programming. This course serves as a seamless continuation of our esteemed "Introduction to Ada" course.

SPARK, Beyond Normal Termination

When teaching SPARK to my students, I generally explain the central position of contracts in formal verification in the following way: Contracts of subprograms summarize their behavior - preconditions constrain their inputs, while postconditions describe their effects. It is an easy way to see contracts, However, not returning normally, for example looping forever or raising exceptions, is definitely a significant effect of a subprogram. Modeling that effect would be beneficial because if it occurs in an unexpected way it might cause the entire program to derail. Release 24.0 of SPARK includes contracts that can be used to reason about subprograms which do not return normally. This blog post describes them.

VSS: Cursors, Iterators and Markers

The VSS (as an abbre­vi­a­tion for Vir­tu­al String Sub­sys­tem) library is designed to pro­vide advanced string and text pro­cess­ing capa­bil­i­ties. It offers a con­ve­nient and robust API that allows devel­op­ers to work with Uni­code text, regard­less of its inter­nal rep­re­sen­ta­tion. Last time we provided overview of the library, and in this arti­cle, we will introduce concepts of cursors that are used to iterate, retrieve, and modify text data.

GNAT Pro Roadmap

Every year the GNAT Pro product family acquires new members and capabilities, to help our customers develop safer, more secure and more efficient code on newer hardware and software platforms. Moving forward, our goal is to offer a clear view on the future development of our technology. As part of this effort, we have made available a public roadmap for AdaCore products on our documentation platform.

A little bit of Photoshop® using GNAT for CUDA®

Today I want to go over some internal mechanisms of a Photoshop-like application to better illustrate an up-and-coming tech, GNAT for CUDA®, developed at AdaCore.

Announcements around Rust

AdaCore has two announcements about Rust that we’d like to share with you!

Extending Priority Inheritance Beyond Protected Operations

This blog entry shows how to define protected types that extend the language-defined priority inheritance for protected actions to the statements outside those protected actions. We create a mutex type for illustration.

Designing a WebAssembly toolchain for Ada/SPARK

WebAssembly (Wasm) is a binary instruction format for a stack-based virtual machine, which was designed as a portable compilation target for programming languages. Wasm can be executed in browsers, native runtimes and embedded contexts.The goal of my six-month internship at AdaCore was to draft a design for a toolchain that would support an Ada/SPARK workflow to WebAssembly. In this blog post the drafted design is introduced and discussed.

Formal Proof on Device Drivers with SPARK

Programming device drivers requires certain practices or operations. These include, for example, the multitude of volatile variables in the code. On the other hand, SPARK imposes a number of restrictions on programs and also limits the use of certain practices permitted in Ada. Here's a list of hurdles I encountered during my internship involving driver code and the rules authorized by SPARK. I also present ways of getting around these problems, as well as some best practices for having the most SPARK-compatible code in advance. This list is not exhaustive.

SPARK Tetris on the Raspberry Pi Pico

Tetris was the first computer game played in space but let's review our ambitions for the time and try to implement it on a Raspberry Pico first. This idea appeared during my internship at AdaCore. The main purpose of my internship was to explore the possibilities of formal verification in device drivers using SPARK. It seemed both very challenging and valuable to prove such low-level code to ensure safety and security.

Announcing the 2023 Ada/SPARK Crate of the Year Award

We're happy to announce the third edition of our programming awards, The Ada/SPARK Crate of the Year Award! This time with a different approach as you will see below. 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.

Bare-metal C++ development environment for certifiable safety-critical applications

We are happy to announce the availability of GNAT Pro for C++, a versatile development environment for bare-metal targets capable of supporting different subsets of the C++ language. It constitutes the best choice for safety-critical bare-metal systems that want to reduce complexity, memory footprint and execution-time overhead, paving the way to software certification. GNAT Pro for C++ targets popular hardware in the avionics, defense, railway, and space domains: PowerPC (32 bits), x86 (64 bits), RISC-V (32/64 bits), LEON3 (32 bits) and ARM (32/64 bits).

Identifying and authorizing users at AdaCore

Back in the 90s when AdaCore was founded, the state of IT security was very different. A unique Unix login and password were enough to connect to a shared server and run business applications. Most of the protocols used were still unencrypted, and the most elaborate access controls were based on Unix groups and perimeter defense. As the company evolved, we gave users access to more and more services, some not hosted on-premise. More services meant distinct credentials. Security-savvy users, who did not accept reusing the same password everywhere, had the burden of maintaining all these distinct credentials. Most credentials were long-lived, and very often shared. Also as the notion of perimeter defense became more and more fuzzy with the introduction of PaaS, IaaS, .. the need for safer access and communication protocols increased significantly.

An Introduction to Memory Safety Concepts and Challenges

This blog post explains the concept of memory safety and the most common memory errors. Then, it introduces three memory-safe languages that have built-in countermeasures against memory errors.

Memory Safety in Ada and SPARK through Language Features and Tool Support

This blog post describes how Ada and SPARK provide memory safety through a combination of language features, run-time checks, and static and dynamic analysis tools.

Announcing Ada binding to the wolfSSL library

Today, we at wolfSSL (https://www.wolfssl.com/) are happy to announce the availability of an Ada/SPARK binding that enables Ada applications to use post-quantum TLS 1.3 encryption through the wolfSSL embedded SSL/TLS library. The wolfSSL library is thread safe by design. Multiple threads can enter the library simultaneously without creating conflicts because wolfSSL avoids global data, static data, and the sharing of objects. When objects are used in the API the wolfSSL library provides opaque pointers to objects whose contents is only known internally by the wolfSSL library. This library interface design makes it easy to make bindings to other programming languages and at the same time enables the contents of the objects used internally to be highly configurable.

Announcing Advent of Ada 2023: Coding for a Cause!

We're thrilled to kick off the holiday season with the second edition of Advent of Ada, a programming challenge that not only tests your coding skills but also contributes to a meaningful cause.As many of you know, Advent of Code has become a beloved tradition since its inception in 2015. The concept is simple yet brilliant: from December 1st to 25th, every day a new small programming exercise is published on the adventofcode.com website. Participants get points for each completed exercise.

Advent of Ada/SPARK 2023 Results

At the end of November we called the Ada and SPARK programmers community to take on a challenge for a good cause. For each person completing one of the Advent of Code exercises using the Ada programming language, AdaCore would donate $10 to the Ada Developers Academy. And for those willing to go an extra mile, AdaCore would donate $20 if the solution is implemented in SPARK. We are now in January and it is time for the results!

Announcing Updates to learn.adacore.com

Some time ago, we announced some updates to the learn website. In the meantime, we published the Introduction To Embedded Systems Programming course and the initial parts of the Advanced Journey with Ada course. Today, we'd like to announce some updates that have been made to the learn website since then.

AdaCore Enhances GCC Security with Innovative Features

In a significant stride towards bolstering the security of the open-source ecosystem, AdaCore has recently contributed a set of security hardening features to the GCC project (GNU Compiler Collection). These features, designed to fortify the software produced by GCC against various cyber threats, highlight our commitment to advancing the field of secure programming and our 30+ years of contributing to the open-source software development ecosystem.

GNAT Static Analysis Suite: A Vision for Static Analysis in Ada

You may have noticed that over the past two years, we have made significant updates to our CodePeer product - the most visible change being the renaming of the product itself, now branded as “GNAT Static Analysis Suite”. For those who are already using the product and are looking to use the new version, it may be a good time to step back and share our vision, at AdaCore, for static analysis.

Memory Safety in Rust

Informally, memory safety in a program means that each data access is well behaved; i.e., is consistent with the item’s data type, does not impinge on any storage locations beyond the data value’s boundaries, and, if the program is multithreaded, does not produce an inconsistent or corrupted value. Memory safety violations result in undefined behavior, which is a Bad Thing: instances like the notorious “buffer overrun” can turn an otherwise safe and secure program into a ticking virtual time bomb. Some of the most eventful malware attacks in recent years are due to memory safety violations, and the topic has moved from techno-geek subreddits into mainstream discourse. Anyone developing or acquiring software, especially for applications with high assurance requirements, needs to pay attention.

DNSSEC and DMARC Compliance at AdaCore

While foundational to the internet, the traditional DNS system has its vulnerabilities. Threats such as DNS spoofing and cache poisoning pose significant risks to the integrity and authenticity of DNS data. DNSSEC is designed to address this risk.

Ada/SPARK Crate Of The Year 2023 Winners Announced!

In 2023 we announced the third edition of the Ada/SPARK Crate Of The Year Awards. We see the Alire source package manager as a game changer for Ada/SPARK, so we want to use the Crate of the Year awards to honor the people contributing to the ecosystem. This edition was different from the previous ones: we decided to depart from a submissions-based approach and instead consider all crates available in the Alire ecosystem. Today we are pleased to announce the results.

Enhancing Ada Embedded Development: The Power of Real-Time Logging with RTT

Efficient embedded development in Ada relies on powerful tools. Real-time logging plays a pivotal role, enabling live monitoring and analysis. Unlike traditional methods, SEGGER's Real-Time Transfer (RTT) method offers hardware-independent real-time logging with low latency.This article explores RTT's simplicity: storing protocol data in a ring buffer on the target device, read by the debugger without halting program execution. The provided Ada code showcases RTT's implementation, from buffer types to control blocks.Integration with development environments is seamless, as seen with the Cortex Debug extension for VS Code. The extension supports RTT, providing features like textual and graphical display of RTT stream data.In summary, SEGGER's RTT method is a powerful, hardware-independent solution for real-time logging in Ada development. Its efficiency and flexibility make it indispensable for debugging, error detection, and security in embedded systems. Explore the GitHub repository for a hands-on experience with RTT in Ada embedded development.

Co-Developing Programs and Their Proof of Correctness

I am delighted to announce that the Communications of the ACM has published a paper on SPARK: “Co-Developing Programs and Their Proof of Correctness”. The paper provides a comprehensive and up-to-date presentation of SPARK; as such, it’s a great reference to share with anyone - in industry, academia, or anywhere in between - who might like to know more about SPARK.

BACK TO THE BUILDING BLOCKS: AdaCore’s Contributions to Secure and Measurable Software

The focus on enhancing cybersecurity through various technological approaches and methodologies, as detailed in the White House Office of the National Cyber Director’s (ONCD) document titled “Back to the Building Blocks: A Path Toward Secure and Measurable Software" underscores a pivotal shift in how organizations, especially those at the helm of technological innovation, must adapt and respond to the ever-evolving landscape of cyber threats. This document provides an overview of some strategies and technologies that are critical in bolstering cybersecurity defenses.

International Women’s Day: My Career Journey

Every 8th March, International Women’s Day is celebrated around the world - it’s a great opportunity to highlight women’s talents, their achievements, and what makes them great at what they do.This year’s theme is #InspireInclusion. At AdaCore, this got us thinking about what our team values the most and how we strive to create a sense of belonging and community, no matter who our people are, their level of seniority, or where they’re based.Viviane Garese and Sofia Casale reveal more about their career journeys, their accomplishments in Software Engineering and Sales, and how AdaCore’s core value of collaboration helps to inspire inclusion at work every day.

AdaCore Contribution to Reducing GHG Emissions

Like any other company, AdaCore contributes to climate change through its activities. We recognize that it is our responsibility to reduce this negative impact, and we've been on a path to make measurable concrete progress in the reduction of our GHG emissions since 2019. In this post, we are describing our current progress and plans forward.

A Fresh Take on DO-178C Software Reviews

The software review is an essential part of the evidence required for certification according to DO-178C. In this blog post we reflect on the objectives and challenges regarding DO-178C compliance.

Ada Programming like it's 1985

A few days ago, someone posted a request for the Abacus Commodore 64 Ada compiler on the reddit Ada channel. After a quick look at the manual I decided to give it a try using a C64 emulator. How hard can it be?