Developing secure code using SPARK (Part 2)

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