AdaCore Blog

72 entries tagged with #Safety

by Fabien Chouteau

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 Johannes Kliemann

Adding Ada to Rust

While implementing application logic in Ada or SPARK is an improvement over a pure C project, its weakest link is still the C code in the SDK. On the other hand, there are many libraries, board support packages, and SDKs written in Rust, easily usable with Cargo. So instead of building the Ada application on top of a C base, one could use a Rust base instead to combine the large catalog of ready-to-use software with Rust's safety features, providing a much more solid base for an Ada project.

by Yannick Moy

When Formal Verification with SPARK is the Strongest Link

Security is only as strong as its strongest link. That's important to keep in mind for software security, with its long chain of links, from design to development to deployment. Last year, members of NVIDIA's Offensive Security Research team (aka "red team") presented at DEF CON 29 their results on the evaluation of the security of a firmware written in SPARK and running on RISC-V. The ended up not finding vulnerabilities in the code, but in the RISC-V ISA instead. This year, the same team presented at DEF CON 30 a retrospective on the security evaluation of 17 high-impact projects since 2020. TL;DR: using SPARK makes a big difference for security, compared to using C/C++.

#Security    #SPARK    #Formal Verification   

by Fabien Chouteau

Embedded Ada/SPARK, There's a Shortcut

For years in this blog my colleagues and I have published examples, demos, and how-to’s on Ada/SPARK embedded (as in bare-metal) development. Most of the time, if not always, we focused on one way of doing things: to start from scratch and write everything in Ada/SPARK, from the low level drivers to the application. While this way of doing Ada/SPARK embedded will yield the best results in terms of software quality, it might not be the most efficient in all cases. In this blog post I want to present an alternative method to introduce Ada/SPARK into your embedded development projects.

#Embedded   

by Paul Butcher

Join us at the High Integrity Software (HIS) Conference 2022!

After two years of virtual events, we are very happy to report that the High Integrity Software Conference (HIS) will be making a physical comeback on Tuesday 11th October 2022 at the Bristol Marriott Hotel City Centre, Bristol, UK. Since 2014, AdaCore has been co-organising the event with Capgemini Engineering (previously known as Altran Technologies, SA). The success and growth of the conference have ensured it remains a regular fixture for returning delegates, and the exciting lineup for this year's event will ensure HIS 2022 is no exception!

by Claire Dross

Handling Aliasing through Pointers in SPARK

As I explained in a blog post a couple of years ago, pointers are subjected to a strict ownership policy in SPARK. It prevents aliasing and allows for an efficient formal verification model. Of course, it comes at the cost of restrictions which might not be applicable to all usage. In particular, while ownership makes it possible to represent certain recursive data-structures, those involving cycles or sharing are de-facto forbidden. This is a choice, and not every proof tool did the same. For example, the WP plug-in of Frama-C supports pointers with arbitrary aliasing. If some information about the separation of memory cells is necessary to verify a program, then the user shall give the annotation explicitly. I have investigated modeling pointers with aliasing in SPARK as indices in a big memory array. I will present the results of my experiments in this blog post. We will see that, while such a representation is indeed possible modulo some hiding in SPARK, it can quickly become rather heavy in practice.

#SPARK    #Data Structures    #Formal Verification   

by Quentin Ochem , Florian Gilcher

AdaCore and Ferrous Systems Joining Forces to Support Rust

For over 25 years, AdaCore has been committed to supporting the needs of safety- and mission-critical industries. This started with an emphasis on the Ada programming language and its toolchain, and over the years has been extended to many other technologies. AdaCore’s product offerings today include support for the Ada language and its formally verifiable SPARK subset, C and C++, and Simulink and Stateflow models. We have accomplished this while addressing the requirements of various safety standards such as DO-178B/C, EN 50128, ECSS-E-ST-40C / ECSS-Q-ST-80C, IEC 61508 and ISO 26262.

by Yannick Moy

SPARKNaCl - Two Years of Optimizing Crypto Code in SPARK (and counting)

SPARKNaCl is a SPARK ver­sion of the Tweet­Na­Cl cryp­to­graph­ic library, developed by formal methods and security expert Rod Chapman. For two years now, Rod has been developing and optimizing this open-source cryptographic library while preserving the automatic type-safety proof across code changes and tool updates. He has recently given a talk about this experience that I highly recommend.

