AdaCore Blog

How Ada and SPARK Can Increase the Security of Your Software

How Ada and SPARK Can Increase the Security of Your Software

by Yannick Moy , Roderick Chapman

AdaCore Technologies for Cyber Security booklet

There is a long-standing debate about which phase in the Software Development Life Cycle causes the most bugs: the specification phase or the coding phase? Along with the information on the cost to fix these bugs, answering this question would allow better allocation of QA (Quality Assurance) resources. Furthermore, the cost of bug fixes remains the subject of much debate.

A recent study by NIST shows that, in the software industry at large, coding bugs are causing the majority of security issues. They analyzed the provenance of security bugs across all publicly disclosed vulnerabilities in the National Vulnerability Database from 2008 to 2016. They discovered that coding bugs account for two thirds of the total. As they say:

The high proportion of implementation errors suggests that little progress has been made in reducing these vulnerabilities that result from simple mistakes, but also that more extensive use of static analysis tools, code reviews, and testing could lead to significant improvement.

Our view at AdaCore is that the above list of remedies lacks a critical component for "reducing these vulnerabilities that result from simple mistakes" and probably the most important one: pick a safer programming language! This might not be appropriate for all your software, but why not re-architect your system to isolate the most critical parts and progressively rewrite them with a safer programming language? Better still - design your next system this way in the first place. What safer language to choose? One candidate is Ada, or its SPARK subset. How can they help? We've collected the answers to that question in a booklet to help people and teams who want to use Ada or SPARK for increasing the security of their software. It is freely available here.

Posted in #Ada    #SPARK    #Security   

About Yannick Moy

Yannick Moy

Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.

About Roderick Chapman

Roderick Chapman

Rod is Director of Protean Code Limited. He specializes in the design, implementation and verification of high-integrity software systems. For many years, Rod led the SPARK design team at Praxis and Altran in the UK, and continues to work closely with the SPARK team at AdaCore.