AdaCore Blog

An Insight Into the AdaCore Ecosystem

by Elsa Ferrara
Formal Proof on Device Drivers with SPARK

Formal Proof on Device Drivers with SPARK

Programming device drivers requires certain practices or operations. These include, for example, the multitude of volatile variables in the code. On the other hand, SPARK imposes a number of restrictions on programs and also limits the use of certain practices permitted in Ada. Here's a list of hurdles I encountered during my internship involving driver code and the rules authorized by SPARK. I also present ways of getting around these problems, as well as some best practices for having the most SPARK-compatible code in advance. This list is not exhaustive.

by Thijs Dreef
Designing a WebAssembly toolchain for Ada/SPARK

Designing a WebAssembly toolchain for Ada/SPARK

WebAssembly (Wasm) is a binary instruction format for a stack-based virtual machine, which was designed as a portable compilation target for programming languages. Wasm can be executed in browsers, native runtimes and embedded contexts.The goal of my six-month internship at AdaCore was to draft a design for a toolchain that would support an Ada/SPARK workflow to WebAssembly. In this blog post the drafted design is introduced and discussed.

by Vadim Godunko
VSS: Cursors, Iterators and Markers

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   

by Claire Dross
SPARK, Beyond Normal Termination

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    

by Fabien Chouteau
The End of Binary Protocol Parser Vulnerabilities

The End of Binary Protocol Parser Vulnerabilities

This week we announced a new tool called RecordFlux. The goal of RecordFlux is to address one of the most critical parts of the software stack in terms of security, binary protocol parsers/serializers.From a protocol specification written in the RecordFlux Domain Specific Language (DSL), the tool can generate provable SPARK code. This means memory safety (no buffer overruns), absence of integer overflow errors, and even proof of functional properties. In this blog post I will try to explain how this is a game changer for cybersecurity.

by Maxim Reznik
Introduction to VSS library

Introduction to VSS library

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. In this arti­cle, we will intro­duce you to the library and explain its pur­pose, high­light­ing its use­ful­ness for devel­op­ers work­ing in this area.

#Unicode    #strings    #Libraries    #vss