AdaCore Blog

An Insight Into the AdaCore Ecosystem

by Claire Dross –

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.

#Formal Verification    #SPARK   

by Emma Adby –

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.

by Emma Adby –

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.

by Emma Adby –

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.

#MakewithAda    #Ada    #SPARK   

by Jon Andrew –

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.

by Nicolas Setton –

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.

by Pat Rogers –

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.

#SPARK    #Ada    #Transitioning to SPARK   

by Abe Cohen –

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.

by Johannes Kliemann –

Ada on the ESP8266

Not long ago, AdaCore published its LLVM frontend for GNAT. Also quite recently Espressif updated their LLVM backend to LLVM 9 which also happens to be the LLVM version of GNAT. This gave me to the idea to try out if LLVMs promise of providing modular and reusable toolchain technologies is true.

by Martyn Pike –

A Trivial File Transfer Protocol Server written in Ada

For an upcoming project, I needed a simple way of transferring binary files over an Ethernet connection with minimal (if any at all) user interaction. A protocol that's particularly appropriate for this kind of usage is the Trivial File Transfer Protocol (TFTP).

by Roderick Chapman –

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.

#SPARK    #Cryptography    #Formal Verification   

by Ghjuvan Lacambre –

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.

#IDE    #gdb   

by Maxim Reznik –

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.

#WebAssembly    #web    #android   

by Pat Rogers –

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.

#Ada    #SPARK    #Robotics   

by Pierre-Marie de Rodat –

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:

#Libadalang   

by Vadim Godunko –

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.

#GNAT     #LLVM    #WebAssembly    #Programming    

by Fabien Chouteau –

AdaCore at FOSDEM 2020

Like last year and the year before, AdaCore will participate to the celebration of Open Source software at FOSDEM. It is always a key event for the Ada/SPARK community and we are looking forward to meet Ada enthusiasts. You can check the program of the Ada/SPARK devroom here.

#FOSDEM   

by Fabien Chouteau –

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.

#embedded    #STM32   

by Quentin Ochem –

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

by Paul Butcher –

AdaCore for HICLASS - Enabling the Development of Complex and Secure Aerospace Systems

What's changed? In 2019 AdaCore created a UK business unit and embarked on a new and collaborative venture researching and developing advanced UK aerospace systems. This blog introduces the reader to ‘HICLASS’, describes our involvement and explains how participation in this project is aligned with AdaCore’s core values.

#SPARK    #UK   

by Martyn Pike –

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

by Alexander Senier –

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.

#Formal Verification    #Formal Methods    #SPARK   

by Arnaud Charlet –

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.

#CodePeer    #QGen    #SPARK Pro    #Open Source   

by Michael Frank –

Learning SPARK via Conway's Game of Life

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

#SPARK     #Programming    

by Claire Dross –

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.

#SPARK    #Formal Verification   

by Arnaud Charlet –

Combining GNAT with LLVM

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

#GNAT     #LLVM   

by Emma Adby –

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. 

by Maxim Reznik, Yannick Moy –

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.

#virtual    #conference    #Ada   

by Isabelle Vialard –

Secure Use of Cryptographic Libraries: SPARK Binding for Libsodium

The challenge faced by cryptography APIs is to make building functional and secure programs easy for the user. In this blog post I will present you how I created a SPARK binding for Libsodium, using strong typing and preconditions/postconditions to enforce a safe and functional use of basic cryptographic primitives.

#SPARK    #Security    #Cryptography    #Binding   

by Joffrey Huguet, Johannes Kanig –

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.

#Formal Verification    #SPARK   

by Juan Zamorano –

Using Ada for a Spanish Satellite Project

I am an Associate Professor at Polytechnic University of Madrid’s (Universidad Politécnica de Madrid / UPM) in the Department of Architecture and Technology of Computer Systems. For the past several years I have been directing a team of colleagues and students in the development of a UPMSat-2 microsatellite. The project originally started in 2013 as a follow-to the UPM-SAT 1, launched by an Ariane-4 in 1995.

by Yannick Moy, Raphaël Amiard, Tucker Taft –

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.

#Ada    #SPARK   

by Claire Dross –

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.

#VerificationTools   

by Nicolas Setton –

GNAT Community 2019 is here!

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

by Boran Car –

Bringing Ada To MultiZone

C is the dominant language of the embedded world, almost to the point of exclusivity. Due to its age, and its goal of being a “portable assembler”, it deliberately lacks type-safety, opening up exploit vectors. Proposed solutions are partitioning the application into smaller intercommunicating blocks, designed with the principle of least privilege in mind; and rewriting the application in a type-safe language. We believe that both approaches are complementary and want to show you how to combine separation and isolation provided by MultiZone together with iteratively rewriting parts in Ada. We will take the MultiZone SDK demo and rewrite one of the zones in Ada.

#Ada    #embedded    #Embedded Development    #Security    #multizone    #Hex-Five   

by Allan Ascanius, Per Dalgas Jakobsen –

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.

#Robotics    #Ada    #SPARK   

by Joffrey Huguet –

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.

#SPARK    #Formal Verification    #Cryptography   

by Pamela Trevino –

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.

by Arnaud Charlet –

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.

#CodePeer   

by Peter Chapin –

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.

#SPARK    #Space    #Education    #Safety   

by Yannick Moy, Nicolas Setton, Ben Brosgol –

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.

#MISRA-C    #SPARK    #Safety    #Security   

by Yannick Moy, Nicolas Roche, Pierre-Marie de Rodat, Fabien Chouteau –

AdaCore at FOSDEM 2019

Like last year, we've sent a squad of AdaCore engineers to participate in the celebration of Open Source software at FOSDEM. Like last year, we had great interactions with the rest of the Ada and SPARK Community in the Ada devroom on Saturday. That's what we have to say about it.

#Ada    #SPARK    #Open Source    #Community   

by Rob Tice –

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.

#Fixed Point    #Floating Point    #Tasking    #Fractal    #AWS    #Generics   

by Rob Tice –

AdaFractal Part1: Ada with a Portable GUI

The is the first part of a multiple part post that covers the development of the AdaFractal project. The idea was to create fractals in Ada. Here we will cover how to use AWS to create a flexible and portable way to display the generated fractals without using bulky graphics libraries.

#AWS    #QNX    #VxWorks    #GUI    #Fractal   

by Quentin Ochem –

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.

by Quentin Ochem –

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.

by Yannick Moy –

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

#Formal Verification    #Cloud    #Security   

by Emma Adby –

It's time to Make with Ada!

The challenge Are 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!

by Pamela Trevino –

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.

by Julia Teissl –

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. 

Next Page »