Building Safety by Design: CHERI in Critical Systems Development

Paul Butcher, the Secure Avioincs by Design Project Manager for AdaCore, discusses the usage of CHERI in safety-critical software.

#CHERI   

Should I choose Ada, SPARK, or Rust over C/C++?

At AdaCore, we’re in the business of supporting people who develop high-integrity software, in particular for embedded systems. In terms of programming languages, this means supporting the most commonly found candidates, which in 2024 include C/C++, Ada/SPARK, and Rust. If you’ve already made your decision, we will support you. However, in a number of situations, people ask us: “What should we do? What’s the best out there?”. While it’s difficult to give a one-size-fits-all answer, there are some strategic elements to consider.

#Ada    #Rust    #SPARK    #C++   

Ada GameDev Part 3: Enjoy Video Games Programming with Raylib

In April 2024 a streamer named Tsoding developed a video game from start to finish in Ada in 20 days. He seemed to have enjoyed the experience, to the point where he says that Ada will be the next trendy programming language for game development. Ignoring the potential irony in the streamer’s comment, I thought let’s give Ada gamedev a little push in that direction.

#Ada    #GameDev    #raylib   

Getting Started with Renode: Simulating an Ada STM32F429disco Blinky Firmware.

I recently watched the talks from the 28th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2024), which was held in Barcelona last June.One talk that stood out was "HiRTOS: a Multicore RTOS Written in SPARK Ada" by J. German Rivera. In his presentation, he mentioned running HiRTOS on Renode, an open-source simulation and virtual development framework for complex embedded systems (https://github.com/renode/renode).

#Renode   

Secure Supply Chain and vulnerability reports at AdaCore

In the past few years, attacks compromising software supply chains (MITRE ATT&CK T1195) have become more prominent, with cases such as NotPeya, Target data breach, Solarwinds, … The impact of the SolarWinds attack in 2020 in the United States led to Executive Order 14028, which strongly focuses on improving the security and integrity of software supply chains. Since then, various initiatives have been started, either by governments or organizations, such as SSDF (“Secure Software Development Framework”) by NIST or the SLSA framework (“Supply Chain Levels for Software Artifacts”) by OpenSSF (2021).

#SLSA   

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.

#Embedded    #DIY    #vscode   

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.

#Docker    #GitLab    #CodePeer    #DevOps    #GNAT SAS   

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.

#memory safety    #safe programming languages    #Ada    #SPARK   

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.

#Programming     #memory safety    #memory bugs    #Ada    #SPARK    #Rust   

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.

#CUDA    #GNAT Pro    #Photoshop    #GPU    #Ada    #AdaCore    #NVIDIA    #GPGPU    #Computer Vision    #Image Analysis    #Bilateral Filter    #Signal Processing    #parallel computing    #Surface Blur    #Image Processing   

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

#C++    #Safety Critical Development    #Certification    #Bare-metal   

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.

#Ada    #Protected Types    #Priority Inheritance   

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.

#vss    #Unicode    #strings    #Libraries   

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.

#SPARK    

Reducing Ada code bases with adareducer

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

#Libadalang    #Ada   

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.

#SPARK    #Dad Jokes