Developing secure code using SPARK: Part 2 – How to use it - Embedded.com

Developing secure code using SPARK: Part 2 – How to use it

In Part 1 of this two-part series, we summarized the basic issues with software security and explained how the programming language choice can affect the ease or difficulty of demonstrating that a system meets security requirements such as those defined in the Common Criteria. General purpose languages including C, C++, Ada, and Java are too complex to satisfy the reliability and analyzability requirements at the highest security levels; subsetting is needed. In this second part in the series one such language subset—SPARK*— is described and how it can be used to develop high-security systems cost-effectively.

SPARK1 is based on the principle of Correctness by Construction, an efficient and mathematically rigorous approach to software development that avoids defects, or detects and removes them quickly. Correctness by Construction involves strong static verification as the system is being implemented and allows the cumulative development of certification-oriented evidence.

SPARK is an Ada subset augmented with a notation for specifying contracts (annotations in the form of Ada comments) that are analyzed statically. The current version of SPARK is based on Ada 2005 and includes a large portion of Ada’s static semantic facilities such as packages/ encapsulation, subprograms, most types, and some Object-Oriented Programming features, as well as the Ravenscar tasking profile.2 Features such as exceptions, goto statements, and dynamic binding are excluded because they would complicate formal verification; other features such as access types (pointers ), dynamically sized arrays, and recursion are excluded because they would interfere with time or space predictability. Upcoming versions of the SPARK language and toolset are adding support for generic templates.
 
Despite the restrictions, large real-world applications can be (and have been) programmed in SPARK. Because of the restrictions, developers can rigorously demonstrate security-related properties such as freedom from run-time exceptions, absence of variables that are read before being assigned, and, for a multi-tasking application, absence of variables that are shared but unprotected.

The behavior of every SPARK program is unambiguous; in cases in which the Ada rules offer implementation flexibility, the choice will have no bearing on the program’s effect. Ada does not dictate the order of evaluation in expressions, for example, and in some cases the value may depend on the order chosen. The SPARK rules prevent functions from having side effects, however, so even though different evaluation orders are permitted, the end result will be the same.

SPARK contracts fall into two categories: core annotations and proof annotations. The core annotations relate to data flow and information flow, and inter-module dependences; for example, which global variables are referenced by a subprogram, and how the values of a procedure’s “out” or “in out” parameters are derived.

The proof annotations are optional and may be used for mathematically proving various dynamic properties of the program, such as a subprogram’s pre- and postconditions. In the most general scenario, a proof can demonstrate compliance of the program with respect to its formal specification as expressed in a language such as Z.3

SPARK can help achieve high assurance even without such a formal specification, however; the ability to prove that an exception will not be raised at run time—for example no stack overflow or array bounds violation—is by itself a major advance.

A SPARK example4 of a linear search procedure that updates a counter each time a match is found illustrates both kinds of annotations:
 
package Search
  –# own Counter;
  –# initializes Counter;

is
  Counter : Natural := 0;

  type IntArray is array (Integer range <>) of Integer;

  procedure Linear_Search
    (Table : in IntArray;
     Value : in Integer;
     Found : out Boolean;
     Index : out Integer);
  –# global in out Counter;
  –# derives Counter      from Counter, Table, Value &
  –#         Found, Index from Table, Value;
  –# pre  Counter < Integer'Last;
  –# post Found -> (Table(Index) = Value and
                    Counter = Counter~ + 1);

end Search;

package body
Search is

  procedure Linear_Search
    (Table : in IntArray;
     Value : in Integer;
     Found : out Boolean;
     Index : out Integer) is
  begin
     Found := False;
     Index := 0;

     for I in Integer range Table'Range loop
        –# assert Found = False and Counter < Integer'Last
        –#        and Counter = Counter~;

        if Table(I) = Value then
           Counter := Counter + 1;
           Found := True;
           Index := I;
           exit;
        end if;
     end loop;

  end Linear_Search;

end Search;

This example shows several core annotations:

  • The own and initializes annotations in the package specification, which identify a state variable and confirm that it is initialized;
  • The global annotation for the procedure specification, which indicates the intent to both reference and assign to the global variable; and
  • The derives annotation for the procedure specification, which documents the information flow dependences among the formal parameters and global variable.

