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.
We are happy to announce that, AdaCore, alongside Altran and Jaguar Land Rover will be major sponsors of the fifth edition of the renowned High Integrity Software Conference on the 6th November in Bristol!
We are very proud to announce the availability of our new Ada and SPARK learning platform learn.adacore.com, which will replace AdaCoreU(niversity) e-learning platform. Learn all about it in this blog post.
Calling all members of the Ada and SPARK community, we are pleased to announce that GNAT Community 2018 is here! adacore.com/download
ANSSI, 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.
There is a long-standing debate about which phase in the Software Development Life Cycle causes the most bugs: is it the specification phase or the coding phase? A recent study by NIST shows that, in the software industry at large, coding bugs are causing the majority of security issues. Choosing a safer language like Ada or SPARK is a critical component for reducing these vulnerabilities that result from simple mistakes. In a new freely available booklet, we explain how these languages and the associated toolsets can be used to increase the security of software.
Last week, the programmer Hillel posted a challenge (the link points to a partial postmortem of the provided solutions) on Twitter for someone to prove a correct implementation of three small programming problems: Leftpad, Unique, and Fulcrum.
PolyORB, AdaCore's versatile distribution middleware, now lives on Github. Its new home is https://github.com/AdaCore/polyorb
This 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.
One of the most criticized aspect of the Ada language throughout the years has been its outdated syntax. Fortunately, AdaCore decided to tackle this issue by implementing a new, modern, syntax for Ada.
There are a lot of DIY CNC projects out there (router, laser, 3D printer, egg drawing, etc.), but I never saw a DIY CNC sandblaster. So I decided to make my own.
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?
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 user Alexander Senier presented recently at BOB Konferenz in Germany their use of SPARK for building secure mobile architectures. What's nice is that they build on the guarantees that SPARK provides at software level to create a secure software architecture based on the Genode operating system framework. They present 3 interesting architectural designs that make it possible to build a trustworthy system out of untrustworthy building blocks. Almost as exciting as Alchemy's goal of transforming lead into gold! Here is the video of that presentation.
Updated July 2018
Tokeneer is a software for controlling physical access to a secure enclave by means of a fingerprint sensor. This software was created by Altran (Praxis at the time) in 2003 using the previous generation of SPARK language and tools, as part of a project commissioned by the NSA to investigate the rigorous development of critical software using formal methods. The project artefacts, including the source code, were released as open source in 2008. Tokeneer was widely recognized as a milestone in industrial formal verification. We recently transitioned this software to SPARK 2014, and it allowed us to go beyond what was possible with the previous SPARK technology. We have also shown how security vulnerabilities introduced in the code can be detected by formal verification.
This 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.
With the recent addition of a Manual Proof capability in SPARK 18, it is worth looking at an example which cannot be proved by automatic provers, to see the options that are available for proving it with SPARK. We present three ways to complete a proof beyond what automatic provers can do: using an alternative automatic prover, proving interactively inside our GPS IDE, and using an alternative interactive prover.
Bitcoin is getting a lot of press recently, but let's be honest, that's mostly because a single bitcoin worth 800 USD in January 2017 was worth almost 20,000 USD in December 2017. However, bitcoin and its underlying blockchain are beautiful technologies that are worth a closer look. Let’s take that look with our Ada hat on!
This blog post is part one of a tutorial based on the OpenGLAda project and will cover some the background of the OpenGL API and the basic steps involved in importing platform-dependent C functions.
