AdaCore Blog

50 entries tagged with #Linux

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.

#wolfSSL   

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    #Runtime    #Proof   

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

#SPARK    #STM32    #Embedded   

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.

#SPARK     #Cryptography    #Formal Verification    #Code generation    #RISC-V    #Security   

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.

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   

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    #Frama-C    #Security    #Formal Methods    #Static Analysis   

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.

#Testing    #Ada    #VerificationTools   

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.

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.

#Raspberry Pi    #ARM    #Linux    #Ada    #Roomba   

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!

#STM32    #Ravenscar    #Ada    #Makers    #Embedded Development   

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!

#Code generation    #Ada   

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!

#cable porn   

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.

#Language    #Formal Verification    #SPARK