#SPARK    #Cryptography    #Formal Verification   

by Paul Butcher

Fuzz Testing in International Aerospace Guidelines

Through the HICLASS UK research group, AdaCore has been developing security-focused software development tools that are aligned with the objectives stated within the avionics security standards. In addition, they have been developing further guidelines that describe how vulnerability identification and security assurance activities can be described within a Plan for Security Aspects of Certification.

#Fuzzing    #Cyber Security    #Civil Avionics    #DO-356A    #ED-203A   

by Yannick Moy

When the RISC-V ISA is the Weakest Link

NVIDIA has been using SPARK for some time now to develop safety- and security-critical firmware applications. At the recent DEF CON 29, hackers Zabrocki and Matrosov presented how they went about attacking NVIDIA firmware written in SPARK but ended up attacking the RISC-V ISA instead!Zabrocki starts by explaining the context for their red teaming exercise at NVIDIA, followed by a description of SPARK and their evaluation of the language from a security attack perspective. He shows how they used an extension of Ghidra to decompile the binary code generated by GNAT and describes the vulnerability they identified in the RISC-V ISA thanks to that decompilation. Matrosov goes on to explain how they glitched the NVIDIA chip to exploit this vulnerability. Finally, Zabrocki talks about projects used to harden RISC-V platforms.

#Security    #SPARK    #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 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.

#Security   

by Pat Rogers

From Ada to Platinum SPARK: A Case Study for Reusable Bounded Stacks

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

#SPARK    #Ada    #Transitioning to SPARK   

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 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 Allan Ascanius , Per Dalgas Jakobsen

Winning DTU RoboCup with Ada and SPARK

The Danish Technical University has a yearly RoboCup where autonomous vehicles solve a number of challenges. We participated with RoadRunner, a 3D printed robot with wheel suspension, based on the BeagleBone Blue ARM-based board and the Pixy 1 camera with custom firmware enabling real-time line detection. Code is written in Ada and formally proved correct with SPARK at Silver level.

#Robotics    #Ada    #SPARK   

by Peter Chapin

Ten Years of Using SPARK to Build CubeSat Nano Satellites With Students

My colleague, Carl Brandon, and I have been running the CubeSat Laboratory at Vermont Technical College (VTC) for over ten years. During that time we have worked with nearly two dozen students on building and programming CubeSat nano satellites. Because of their general inexperience, and because of the high student turnover rate that is natural in an educational setting, our development process is often far from ideal. Here SPARK has been extremely valuable to us. What we lack in rigor of the development process we make up for in the rigor of the SPARK language and tools. In November 2013 we launched a low Earth orbiting CubeSat. The launch vehicle contained 13 other university built CubeSats. Most were never heard from. One worked for a few months. Ours worked for two years until it reentered Earth's atmosphere as planned in November 2015.

#SPARK    #Space    #Education    #Safety   

by Yannick Moy , Nicolas Setton , Ben Brosgol

A Readable Introduction to Both MISRA C and SPARK Ada

MISRA C is the most widely known coding standard restricting the use of the C programming language for critical software. For good reasons. For one, its focus is entirely on avoiding error-prone programming features of the C programming language rather than on enforcing a particular programming style. In addition, a large majority of rules it defines are checkable automatically (116 rules out of the total 159 guidelines), and many tools are available to enforce those. As a coding standard, MISRA C even goes out of its way to define a consistent sub-language of C, with its own typing rules (called the "essential type model" in MISRA C) to make up for the lack of strong typing in C.

#MISRA-C    #SPARK    #Safety    #Security   

by Emma Adby

Welcoming New Members to the GNAT Pro Family

As we see the importance of software grow in applications, the quality of that software has become more and more important. Even outside the mission- and safety-critical arena customers are no longer accepting software failures (the famous blue screens of death, and there are many...). Ada has a very strong answer here and we are seeing more and more interest in using the language from a range of industries. It is for this reason that we have completed our product line by including an entry-level offer for C/C++ developers wanting to switch to Ada and reinforced our existing offer with GNAT Pro Assurance for programmers building the most robust software platforms with life cycles spanning decades.

#GNAT Pro    #Ada   

by J. German Rivera

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.

by Jonas Attertun

Make with Ada 2017: Brushless DC Motor Controller

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

#Makers    #MakewithAda    #STM32    #Embedded   

