Need Secure Software?
Security in modern embedded systems is critical-- software developers must keep ahead of the “bad guys”. A key decision is the choice of programming language: while some languages make it easier to produce secure code, others seem to exacerbate rather than solve the problem. This article identifies the key requirements that a programming language must satisfy, and shows how Ada effectively meets these demands.
Common Criteria
The ground rules for developers of systems with security requirements are laid down in the “Common Criteria”, an international standard that identifies three principal artifacts:
1) The Protection Profile (PP) specifies implementation-independent security functional requirements (such as privacy protection) and also security assurance requirements (such as vulnerability assessment). These requirements are organized into “packages” known as Evaluation Assurance Levels (EALs), ranging from confidence level 1 (lowest) to 7.
2) The Security Target (ST) is an implementation-dependent design against a specific PP. It specifies security mechanisms that meet the PP’s requirements and is the basis for the development of the Target of Evaluation.
3) The Target of Evaluation (TOE) is a vendor’s implementation of an ST, and is what actually gets evaluated.
Programming Language Implications
The Common Criteria standard does not provide explicit guidance on the choice of programming language. However, since an EAL captures a specific set of security assurance requirements we can deduce some general properties that the language must display.
EAL 5: “Semiformally designed and tested”
EAL 6: “Semiformally verified design and tested”
EAL 7: “Formally verified design and tested”
Both semiformal and formal require a “restricted syntax language with defined semantics”; the difference is that “formal” requires a mathematical basis.
A language that is used to implement TOEs at levels 5 and higher needs to satisfy four general requirements, similar to those for safety-critical systems:
• Application Reliability
The language should support good principles of software engineering, free of “traps and pitfalls”.
• Program Predictability
The language semantics should be well defined and should facilitate static prediction that space constraints will be met.
• Program Analysability
Depending on the EAL, TOE certification requires evidence of system properties that can be demonstrated from various analyses.
High-security embedded systems will have real-time constraints and will need to deal with hardware interrupts and other low-level issues.
There are tradeoffs among these requirements. Features that make a language expressive can make programs harder to analyse. Features that can help make software maintainable, such as Object-Oriented Programming, are problematic because of their dynamic nature.
No widely-used programming language in its entirety can meet the four requirements described above: it is necessary to use a subset.
The Ada Approach
Ada has long been a major player in the domain of safety-critical systems and the language issues for high-security systems are similar. Ada helps to meet the requirements mentioned above, and its flexible approach towards subsetting allows developers to tailor the language to specific security requirements.
Reliability
Ada was designed from the start to support sound software engineering techniques and to promote program reliability. For example, the notorious “buffer overflow” problem in C and C++ does not arise in Ada. It will be prevented by a run-time check that raises an exception (thus allowing controlled recovery), and in addition many range errors leading to buffer overflows are prevented by the strong typing. Also Type errors are caught at compile time, when they are less expensive to correct. Another benefit ADA offers is that the syntax for numeric literals is clear.
Predictability
The Ada language semantics are precisely defined in an international standard, and a program’s behavior is in general well defined and predictable. In cases where the meaning of a construct is not completely specified, the use of a carefully specified subset such as SPARK can eliminate any ambiguity and ensure a predictable effect.
Analysability
A variety of Ada features directly support analysability. For example, scalar data may be declared with explicit ranges, aiding readability and facilitating range analysis. This is one of the most significant differentiators between Ada and languages such as C, C++ and Java. Moreover, parameter passing in Ada specifies the parameter modes based on the direction of data flow, thus in, out, or in out. This facilitates information flow analysis.
However, features can also introduce complexity that interferes with analysability. Object Oriented Programming (OOP) is a notable example: the flexibility and dynamic nature of OOP is exactly the opposite of what is needed for static analysis. A study on the use of Ada in high-integrity systems showed that the set of features that should be used depends on the critically level (or EAL for high-security systems). Thus a developer requiring a particular analysis technique can go to and identify whether or not a particular feature is permitted.
Expressibility
Ada has a number of features that may be particularly useful in high- security systems, such as concurrency. Ada has a high-level model (“tasking”) that supports structured concurrent programming. Security functions are sometimes best mapped to individual threads of control, and Ada’s tasks are an excellent match. By comparison C and C++ lack this facility entirely, and Java’s thread model is low level and error prone. Ada is also one of only a few languages to provide direct support for fixed point data (both binary and decimal).
Ada has specific features that help support the development of safety-critical or high-security systems. One example is a compiler directive, pragma Normalise_Scalars, that directs the compiler to use, if possible, an invalid value as the default initialisation for scalar objects.
Subsettability
The Ada design anticipated the need for developers to be able to use less than the full language. The mechanism for realising this facility is a compiler directive, pragma Restrictions, with arguments identifying the specific features to be excluded. A higher-level directive, pragma Profile, is a collection of Restrictions pragmas. The language is carefully designed so that individual features can be removed leaving a complete and usable result.
There is no such thing as the high-integrity subset of Ada. Developers can define their own subsets based on the expressibility desired and the analysis techniques they plan to use. In practice, one particular high-integrity Ada subset deserves special note, the SPARK language. SPARK is an Ada subset augmented with special annotations that identify various program properties such as pre-conditions, post-conditions, and information dependencies.