Developing secure code using SPARK – Part 1 -

Developing secure code using SPARK – Part 1

The modern cyberworld is a dangerous place. Software must not only be reliable—i.e., perform its intended functions—but also robust: It needs to withstand attempts at subversion from the array of threats posed by malevolent sources. Implementing security as an add-on isn’t effective. Performing static analysis retrospectively on the source code of an existing system may uncover bugs and vulnerabilities but can never demonstrate their absence. Instead, developers have to consider preventive measures from the start, and for the most critical kinds of systems, implement an approach backed by mathematical rigor.

One technique is to use an appropriate programming language that permits specifying relevant security-oriented properties (“contracts”), and then demonstrate statically that these properties are satisfied by applying automated tools as the system is being designed and implemented.

The SPARK language, a formally analyzable Ada subset augmented with special comment syntax for contracts, illustrates this approach. SPARK has been used, in conjunction with a development methodology known as Correctness by Construction (CbyC), to produce a variety of systems that need to achieve the highest levels of security and/or safety.

Because defects are prevented or caught early, the traditional debugging phase is much reduced. The level of effort required by using SPARK is around the same as for conventional systems, but with the benefit of much higher assurance that the system does what it is supposed to do, and does not do what it is not supposed to do.

Software security basics
Security is commonly defined as the protection of assets against unauthorized attempts to compromise their confidentiality, integrity, or availability. In the context of a computer system, an asset needs to be considered in a very general sense. It may consist of sensitive data (employee salaries or social security numbers), physical equipment that the system is controlling or monitoring, or even—and especially—the internal data structures and executable code of the software itself. In a safety-critical system, the assets may be human beings—for example passengers and crew on an aircraft, or a patient receiving medication from an infusion pump.

The measures taken to achieve sufficient security depend on the value of the assets (or the costs associated with recovering from a security breach) and the perceived likelihood of the threats and the skills of potential attackers. These measures fall into two categories:

  • Security functions such as user authorization or data encryption algorithms that are implemented by the software as part of the system architecture, and
  • Security assurance steps taken by the developer to demonstrate that the security functions have been implemented correctly, and that the rest of the system contains no vulnerabilities that could be exploited to defeat these functions.

This partitioning is illustrated in the Common Criteria standard,1 which is basically a catalog of security-related functional and assurance requirements that can be used to evaluate the security of products across a variety of application domains. In the Common Criteria the security assurance requirements are grouped into seven increasingly demanding sets, known as evaluation assurance levels (EALs; see figure 1). The lowest level, EAL1, “…is applicable where some confidence in correct operation is required, but the threats to security are not viewed as serious.” 1 At the other extreme, EAL7 “…is applicable…in extremely high-risk situations and/or where the high value of the assets justifies the higher costs.” 1

Figure 1: The Common Criteria defines a range of evaluation assurance levels (EALs). In a Common Criteria-based scenario, a product’s security requirements, both functional and assurance, are specified in an implementation-independent manner in a document known as a protection profile. A vendor developing a specific product can have it evaluated and certified against the relevant protection profile.

A higher EAL by itself does not necessarily mean a more secure product, since the interpretation of assurance requirements is based on both the associated security functional requirements and the intended deployment environment as defined in the protection profile. A product at a higher EAL that assumes installation on a standalone platform may be less secure, if used on a network, than a lower-EAL product designed for use on such a network.

EAL6 and EAL7 require the application of formal (i.e., mathematically based) methods; among other things, the developer must present a formal model of select security policies. The need for formal methods, and the increased scope, depth, and rigor required at these high EALs, are best satisfied by using languages and tools that have been designed for this purpose.

Security through language subsets ,br/>Programming languages are like cars: Power and performance can attract attention and create industry buzz but can also be dangerous when misused. Expressiveness through Object Orientation, concurrency support, exceptions, generic templates, and other modern features may help make code easier to develop and maintain, but their generality comes at a price.

Each raises issues that complicate the verification of high-integrity systems (i.e., systems that are safety critical, require high levels of security, or both). Problems stem from the complexity of the analysis required to demonstrate various program properties in the presence of the feature, and from possible “traps and pitfalls” in the feature’s usage that can cause vulnerabilities. And semantics optimized for run-time efficiency (such as the absence of array index bounds checking in C and C++) can lead to undefined behavior.

