We’ll be running a series of excerpts from a book written by Roderick Chapman and Yannick Moy that cover AdaCore Technologies for Cyber Security. Here’s the first, and it serves as an introduction to what you’ll be seeing in upcoming pieces. Note that the original content comes from AdaCore. 

Read part two here.

It seems that every week’s news brings a story about yet another high-profile failure of a computer system owing to a security issue. These problems have a significant impact on the public, businesses, and government alike, affecting the reputation and share price of major organizations. In the most critical industry sectors, company directors face liability and governance concerns in an increasingly litigated environment.

In general, the “security” of computer systems can be characterized as a weakest-link scenario where attackers need only find and exploit a single weakness in any part of a system, including its hardware, software, operational environment, people, or operating procedures. Many attacks rely on social engineering, insiders, human factors, accidental misuse, and so on. These issues are important aspects of secure system design, but aren’t the focus here. We refer you to Ross Anderson’s Security Engineering book, the US CERT website, or the recently established Cyber Security Body of Knowledge (CyBOK) project for an overview of these wider issues.

Instead, this document focuses on a common attack vector—that of insufficiently secure software—and what can be done about it. More specifically, we concentrate on the contribution that the Ada and SPARK languages and their associated tools can make. Ada was designed from the outset to support the needs of “high assurance” systems; its strengths in this area are now becoming more widely recognized as the operational environment has become more malicious, and hence less tolerant of defective software. From the outset, Ada was designed to emphasize readability, understanding, and verification. Many pernicious defects that plague other languages are absent from Ada. For example:

• Ada’s syntax prevents several problems, including confusion of assignment and comparison, the “dangling else” problem, and the unintentional use of the null statement.
• Ada doesn’t require the explicit use of “pointers” for low-level programming, parameter passing, or the use of array types. As such, a huge number of “pointer-related” defects are entirely avoided.
• Ada’s strong typing prevents a host of issues, including assignment of incompatible values to one another, confusion over “promotion” of types, and so on.
• Ada has high-level features for concurrent programming, freeing the programmer from low-level use of “locks” or semaphores and threads.

SPARK, a formally analyzable subset of Ada, inherits all of Ada’s strengths and offers additional advantages for high-assurance software. These include the ability to mathematically prove program properties such as the correct data uses, the absence of run-time errors, and even functional correctness with respect to a formally specified set of requirements.

Upcoming pieces will covers why producing secure software is such a challenge, and thus motivates our technical approach; the Ada and SPARK languages describing AdaCore’s tools, with a focus on how they can support an evidence-based assurance case for security; a selection of common “vulnerabilities” in software, and how Ada and AdaCore’s tools can address these issues; a number of industrial scenarios, from purely retrospective analysis of legacy systems, to new developments, to systems that involve mixed criticality and development technologies; and a “call to arms” for software developers.

Note that many of the technologies covered here and in upcoming parts will be discussed in lots more detail at the upcoming Sound Static Analysis for Security Workshop.

Dr. Roderick Chapman is an independent consulting engineer with more than 20 years of experience in the development and certification of critical software. Following graduation from the University of York in the U.K., Rod joined Praxis (now Altran UK). Rod is a regular speaker at international conferences, and he is widely recognized as a leading authority on high integrity software development, programming language design, and software verification tools. In February 2015, Rod was appointed Honorary Visiting Professor in the Department of Computer Science at the University of York.

Dr. Yannick Moy is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory with INRIA (France). At AdaCore, he works on the software source code analyzers CodePeer and SPARK Pro. Yannick has led the development of the SPARK 2014 technology, which he has presented in articles, at conferences, in courses and in blogs (blog.adacore.com). Yannick previously worked on source code analyzers at PolySpace (now The MathWorks) and at the Université Paris-Sud.

eletter-05-21-2018 eletter-05-22-2018