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