Yannick Moy

As a programming language, Ada offers a number of features that require runtime support, e.g. exception propagation or concurrency (tasks, protected objects). The GNAT compiler implements this support in its runtime library, which comes in a number of different flavors, with more or less capability. The GNAT light runtime library is a version of the runtime library targeted at embedded platforms and certification, with an Operating System or without it (baremetal). It contains around 180 units focused mostly on I/O, numerics, text manipulation, memory operations.

Variants of the GNAT light runtime library have been certified for use at the highest levels of criticality in several industrial domains: avionics (DO-178), space (ECSS-E-ST40C), railway (EN 50128), automotive (ISO-26262). Details vary across certification regimes, but the common approach to certification used today is based on written requirements traced to corresponding tests, supported by test coverage analysis. Despite this strict certification process, some bugs were found in the past in the code. An ongoing project at AdaCore is applying formal proof with SPARK to the light runtime units, in order to prove their correctness: that the code is free of runtime errors, and that it satisfies its functional specifications.

So far, 30 units (out of 180) have been proved, and a few bugs fixed along the way (including a security vulnerability). In this talk, I will describe the approach followed, what was achieved, and what we expect to achieve.

Pointers are a notorious "defect attractor", in particular when dynamic memory management is involved. Ada mitigates these issues by having much less need for pointers overall (thanks to first-class arrays, parameter modes, generics) and stricter rules for pointer manipulations that limit access to dangling memory. Still, dynamic memory management in Ada may lead to use-after-free, double-free and memory leaks, and dangling memory issues may lead to runtime exceptions.

The SPARK subset of Ada is focused on making it possible to guarantee properties of the program statically, in particular the absence of programming language errors, with a mostly automatic analysis. For that reason, and because static analysis of pointers is notoriously hard to automate, pointers have been forbidden in SPARK until now. We are working at AdaCore since 2017 on including pointer support in SPARK by restricting the use of pointers in programs so that they respect "ownership" constraints, like what is found in Rust.

In this talk, I will present the current state of the ownership rules for pointer support in SPARK, and the current state of the implementation in the GNAT compiler and GNATprove prover, as well as our roadmap for the future.

SPARK started in 1987 as a restricted subset of Ada 83, defined by its own grammar rules. The overhaul of the language and toolset starting in 2010 increased greatly the language subset, dropping in effect the need for separate grammar rules. Since then, SPARK has progressively adopted most of the Ada features, to a point where the last remaining non-SPARK significant Ada feature today is pointers. We have started work on including safe pointers in SPARK, borrowing the ideas of pointer ownership from Rust. So one can legitimately wonder what difference remains between SPARK and Ada.

In the first part of this talk, I will lay out the principles that have guided us through the inclusion of language features in SPARK since 2010. I will describe in particular the trade-offs that we considered for support of important features like recursion, types with non-static constraints, generics, object orientation, concurrency. I will give a preview of the support envisioned for pointers in SPARK. So that the distinction between Ada and SPARK appears clearly: it's not about quantity, it's about safety and security.

In the second part of this talk, I will give a tour of FOSS projects which are using SPARK today: Aida, Certyflie, Muen, PolyORB-HI, Pulsar, StratoX, Tokeneer. For each one, I will describe at which level of assurance SPARK is used, with how much efforts and for which benefits. Then I will focus on the largest one, Muen, an x86/64 separation kernel for high assurance. Finally, we will look at the resources which are available to the community for FOSS development in SPARK.

SPARK is a programming language and a set of tools for building highly reliable software. The SPARK language is a subset of Ada and can be compiled with the GNAT toolchains to a wide range of platforms, including the popular ARM Cortex M3, M4 and M7. The SPARK language also provides specification features, so that the intended behavior of the program can be embedded in the program itself. The SPARK formal verification tool can check that a program does not contain any run-time error, such as buffer or integer overflows, and that the code complies with its specification. We will demonstrate these capabilities on a game of Tetris, whose core game logic has been proved, and which has been ported to several embedded platforms: SAM4S Xplained Pro Evaluation Kit, Pebble Time watch, Unity game engine, Arduboy game platform. We will show in particular that you don’t need any specific mathematical background to achieve such results!