66 entries tagged with #face
by Paul Butcher
Finding Vulnerabilities using Advanced Fuzz testing and AFLplusplus v3.0
Some of you may recall an AdaCore blog post written in 2017 by Thales engineer Lionel Matias titled "Leveraging Ada Run-Time Checks with Fuzz Testing in AFL". This insightful post took us on a journey of discovery as Lionel demonstrated how Ada programs, compiled using GNAT Pro and an adapted assembler pass can be subjected to advanced fuzz testing. In order to achieve this Lionel demonstrated how instrumentation of the generated assembly code around jump and label instructions, could be subjected to grey-box (path aware) fuzz testing (using the original AFL v2.52b as the fuzz engine). Lionel explained how applying the comprehensive spectrum of Ada runtime checks, in conjunction with Ada's strong typing and contract based programming, enhanced the capabilities of fuzz testing beyond the abilities of other languages. Ada's advanced runtime checking, for exceptions like overflows, and the scrutiny of Ada's design by contract assertions allow corner case bugs to be found whilst also utilising fuzz testing to verify functional correctness.
Make with Ada 2020: The autonomous firetruckThe AFT (Autonomous FireTruck) is a prototype of an autonomous firetruck that can put out fire without risking people's lives. This project won a finalist prize in the Make with Ada 2019/20 competition.
Ada for micro:bit Part 8: Music to my ears
Ada 202x support in GNAT
News from the Ada front The next revision of the Ada standard is now almost ready, so it's time for a status update on where GNAT and AdaCore stand on this front!
Make With Ada 2020: High Integrity Sumobot
Blaine Osepchuk's project won a finalist prize in the Make with Ada 2019/20 competition. This project was originally posted on Hackster.io here. For those interested in participating in the 2020/21 competition, registration is now open and project submissions will be accepted until Jan 31st 2021, register here.
Ada for micro:bit Part 7: Accelerometer
Ada for micro:bit Part 6: Analog Input
Ada for micro:bit Part 5: Analog Output
Ada for micro:bit Part 4: Pin Input
Ada for micro:bit Part 3: Pin OutputWelcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
Code Obfuscator for Ada using Libadalang and SPARKA code obfuscator is a method of sharing coding discussions of real-world examples without giving away proprietary or classified information. This article shows an example of an Ada obfuscator, written in the SPARK language and using the Libadalang library to intelligently hide names and text within the source.
Ada for micro:bit Part 2: Push buttons
The FACE™ open systems strategy gaining traction in the avionics industryThe FACE™ approach is a government-industry initiative for reducing defense system life cycle costs through portable and reusable software components. It consists of a technical approach — a software standard based on well-defined common interfaces — and a business strategy for encouraging the development and deployment of FACE conformant products.
by Emma Adby
Make with Ada 2020: CryptAda - (Nuclear) Crypto on Embedded DeviceTeam CryptAda's project collects entropy, manages an entropy pool, implements a homemade PRNG, and generates RSA keys directly on the board with an accent on security. Additionally, this project won a finalist prize in the 2019/20 Make with Ada competition.
by Emma Adby
Make with Ada 2020: The SmartBase - IoT Adjustable BedJohn Singleton's The SmartBase makes your existing adjustable bed safer and easier to use by adding voice control and safe (and fun!) LED underbed lighting! Additionally, this project won first place prize in the 2019/20 Make with Ada competition.
by Pat Rogers
From Ada to Platinum SPARK: A Case Study for Reusable Bounded StacksThis blog entry describes the transformation of an Ada stack ADT into a completely proven SPARK implementation that relies on static verification instead of run-time enforcement of the abstraction’s semantics. We will prove that there are no reads of unassigned variables, no array indexing errors, no range errors, no numeric overflow errors, no attempts to push onto a full stack, no attempts to pop from an empty stack, that subprogram bodies implement their functional requirements, and so on. As a result, we get a maximally robust implementation of a reusable stack abstraction providing all the facilities required for production use.
by Pat Rogers
Making an RC Car with Ada and SPARK
As a demonstration for the use of Ada and SPARK in very small embedded targets, I created a remote-controlled (RC) car using Lego NXT Mindstorms motors and sensors but without using the Lego computer or Lego software. I used an ARM Cortex System-on-Chip board for the computer, and all the code -- the control program, the device drivers, everything -- is written in Ada. Over time, I’ve upgraded some of the code to be in SPARK. This blog post describes the hardware, the software, the SPARK upgrades, and the repositories that are used and created for this purpose.
Using GNAT-LLVM to target Ada to WebAssembly
The GNAT-LLVM project provides an opportunity to port Ada to new platforms, one of which is WebAssembly. We conducted an experiment to evaluate the porting of Ada and the development of bindings to use Web API provided by the browser directly from Ada applications.
Ada on a FeatherI was quite happy to see AdaFruit release their first Feather format board including a micro-controller with plenty of Ada support, the STM32F4. I bought a board right away and implemented some support code for it.
by Paul Butcher
AdaCore for HICLASS - Enabling the Development of Complex and Secure Aerospace Systems
What's changed?In 2019 AdaCore created a UK business unit and embarked on a new and collaborative venture researching and developing advanced UK aerospace systems. This blog introduces the reader to ‘HICLASS’, describes our involvement and explains how participation in this project is aligned with AdaCore’s core values.
RecordFlux: From Message Specifications to SPARK CodeHandling binary data is hard. Errors in parsers routinely lead to critical security vulnerabilities. In this post we show how the RecordFlux toolset eases the creation of formally verified binary parsers in SPARK.
The Power of Technology Integration and Open Source
Part of our core expertise at AdaCore is to integrate multiple technologies as smoothly as possible and make it a product. This started at the very beginning of our company by integrating a code generator (GCC) with an Ada front-end (GNAT) which was then followed by integrating a debugger engine (GDB) and led to today's rich GNAT Pro offering.
Secure Use of Cryptographic Libraries: SPARK Binding for LibsodiumThe challenge faced by cryptography APIs is to make building functional and secure programs easy for the user. In this blog post I will present you how I created a SPARK binding for Libsodium, using strong typing and preconditions/postconditions to enforce a safe and functional use of basic cryptographic primitives.
Proving a simple program doing I/O ... with SPARKThe functionality of many security-critical programs is directly related to Input/Output (I/O). This includes command-line utilities such as gzip, which might process untrusted data downloaded from the internet, but also any servers that are directly connected to the internet, such as webservers, DNS servers and so on. In this blog post we show an approach that deals with error handling and reasoning about content, and demonstrate the approach using the cat command line utility.
Using Ada for a Spanish Satellite Project
I am an Associate Professor at Polytechnic University of Madrid’s (Universidad Politécnica de Madrid / UPM) in the Department of Architecture and Technology of Computer Systems. For the past several years I have been directing a team of colleagues and students in the development of a UPMSat-2 microsatellite. The project originally started in 2013 as a follow-to the UPM-SAT 1, launched by an Ariane-4 in 1995.
by Boran Car
Bringing Ada To MultiZoneC 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.
by Yannick Moy
Amazon Relies on Formal Methods for the Security of AWSByron Cook, who founded and leads the Automated Reasoning Group at Amazon Web Services (AWS) Security, gave a powerful talk at the Federated Logic Conference in July about how Amazon uses formal methods for ensuring the security of parts of AWS infrastructure. In the past four years, this group of 20+ has progressively hired well-known formal methods experts to face the growing demand inside AWS to develop tools based on formal verification for reasoning about cloud security. What is unique so far is the level of investment at AWS in formal verification as a means to radically eliminate some security problems, both for them and for their customers. This is certainly an approach we're eager to support with our own investment in the SPARK technology.
by Julia Teissl
Train control using Ada on a Raspberry Pi
I was looking for a topic for my master thesis in embedded systems engineering when one of my advisor proposed the idea of programming a control system for autonomous trains in Ada. Since I am fascinated by the idea of autonomous vehicles I agreed immediately without knowing Ada.
Ada on FPGAs with PicoRV32When 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.
by Rob Tice
SPARKZumo Part 2: Integrating the Arduino Build Environment Into GPSThis 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.
Getting Rid of Rust with AdaThere 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.
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?
by Felix Krause
The Road to a Thick OpenGL Binding for Ada: Part 2This 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.
by Felix Krause
The Road to a Thick OpenGL Binding for Ada: Part 1
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.
Leveraging Ada Run-Time Checks with Fuzz Testing in AFLFuzzing 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.
Cross-referencing Ada with Libadalang
Libadalang has come a long way since the last time we blogged about it. In the past 6 months, we have been working tirelessly on name resolution, a pretty complicated topic in Ada, and it is finally ready enough that we feel ready to blog about it, and encourage people to try it out.
Make with Ada 2017- Ada Based IoT Framework
SummaryThe Ada IoT Stack consists of an lwIp (“lightweight IP”) stack implementation written in Ada, with an associated high-level protocol to support embedded device connectivity nodes for today’s IoT world. The project was developed for the Make With Ada 2017 competition based on existing libraries and ported to embedded STM32 devices.
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.
Physical Units Pass the Generic TestThe support for physical units in programming languages is a long-standing issue, which very few languages have even attempted to solve. This issue has been mostly solved for Ada in 2012 by our colleagues Ed Schonberg and Vincent Pucci who introduced special aspects for specifying physical dimensions on types. This dimension system did not attempt to deal with generics though. As was noted by others, handling generics in a dimensional analysis that is, like in GNAT, a compile-time analysis with no impact on the executable size or running time, is the source of the problem of dimension handling. Together with our partners from Technical Universitat München, we have finally solved this remaining difficulty.
Make with Ada 2017: Brushless DC Motor ControllerThis project involves the design of a software platform that provides a good basis when developing motor controllers for brushless DC motors (BLDC/PMSM). It consist of a basic but clean and readable implementation of a sensored field oriented control algorithm. Included is a logging feature that will simplify development and allows users to visualize what is happening. The project shows that Ada successfully can be used for a bare-metal project that requires fast execution.
by Rob Tice
The Adaroombot ProjectThe 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.
DIY Coffee Alarm ClockA few weeks ago one of my colleagues shared this kickstarter project : The Barisieur. It’s an alarm clock coffee maker, promising to wake you up with a freshly brewed cup of coffee every morning. I jokingly said “just give me an espresso machine and I can do the same”. Soon after, the coffee machine is in my office. Now it is time to deliver :)
GPS for bare-metal developers
In my previous blog article, I exposed some techniques that helped me rewrite the Crazyflie’s firmware from C into Ada and SPARK 2014, in order to improve its safety.
by Jorge Real
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!
by Pat Rogers
Getting started with the Ada Drivers Library device drivers
The Ada Drivers Library (ADL) is a collection of Ada device drivers and examples for ARM-based embedded targets. The library is maintained by AdaCore, with development originally (and predominantly) by AdaCore personnel but also by the Ada community at large. It is available on GitHub and is licensed for both proprietary and non-proprietary use.
Going After the Low Hanging BugAt AdaCore, we have a strong expertise in deep static analysis tools (CodePeer and SPARK), and we have been relying on the compiler GNAT and our coding standard checker GNATcheck to deal with more syntactic or weakly-semantic checks. The recent Libadalang technology, developed at AdaCore, provided us with an ideal basis to develop specialized light-weight static analyzers. As an experiment, we implemented two simple checkers using the Python binding of Libadalang. The results on our own codebase were eye-opening: we found a dozen bugs in the codebases of the tools we develop at AdaCore (including the compiler and static analyzers).
Introducing LibadalangAdaCore is working on a host of tools that works on Ada code. The compiler, GNAT, is the most famous and prominent one, but it is far from being the only one. At AdaCore, we already have several other tools to process Ada code: the ASIS library, GNAT2XML, the GPS IDE. A realization of the past years, however, has been that we were lacking a unified solution to process code that is potentially evolving, potentially incorrect Ada code. Hence Libadalang.
Make with Ada: DIY instant cameraThere are moments in life where you find yourself with an AdaFruit thermal printer in one hand, and an OpenMV camera in the other.
Make With Ada Winners Announced!
Judging for the first annual Make with Ada competition has come to an end and we can now reveal the results.
Integrate new tools in GPSThis blog, the first in a series, explains the basic mechanisms that GPS (the GNAT Programming Studio) provides to integrate external tools. A small plugin might make your daily workflow more convenient by providing toolbar buttons and menus to spawn your tool and parse its output.
Unity & AdaUsing Ada technologies to develop video games doesn’t sound like an an obvious choice - although it seems like there could be an argument to be made. The reverse, however, opens some more straightforward perspectives.
GNAT Programming Studio (GPS) on GitHubThe GPS source repository has been published on GitHub. This post briefly describes how you can access it, and hopefully contribute.
Make with Ada: ARM Cortex-M CNC controller
I started this project more than a year ago. It was supposed to be the first Make with Ada project but it became the most challenging from both, the hardware and software side.
SPARKSMT - An SMTLIB Processing Tool Written in SPARK - Part IToday I will write the first article in a short series about the development of an SMTLIB processing tool in SPARK. Instead of focusing on features, I intend to focus on the how I have proved absence of run-time errors in the name table and lexer. I had two objectives: show absence of run-time errors, and do not write useless defensive code. Today's blog will be about the name table, a data structure found in many compilers that can map strings to a unique integer and back. The next blog post will talk about the lexical analyzer.
Make with Ada: Candy dispenser, with a twist...
A few months ago, my colleague Rebecca installed a candy dispenser in our kitchen here at AdaCore. I don’t remember how exactly, but I was challenged to make it more… fun.
by Yannick Moy , Jamie Ayre , Emma Adby
Ada Lovelace Bicentennial
The three of us attended the Ada Lovelace Symposium in Oxford (UK). The two days were one fantastic discovery after another about the life, achievements and legacy of Ada Lovelace, the programming pioneer who lent her name to the Ada language.
Make with Ada: Formal proof on my wristWhen the Pebble Time kickstarter went through the roof, I looked at the specification and noticed the watch was running on an STM32F4, an ARM cortex-M4 CPU which is supported by GNAT. So I backed the campaign, first to be part of the cool kids and also to try some Ada hacking on the device.
by David Hauzar
SPARK 16: Generating Counterexamples for Failed ProofsWhile the analysis of failed proofs is one of the most challenging aspects of formal verification, it would be much easier if a tool would automatically find values of variables showing why a proof fails. SPARK Pro 16, to be released in 2016, is going to introduce such a feature. If a proof fails, it attempts to generate a counterexample exhibiting the problem. This post introduces this new feature, developed in the scope of the ProofInUse laboratory.
Traits-Based ContainersThis post describes the design of a new containers library. It highlights some of the limitations of the standard Ada containers, and proposes a new approach using generic packages as formal parameters to make these new containers highly configurable at compile time.
Make with Ada: "The Eagle has landed"July 20, 1969, 8:18 p.m. UTC, while a bunch of guys were about to turn blue on Earth, commander Neil A. Armstrong confirms the landing of his Lunar Module (LM), code name Eagle, on the moon. Will you be able to manually land Eagle on the Sea of Tranquillity?
AdaCore Releases GNAT Pro 7.3, QGen 1.0 and GNATdashboard 1.0
February saw the annual customer release of a number of important products. This is no mean task when you consider the fact that GNAT Pro is available on over 50 platforms and supports over 150 runtime profiles (ranging from Full Ada Support to the very restricted Zero Footprint Profile suitable for safety-critical development). All in all, from the branching of the preview version to the customer release it takes us nearly 4 months to package everything up! Quality is assured through the internally developed AdaCore Factory.
Tetris in SPARK on ARM Cortex M4
Tetris is a well-known game from the 80's, which has been ported in many versions to all game platforms since then. There are even versions of Tetris written in Ada. But there was no version of Tetris written in SPARK, so we've repaired that injustice. Also, there was no version of Tetris for the Atmel SAM4S ARM processor, another injustice we've repaired.