The proof annotations are the procedure’s pre and post annotations, and the loop invariant assert annotation. The “->” symbol represents logical implication; thus “Found -> …” means “if Found then …”. A variable with an appended tilde (Counter ~ in this example) means the value of the variable on entry to the procedure. For simplicity, the state variable Counter is declared in the visible part of the package specification, analogous to public in C++ and Java; encapsulating it in the package body would be better style. A more complete discussion of a similar example appears in AdaCore’s Ada Gems 685 and 696 .

*The SPARK programming language is not sponsored by or affiliated with SPARC International Inc. and is not based on the SPARC architecture. Since SPARK is an Ada subset, with annotations in the form of comments, a SPARK program can be compiled by any standard Ada compiler. Before compilation, however, the program is analyzed by the Examiner and optionally other SPARK tools. The Examiner basically verifies consistency between the source code and the contracts; this involves several kinds of analysis, some of which are performed unconditionally:

• Syntactic analysis, checking that the program complies with the SPARK language restrictions and that the annotations are well-formed;

• Static semantic analysis, including the detection of aliasing (for example the use of the same variable as a global variable and an actual parameter) and function side effects;

• Data-flow analysis, including the detection of unused or uninitialized variables.

The Examiner can also optionally perform other kinds of analysis:

• Information-flow analysis—for example, checking the dependences between input and output variables;

• Verification condition (VC) generation: the generation of “theorems” that are implied by the pre and post-conditions in the context of the SPARK source code.

Proving the VCs is the job of a SPARK tool known as the Simplifier. For VCs that the Simplifier cannot prove, another SPARK tool—an interactive proof assistant known as the Checker—is available, but in most cases the Simplifier is sufficient. As a management aid, the POGS tool (Proof ObliGation Summarizer) collates and provides status information for each VC in the program.

If a VC cannot be proved, then the most likely cause is either a program bug or a missing or incorrect annotation. SPARK’s early diagnosis of this situation is key to preventing errors.

Tool practicalities
The purpose of a static analysis tool is to detect some particular class(es) of error, such as unreachable code, references to uninitialized variables, or deadlock. The tool thus has two general goals:

• Soundness: to detect all instances of the class; and
• Precision: to only report instances of the class.

Soundness implies the absence of false negatives. If a tool is not sound, then errors may slip through undetected. Precision implies no false positives (that is, no false alarms).

A tool with low precision is unusable if the developer has to inspect a large number of warnings to find the actual errors.

Unfortunately, soundness and precision conflict when the analysis is to be performed on the source code for any practical programming language, including SPARK. The designer of a static analysis tool thus has to make an appropriate tradeoff given the tool’s intended usage.

In the case of the Examiner, the decision is to ensure soundness; this is critical for a tool intended for use at the highest levels of security or safety. As a result, there will thus be occasional false alarms, but in practice these do not arise frequently enough to become an issue.

An additional real-world consideration is the ability of a static analysis tool to support modular, incremental development and to scale up to systems comprising millions of lines of code and written in multiple programming languages. The SPARK tools have been designed with these practicalities as guiding principles.

They can be applied to the SPARK modules of multi-language systems, which is important because typical systems contain components at different levels of security or safety criticality, and less critical components might not need the rigor of SPARK. The SPARK tools have been successfully used on very large projects across a range of application domains.

Formally verifying properties of the source program is useful, but it’s the compiled code that actually executes. That raises an important issue; compiler bugs, or platform security vulnerabilities that allow the compiled code to be tampered with, could mean that the running program is not equivalent to its source code. (The hardware, also, could be faulty, but that is a separate subject and outside the scope of this article. )

In theory, compiler issues could be addressed by formally verifying the code generator. That is not a practical solution, however. It is more realistic to take an approach similar to the DO-178B avionics safety standard.

Requirements-based tests are used to exercise the compiled code with sufficient depth to detect (and work around) faulty generated code, and, for software at the highest level of safety criticality, the developer needs to demonstrate the correctness of any generated code sequences that are not traceable to the source code. This approach has worked well in practice.

Risks related to interference from other applications on the same platform can be mitigated by choosing an architecture that implements time and space partitioning. Examples are ARINC 6538 and MILS9.

Achieving trust
Many factors affect a system’s security. Often the weak link is the human element, and that can negate even the best technology. On the technical side, demonstrating that a system meets its requirements is insufficient if the requirements themselves are incomplete.

In addition, important decisions such as the strength of an encryption algorithm are independent of the programming language. Nevertheless, the chosen language(s) and tools can have a significant impact on both the development effort and the degree of confidence that the system’s security properties are met.