by Yannick Moy

New Guidance for Adoption of SPARK

While SPARK has been used for years in companies like Altran UK, companies without the same know-how may find it intimidating to get started on formal program verification. To help with that process, AdaCore has collaborated with Thales throughout the year 2016 to produce a 70-pages detailed guidance document for the adoption of SPARK. These guidelines are based on five levels of assurance that can be achieved on software, in increasing order of costs and benefits: Stone level (valid SPARK), Bronze level (initialization and correct data flow), Silver level (absence of run-time errors), Gold level (proof of key properties) and Platinum level (full functional correctness). These levels, and their mapping to the Development Assurance Levels (DAL) and Safety Integrity Levels (SIL) used in certification standards, were presented at the recent High Confidence Software and Systems conference.

#Formal Verification    #SPARK   

by Yannick Moy

Verified, Trustworthy Code with SPARK and Frama-C

Last week, a few of us at AdaCore have attended a one-day workshop organized at Thales Research and Technologies, around the topic of "Verified, trustworthy code - formal verification of software". Attendees from many different branches of Thales (avionics, railway, security, networks) were given an overview of the state-of-practice in formal verification of software, focused on two technologies: the SPARK technology that we develop at AdaCore for programs in Ada, and the Frama-C technology developed at CEA research labs for programs in C. The most interesting part of the day was the feedback given by three operational teams who have experimented during a few months with either SPARK (two teams) or Frama-C (one team). The lessons learned by first-time adopters of such technologies are quite valuable.

#SPARK    #Formal Methods   

by Yannick Moy

SPARKSkein: From tour-de-force to run-of-the-mill Formal Verification

In 2010, Rod Chapman released an implementation in SPARK of the Skein cryptographic hash algorithm, and he proved that this implementation was free of run-time errors. That was a substantial effort with the previous version of the SPARK technology. We have recently translated the code of SPARKSkein from SPARK 2005 to SPARK 2014, and used GNATprove to prove absence of run-time errors in the translated program. The difference between the two technologies is striking. The heroic effort that Rod put in the formal verification of the initial version of SPARKSkein could now be duplicated with modest effort and modest knowledge of the technology, thanks to the much greater proof automation that the SPARK 2014 technology provides, as well as various features that lower the need to provide supporting specifications, most notably contracts on internal subprograms and loop invariants.

#Dev Projects    #Formal Verification    #SPARK   

by Anthony Leonardo Gracio

How to prevent drone crashes using SPARK

The Crazyflie is a very small quadcopter sold as an open source development platform: both electronic schematics and source code are directly available on their GitHub and its architecture is very flexible. Even if the Crazyflie flies out of the box, it has not been developed with safety in mind: in case of crash, its size, its weight and its plastic propellers won’t hurt anyone! But what if the propellers were made of carbon fiber, and shaped like razor blades to increase the drone’s performance? In theses circumstances, a bug in the flight control system could lead to dramatic events. In this post, I present the work I did to rewrite the stabilization system of the Crazyflie in SPARK 2014, and to prove that it is free of runtime errors. SPARK also helped me to discover little bugs in the original firmware, one of which directly related with overflows. Besides the Crazyflie, this work could be an inspiration for others to do the same work on larger and more safety-critical drones.

#UAVs    #crazyflie    #SPARK    #Drones   

by Yannick Moy

A Building Code for Building Code

In a recent article in Communications of the ACM, Carl Landwehr, a renowned scientific expert on security, defends the view that the software engineering community is doing overall a poor job at securing our global information system and that this is mostly avoidable by putting what we know works to work, to the point that most vulnerabilities could be completely avoided by design if we cared enough. Shocking! Or so it should appear.

#Ada    #SPARK    #Static Analysis    #Security   

by Olivier Ramonat

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.

#GNAT Pro    #SPARK Pro    #GPS    #GNATbench    #GNATdashboard    #Ada    #AdaCore Factory    #CodePeer    #QGen   

by Yannick Moy

Use of SPARK in a Certification Context

Using SPARK or any other formal method in a certification requires that the applicant agrees with the certification authority on the verification objectives that this use of formal methods allows to reach, and how this is obtained and documented. In order to facilitate this process, the participants to the workshop on Theorem Proving in Certification have produced a draft set of guidelines, now publicly available.

#Formal Verification    #Certification