67 entries tagged with #Runtime
by Yannick Moy , Lionel Matias
I can’t believe that I can prove that it can sortWhen 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.
A New Era For Ada/SPARK Open Source CommunityToday we have two exciting announcements for the future of the Ada/SPARK ecosystem.
Announcing Updates to learn.adacore.com
by Paul Jarrett
Ada Crate of the Year: Interactive code searchA retrospective on learning Ada and developing a tool with it in 2021 from 2021 Ada Crate of the Year Winner Paul Jarrett.
by Manuel Hatzl
SPARK Crate of the Year: Unbounded containers in SPARKManuel 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
by Yannick Moy , Claire Dross
Proving the Correctness of GNAT Light Runtime LibraryThe 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.
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.
by Paul Butcher
Fuzz Testing in International Aerospace GuidelinesThrough 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.
Starting micro-controller Ada drivers in the Alire ecosystemA 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.
by Yannick Moy
Enhancing the Security of a TCP Stack with SPARKThe 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.
by Pat Rogers
Task Suspension with a Timeout in Ravenscar/JorvikThis 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.
by Yannick Moy
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.
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”.
SPARKNaCl with GNAT and SPARK Community 2021: Port, Proof and PerformanceThis 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.
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.
by Pat Rogers
An Introduction to Jorvik, the New Tasking Profile in Ada 2022The 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.
by Pat Rogers
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.
Performance analysis and tuning of SPARKNaClThis 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.
Ada on any ARM Cortex-M device, in just a couple minutesIn this blog post I want to present a new tool that allows one to very quickly and easily start Ada programming on any ARM Cortex-M or RISC-V microcontroller.
by Paul Butcher
Finding Vulnerabilities using Advanced Fuzz testing and AFLplusplus v3.0
Some of you may recall an AdaCore blog post written in 2017 by Thales engineer Lionel Matias titled "Leveraging Ada Run-Time Checks with Fuzz Testing in AFL". This insightful post took us on a journey of discovery as Lionel demonstrated how Ada programs, compiled using GNAT Pro and an adapted assembler pass can be subjected to advanced fuzz testing. In order to achieve this Lionel demonstrated how instrumentation of the generated assembly code around jump and label instructions, could be subjected to grey-box (path aware) fuzz testing (using the original AFL v2.52b as the fuzz engine). Lionel explained how applying the comprehensive spectrum of Ada runtime checks, in conjunction with Ada's strong typing and contract based programming, enhanced the capabilities of fuzz testing beyond the abilities of other languages. Ada's advanced runtime checking, for exceptions like overflows, and the scrutiny of Ada's design by contract assertions allow corner case bugs to be found whilst also utilising fuzz testing to verify functional correctness.
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!
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.
by Emma Adby
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.
by Jon Andrew
CuBit: A General-Purpose Operating System in SPARK/AdaLast 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.
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.
Ada on the ESP8266Not 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.
Proving properties of constant-time crypto code in SPARKNaClOver 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.
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.
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:
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.
RecordFlux: From Message Specifications to SPARK CodeHandling 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.
Secure Use of Cryptographic Libraries: SPARK Binding for LibsodiumThe challenge faced by cryptography APIs is to make building functional and secure programs easy for the user. In this blog post I will present you how I created a SPARK binding for Libsodium, using strong typing and preconditions/postconditions to enforce a safe and functional use of basic cryptographic primitives.
by Boran Car
Bringing Ada To MultiZoneC 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.
Winning DTU RoboCup with Ada and SPARKThe 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 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.
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.
by Peter Chapin
Ten Years of Using SPARK to Build CubeSat Nano Satellites With StudentsMy 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.
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.
Ada on FPGAs with PicoRV32When 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.
by Yannick Moy
Security Agency Uses SPARK for Secure USB KeyANSSI, 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.
PolyORB now lives on Github
PolyORB, AdaCore's versatile distribution middleware, now lives on Github. Its new home is https://github.com/AdaCore/polyorb
by Rob Tice
SPARKZumo Part 2: Integrating the Arduino Build Environment Into GPSThis is part #2 of the SPARKZumo series of blog posts. This post covers the build system that was used to build the SPARKZumo project and how to automate the process in GPS.
by Rob Tice
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?
by Felix Krause
The Road to a Thick OpenGL Binding for Ada: Part 2This 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.
Leveraging Ada Run-Time Checks with Fuzz Testing in AFLFuzzing 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- 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.
Make with Ada 2017: Brushless DC Motor ControllerThis 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.
by Yannick Moy
Research Corner - Focused Certification of SPARK in CoqThe 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.
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.
by Yannick Moy
Frama-C & SPARK Day Slides and HighlightsThe 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.
by Yannick Moy
VerifyThis Challenge in SPARKThis 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.
by Jorge Real
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!
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.
by Pat Rogers
Getting started with the Ada Drivers Library device drivers
The Ada Drivers Library (ADL) is a collection of Ada device drivers and examples for ARM-based embedded targets. The library is maintained by AdaCore, with development originally (and predominantly) by AdaCore personnel but also by the Ada community at large. It is available on GitHub and is licensed for both proprietary and non-proprietary use.
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!
Verifying Tasking in Extended, Relaxed StyleTasking 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.
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.
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.
Porting the Ada Runtime to a new ARM boardA step by step tutorial to adapt the ARM runtime to new MCUs/boards.
by Yannick Moy
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.
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.
How to prevent drone crashes using SPARKThe 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.
by Martyn Pike
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.
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.
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.
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.