Page 1 of 1
Developing safe and secure applications requires appropriate technology, and the programming language has a significant impact. Its features should help in producing reliable code that can be analyzed to demonstrate relevant properties and to support the required safety or security certification activities. The original Ada language was designed to meet these goals, and subsequent revisions have stayed true to its philosophy. The latest version, Ada 2012, represents another major advance in the language’s evolution. Its features for “contract-based programming” allow the programmer to specify checkable assertions about program properties, including operation preconditions and postconditions, and type invariants. These contracts are in effect program requirements expressed in the source text.
Industries with strong safety or security demands generally require systems to be evaluated against a relevant certification standard. As one example, avionics systems for commercial or military aircraft need to meet the guidance defined in DO-178B (recently revised to DO-178C). This guidance comprises a set of objectives and associated activities that apply to the various software life cycle processes, with an emphasis on verification. Which objectives apply depends on the level of the software component, and the software level in turn is determined by the effect of the component’s failure on the aircraft’s continued safe flight and landing. The levels range from E (no effect) to A (catastrophic). Higher levels require more objectives to be met, and for some objectives, meeting them with independence (the developer cannot be the verifier) and/or with additional configuration management rigor. The various levels and their interpretations are shown in Figure 2.
The DO178B/178C levels range from E (no effect) to A (catastrophic). Higher levels require more objectives to be met, and for some objectives, meeting them with independence.
For systems where security is a concern, the de facto standard is the Common Criteria, which defines and categorizes two kinds of requirements. The first is Security Functional Requirements (SFRs): security-related services that the system must perform. The other is Security Assurance Requirements (SARs): processes that give confidence that the SFRs are implemented correctly. The SARs are grouped into Evaluation Assurance Levels (EALs), ranging from EAL1 (“functionally tested”) to EAL7 (“formally verified design and tested”), as depicted in Figure 3. A given product is evaluated against a Protection Profile characteristic of the application domain; the Protection Profile identifies the assets to be protected, the set of SFRs to be implemented, the required EAL, and the assumptions about the operational environment in which the system is to be deployed.
SARs are grouped into Evaluation Assurance Levels (EALs), ranging from EAL1 (functionally tested) to EAL7 (formally verified design and tested).
Although a software safety standard such as DO-178B and a software security standard such as the Common Criteria differ in obvious and major ways, a basic underlying similarity can be abstracted from the details. In both cases assurance that a system is sufficiently safe and/or secure is obtained by demonstrating two main properties. First, that the required safety/security functionality—maintaining flight parameters within specified airframe limits, supplying appropriate access controls to sensitive data—has been implemented correctly and so on. Second is that the system is immune to failure conditions that could compromise the safety/security requirements.
Programming Language Matters
The ease or difficulty of demonstrating these properties depends on many factors. Skilled developers and sound development practices are obviously important, as is a clear and complete formulation of the software’s requirements (functionality, performance and so forth). But another factor is the programming language(s) and supporting tools. The software is ultimately represented as program text in some language, and claims about program correctness and absence of vulnerabilities need to be expressed and demonstrated in terms of this representation.
The syntax and semantics of the language affect the ease or difficulty of constructing arguments to justify such claims. The main requirements on the language are reliability and analyzability. Reliability in this context means good error detection, absence of “traps and pitfalls,”, and effective software engineering support. Meanwhile, analyzability refers to its predictability—the ability to derive program properties such as freedom from exceptions. Since the expressive power of general-purpose languages tends to introduce complexity that compromises either the reliability or analyzability goal or both, another important requirement is the ability to define subsets for which these goals can be achieved. In short, the programming language can be part of the solution or part or the problem.
A Little Ada History
The Ada language is firmly on the solution side. It was originally designed against a set of requirements for developing reliable, maintainable software. It was designed in particular for critical real-time systems with safety and/or security constraints in mind. Features such as compile-time checks with strong typing, data encapsulation, and run-time checks for array indexing and integer overflow help prevent errors or detect them before they end up in delivered code. Other features that Ada assimilated from software methodology research—including exception handling, tasking (a structured and high-level set of concurrent/threading programming features), and a general facility for generic templates—provide expressive power that eases the job of developing and maintaining large complex systems.
Over the years the Ada language has gone through several revisions. Ada 95 represented a significant upgrade, introducing comprehensive support for Object-Oriented Programming, an efficient and reliable mechanism for state-based mutual exclusion (“protected types”), a general separate compilation facility supporting hierarchical libraries, and an extensive predefined environment. It also added a facility, pragma Restrictions, that lets the programmer specify features that are not being used. At first glance this may seem curious; isn’t the programming language supposed to offer increased expressiveness and generality? Yes, but for some kinds of applications, “too much” can be a problem. Features with complex semantics may introduce the risk of errors; for example, with Object-Oriented Programming there is an important but perhaps subtle syntactic difference between “static binding” and “dynamic binding”: the difference between interpreting an operation based on compile-time versus run-time type information.
Features with run-time semantics—concurrency, exception handling, dynamic memory management—require run-time support libraries that are typically furnished by compiler vendors and not by the application developers. These libraries become part of the executable code and, in systems requiring safety or security certification, are therefore subject to the same requirements as the application code. A language having a very large set of built-in libraries may be more problematic than beneficial in this case. Shrinking or eliminating the run-time libraries will ease the certification effort and of course also reduce the run-time footprint.
Ada’s pragma Restrictions address this issue in a standardized fashion. The program text specifies which features are not used; the compiler enforces these restrictions; and the program builder can link in simplified run-time libraries that only support the features that are used. A practical example is the Ravenscar Profile: a deterministic tasking subset, defined through a set of Restrictions pragmas, which is appropriate in embedded systems with size constraints and/or certification requirements.
The next version of the language, Ada 2005, was relatively modest in scope. The major enhancements were in the area of “programming in the large.” For example, Java-like interfaces were added to the Object-Oriented Programming features, new syntax was introduced for detecting errors associated with operation overriding, and a mechanism for defining interdependent package specifications was added to the separate compilation facility. Other enhancements included standardizing the Ravenscar Profile, defining several new task dispatching policies for real-time systems (such as Earliest Deadline First), and significantly extending the predefined library (containers, linear algebra and so on).
Ada 2012 Continues Tradition
Throughout its evolution, Ada has been faithful to its original design philosophy: emphasizing source code readability over compactness, detecting errors early, and offering high-level facilities that minimize the conceptual distance between the software structure and the problem space. The latest version of the language, Ada 2012, continues this tradition in several ways, most significantly through a new facility known as “contract-based programming.” The programmer can annotate certain program entities—operations and types—with “contract” information: Boolean conditions specifying requirements such as data relationships that must be satisfied at specific points in program execution. Embedding requirements directly in the program text adds a further check that the program logic does what the requirements say it should do and helps ensure consistency between life cycle data that might otherwise get “out of sync,” and in particular supports some of the traceability objectives in DO-178B and DO-178C.
Ada 2012 provides three main kinds of contracts. First are preconditions for operations, which must be true in order for the operation to be invoked. Next are postconditions for operations, which must be true when the operation returns. And the third is Type invariants, which are in effect postconditions that must hold on return from operations invoked on the type’s objects.
An example illustrating these concepts is a package that encapsulates a container type for a table where the element type has an ordering relation, where each table object has a fixed (bounded) size, and where the elements of each table are stored in ascending order and without duplication. The following contracts may be specified for the type and for the insertion and removal operations:
The type invariant, which states that the elements of each table object are in sorted order.
The insertion operation’s precondition, which states that the table object has room for the new element, and that the element is not already present. Its postcondition, which states that the table object’s contents consist of the old elements together with the new one.
The removal operation’s precondition, which states that the element is present, and its postcondition, which states that the table object’s contents consist of the old elements except for the one that has been removed. Note that the type invariant applies to the postcondition for both operations.
Syntax for Contracts
Ada 2012 supplies the relevant syntax for expressing such contracts, including universal and existential quantification and the ability for a postcondition to reference a formal parameter’s “old” value (its value on entry to the operation). The quantification forms would be used in the implementation of the various contract functions. The Boolean expressions are checked at run-time, if specified by the programmer—via the argument to an associated pragma. If checks are enabled and the condition fails, an exception is propagated to the caller of the operation.
The dynamic nature of the contract checks distinguished Ada 2012 from the SPARK language, which has been used in safety-critical and high-security contexts where formal demonstration of program properties is appropriate. SPARK is an Ada subset augmented with annotations for expressing a variety of program properties including preconditions, postconditions, and inter-module data information dependences. For SPARK, these contracts are enforced statically (before program execution) by a tool suite that helps check whether the “theorems” implied by the contracts can be proved based on the program text. The SPARK version of contract-based programming is known as Correctness by Construction.
Ada’s contract-based programming features complement the language’s Object-Oriented Programming support and help meet the guidance in DO-332, the Object-Oriented Technologies and Related Techniques supplement to DO-178C. This supplement introduced the concept of Local Type Consistency to address the issue of verification in the presence of inheritance and dynamically bound operations. Verification is simplified if inheritance is only used to implement class specialization relationships, but this imposes an important requirement on type substitutability: when an operation is overridden, its precondition should not be strengthened, and its postcondition should not be weakened. Ada’s contract syntax makes programs amenable to analysis—possibly by automated tools—that can check whether this requirement is met.
Safety and security are not properties that can be added “after the fact.” To have assurance that software is doing what it is supposed to, and not doing what it is not supposed to, the system needs to be designed from the start with attention paid to reliability and analyzability. An effective programming language will help, by avoiding features with error-prone syntax or semantics, and by making it easier to demonstrate properties such as freedom from run-time exceptions. The ability to define simple language subsets, thus facilitating certification, and to embed contracts in the program text, thus making requirements explicit, are likewise important. The Ada language, and most notably its latest revision Ada 2012, has met these requirements in a standard way.
Although Ada 2012 is new, implementations are already available. One example is AdaCore’s GNAT Pro development environment, which includes comprehensive support for the new language and in particular its contract-based programming features. These features are attracting attention and seeing usage in practice, in particular in the Hi-Lite research project. Hi-Lite is developing a new verification strategy combining formal proofs and testing, and Ada 2012’s contract-based programming features are serving as the foundation.
New York, NY.