17 entries tagged with #RISC V

by Kyriakos Georgiou

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

by Roderick Chapman

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

by Roderick Chapman

Doubling the Performance of SPARKNaCl (again...)

Following my last blog entry, further experiments show how the performance of SPARKNaCl can be doubled (again), plus analysis of worst-case stack usage and code size at all optimization levels.

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

by Roderick Chapman

Performance analysis and tuning of SPARKNaCl

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

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

by Fabien Chouteau

Ada on any ARM Cortex-M device, in just a couple minutes

In 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 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 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 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 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 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 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 Fabien Chouteau

Ada on FPGAs with PicoRV32

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

#Embedded #RISC-V #Ada

by Emma Adby , Fabien Chouteau

GNAT Community 2018 is here!

Calling all members of the Ada and SPARK community, we are pleased to announce that GNAT Community 2018 is here! adacore.com/download

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?

#CCG #SPARK #Arduino #RISC V #Embedded