Language-related vulnerabilities have been exploited to defeat a system’s security. One of the best known examples is buffer overflow (assigning past the bounds of an array), which can lead to overwriting a memory address and thereby hijacking an application to execute malevolent code.

The Common Weakness Enumeration2 describes a large number of such vulnerabilities, as well as others (such as SQL injection and hard-coded passwords) that are at a higher semantic level and are not related to the choice of programming language. An ISO technical report3 analyzes some of the most frequently occurring language-related vulnerabilities and explains how to mitigate them, with language-specific annexes providing additional guidance.

High-integrity software must, of course, be reliable, but more generally must also be analyzable. Demonstrating that a system complies with its operative security or safety certification standard entails, among other things, examining the source code to show that the program’s time and space requirements are met and that its behavior is well-defined; for example, no references to uninitialized variables. The programming language will affect the ease or difficulty in performing this analysis.

Unfortunately, all general-purpose language—including Ada, C, C++, and Java—are too complex to be used, at their full generality, for high-integrity software. They may have features with implementation-dependent or undefined effects, or error-prone syntax or semantics, and in any event the full languages or their run-time libraries are too complex to support the analysis needed to demonstrate the relevant security or safety properties.

One solution is to choose a language subset that avoids problematic features. MISRA C4 and MISRA C++5 take this route, but neither C nor C++ was originally designed with a focus on high-integrity systems. It’s difficult to reorient a language’s underlying philosophy through a subset. In addition, both MISRA C and MISRA C++ include rules that are subject to interpretation, and thus may be enforced differently by different tools.

Java is another possible candidate for subsetting, but its highly dynamic nature, along with its dependence on automatic garbage collection for storage management, complicates the analysis needed to demonstrate time and space predictability. Subsetting can’t effectively solve these problems without largely negating the reasons for considering Java in the first place. Java’s extensive class libraries, moreover, would need to be restricted and/or rewritten, again defeating one of the language’s major benefits.

Ada provides a more appropriate basis for subsetting. Since the language was originally designed for high-integrity software, it has the relevant foundation for reliability, and it does not require the memory management complexity of Java.

Array indices are checked to make sure that they are within bounds, strong typing prevents misusing the value of one type as though it were of another type, and integer overflow raises an exception instead of wrapping around. The language also permits the inclusion of range constraints on scalar data; for example, an integer can be declared to be within the range 0 through 100. The ability to specify scalar range constraints increases the accuracy of bounds analysis and helps catch logic errors early.

Subsetting in Ada can actually be controlled by the application. The pragma Restrictions feature, introduced in Ada 95, allows the program to specify features that are not being used and thus do not require run-time support. The simpler run-time libraries are easier to analyze and also reduce the code footprint. The Ravenscar profile6, a subset of concurrency features amenable to safety or security certification, is specified as a set of such restrictions.

Defining a subset is useful and necessary but still does not directly address the issue of deducing security- or safety-related properties from the program text. For that purpose, a notation is needed that allows the developer to specify a program’s contracts: statically verifiable annotations that identify data object dependences, subprogram preconditions and postconditions, loop invariants, and similar properties. The SPARK language, originally designed by Praxis High-Integrity Systems (now Altran Praxis), takes this approach, using a specialized form of comment for its annotations.

Part Two of this article summarizes the basic elements of the SPARK technology and show how it addresses software security issues.

1. Common Criteria Portal.
2. MITRE Corp. Common Weakness Enumeration.
3. ISO/IEC JTC 1/SC 22/WG 23 Programming Language Vulnerabilities, Technical Report TR 24772. Guidance to avoiding vulnerabilities in programming languages through language selection and use (October 2010).
4. MISRA. Guidelines for the Use of the C Language in Critical Systems (October 2004).
5. MISRA. Guidelines for the Use of the C++ Language in Critical Systems (June 2008).
6. A. Burns, B. Dobbing, T. Vardanega. “Guide for the use of the Ada Ravenscar Profile in high integrity systems,” University of York Technical Report YCS-2003-348 (January 2003).
7. J. Barnes. High Integrity Software – The SPARK Approach to Safety and Security, Addison-Wesley, (2003).

Benjamin Brosgol is a senior member of the technical staff of AdaCore. He has been involved with programming language design and implementation for more than thirty years, concentrating on languages and technologies for high-integrity systems. He was a distinguished reviewer of the original Ada language specification and a member of the design team for the Ada 95 revision.

(This article was published previously on the EETimes web site.)  

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.