AdaCore Technologies for Cybersecurity

Roderick Chapman & Yannick Moy

Building secure software is a challenging task. It seems that almost every week we read the news about yet another computer system that has failed in some way in the face of malicious or accidental misuse. “Cyber Security” is a wide-ranging field, spanning human factors, hardware design, sociology, and legal issues, in addition to software engineering. This booklet summarizes the contribution that the Ada and SPARK languages and AdaCore’s tools can make to this final area—how to develop and verify correct and secure software.

Unlike AdaCore’s previous guides to airborne and rail system software, this booklet does not follow the structure or requirements of a particular standard—in part because there is no widely used security standard that is required in practice. Instead it offers a more general treatment of the problem, but also includes an analysis of how AdaCore’s technologies help address the weaknesses identified in the MITRE Corporation’s Common Weakness Enumeration (CWE). The content is based on the authors’ many years of practical experience in the development of high-end secure systems, the design of the Ada and SPARK programming languages, and research into program verification tools.

The booklet is intended for readers who are involved with software at any level (developers, project managers, procurement personnel) and who would like to learn how currently available technology can help address some of the most serious challenges associated with software and security. Our goal is to provide useful guidance both to those who are using other languages and are interested in the benefits that Ada offers, and to existing Ada users who might be confronted with new security requirements.