Gem #51: Safe and Secure Software: Chapter 11, Certified Safe with SPARK

by John Barnes

Let's get started…

For some applications, especially those that are safety-critical or security-critical, it is essential that the program be correct, and that correctness be established rigorously through some formal procedure. For the most severe safety-critical applications the consequence of an error can be loss of life or damage to the environment. Similarly, for the most severe security-critical applications the consequence of an error may be equally catastrophic such as loss of national security, commercial reputation or just plain theft.

Applications are graded into different levels according to the risk. For avionics applications the DO-178B standard [1] defines the following:

level E none: no problem; e.g. entertainment system fails? – could be a benefit!
level D minor: some inconvenience; e.g. automatic lavatory system fails.
level C major: some injuries; e.g. bumpy landing, cuts and bruises.
level B hazardous; some dead; e.g. nasty landing with fire.
level A catastrophic; aircraft crashes, all dead; e.g. control system fails.

As an aside, note that although a failure of the entertainment system in general is level E, if the failure is such that the pilot is unable to switch it off (perhaps in order to announce something unpleasant) then that failure is at level D.

For the most demanding applications, which require certification by an appropriate authority, it is not enough for a program to be correct. The program also has to be shown to be correct and that is much more difficult.

This chapter gives a very brief introduction to SPARK. This is a language based on a subset of Ada which was specifically designed for the writing of high integrity systems. Although technically just a subset of Ada with additional information provided through Ada comments, it is helpful to consider SPARK as a language in its own right which, for convenience, uses a standard Ada compiler, but which is amenable to a more formal treatment than the full Ada language. Analysis of a SPARK program is carried out by a suite of tools of which the most important are the Examiner, Simplifier, and Proof Checker.

We start by considering the important concept of correctness and contracts.

Read Chapter 11 in full

Note: All chapters of this booklet will, in time, be available on the Ada 2005 home page.