In an all-too-common scenario, developers attempt to reinforce their software through extensive testing and by performing static analysis on the existing code. To slightly paraphrase a famous quote by the late computer scientist Edsger Dijkstra, however, these can show the presence of vulnerabilities, but not their absence.

From SPARK’s perspective, such a state of affairs is not good enough. A rigorous, mathematically based approach is required, especially at the highest security levels. As noted in a study of source code security analysis tools10, SPARK is an example of a language that is “by design, more suitable for secure programming” than C, C++, and Java, and that will “entirely preclude many common weaknesses or expose others. “

The SPARK language and its accompanying Correctness by Construction methods and supporting toolset have been successfully used on a number of high-security (as well as safety-critical) systems. As these experiences have shown, constructing reliable, safe, and secure software can be accomplished in a cost-effective manner, and without requiring the developers to be experts in formal logic. No programming language can guarantee secure software, but choosing a language that is part of the solution and not part of the problem is a good first step.

References
1. J.G.P. Barnes. High Integrity Software—The SPARK Approach to Safety and Security, Addison-Wesley (2003).
2. 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).
3. J.M. Spivey. The Z Notation: A Reference Manual, 2nd Edition, Prentice-Hall (1985).
4. Y. Moy. SPARK Code Sample: Linear Search.
5. Y.Moy. Ada Gem #68: Let’s SPARK!—Part 1 (June 2009).
6. Y.Moy. Ada Gem #69: Let’s SPARK!—Part 2 (September 2009).
7. RTCA SC-167 / EUROCAE WG-12. RTCA/DO-178B—Software Considerations in Airborne Systems and Equipment Certification (December 1992).
8. ARINC 653 Avionics Application Software Standard Interface, Part 1, Required Services (P1-3) and Part 2 – Extended Services (P2-1).
9. W. Vanfleet, J. Luke, et al., “MILS:Architecture for High-Assurance Embedded Computing,” CrossTalk (August 2005).
10. P.E. Black, M. Kass, M. Koo, E. Fong. Source Code Security Analysis Tool Functional Specification Version 1.1; NIST Special Publication 500-268 v1.1 (February 2011).

SPARK has been successfully used in a number of high-security systems. Here is a brief sampling:

Tokeneer
The Tokeneer ID Station project1 was sponsored by the U.S. National Security Agency (NSA) to investigate whether SPARK and the Correctness by Construction methods could be used in practice to develop a system that would meet EAL5 from the Common Criteria.

The effort involved requirements analysis, formal specification (in Z), design (formal refinement of the specification), implementation in SPARK, verification through the SPARK toolset, and top-down testing. A team from Praxis High-Integrity Systems, now Altran Praxis, successfully completed the project on schedule and within budget, at a level of effort that was much less than is typically required for high-integrity software.

Since the delivery of the system, only four minor defects in the ten thousand lines of SPARK code have been reported. The proof activity that was used could be applied at EAL7. All of the project material—requirements, specification, source code, tests, etc.—has been made available by NSA and may be downloaded .

SPARKSkein
Skein is a cryptographic hash function, with a reference implementation in C, that has been entered in the U.S. National Institute of Standards and Technology (NIST) competition for the new Secure Hash Algorithm (SHA-3) standard. Such hash functions are used to compute short digests of long messages and are one of the key building blocks of digital communication and cryptographic systems.

SPARKSkein2 is a SPARK implementation of the Skein algorithm. It was developed jointly by Altran Praxis and AdaCore with the goals of readability, portability (across machines of any word size and endianness, with no pre-processing required), performance, and formal demonstration of freedom from run-time errors. These objectives were met, showing that the use of rigorous methods to achieve correctness did not have to compromise portability or efficiency. In fact, developing the SPARK version uncovered an integer overflow problem in the C reference implementation. SPARKSkein is available through the Skein website. http://www.skein-hash.info/

Further References
1. J. E. Barnes, R. Chapman, R. Johnson, J. Widmaier, D. Cooper, B. Everett. “Engineering the Tokeneer Enclave Protection Software,” 1st IEEE International Symposium on Secure Software Engineering; (March 2006).
2. R. Chapman, E. Botcazou, and A. Wallenburg. “SPARKSkein: A Formal and Fast Reference Implementation of Skein,” in Proc. of the 14th Brazilian Symposium on Formal Methods; Sao Paulo, Brazil (September 2011).

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 previously published on the EETimes DesignLines)

Leave a Reply

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