Tokeneer Discovery - A SPARK Tutorial

This tutorial provides an introduction to the SPARK programming language and Toolset for engineering high-assurance software using the source code from the Tokeneer Project. It contains a series of lessons that demonstrates key features of the language and Toolset, illustrating why SPARK is superior to other standard imperative languages for building high-assurance software. SPARK also prevents the occurrence of a number of the top twenty-five most dangerous programming errors.

SPARK in a Nutshell

SPARK is a programming language, a set of source code analysis (static verification) tools, and a design method for developing high-assurance software.

The SPARK language is a strict subset of Ada augmented with a system of contracts (also known as annotations). The subset removes all ambiguities and undefined behaviour from the Ada language. The presence of contracts differentiates SPARK from other standard imperative programming languages such as C and C++.

For compilation, all SPARK programs can be compiled by any standard Ada compiler.

The static analysis capabilities of the SPARK Toolset are comprehensive. Key characteristics of the SPARK language and Toolset are listed below.

Sound
The analysis will tell you that the code is correct only if it really is - that is, no false negatives. Put another way, for large classes of programming errors, the SPARK Toolset can assert "there are no bugs", rather than the somewhat more flimsy "I can’t find any more bugs" offered by weaker languages and tools.
Low false alarm rate
SPARK raises very few false alarms, especially compared to static analysis tools for other programming languages, owing to the inherent simplicity and precision of SPARK.
Depth
SPARK analysis can verify complex and subtle properties of your code, such as application-specific safety and security properties - not just a predefined list of common errors.
Fast
The Toolset can be used interactively during development - it’s designed to be faster and more thorough than compiling and testing.
Modular
Developers have the flexibility to run the analysis during development with incomplete programs. There’s no need to analyse "the whole program" to get useful results.

The analysis tools can detect and mitigate against dangerous programming errors such as improper input validation, integer overflow or wraparound, buffer overflow errors, improper initialization, improper validation of array index, and information leak (follow the provided links to find the CWE/SANS experts’ descriptions of the errors and coping strategies). Examples of how SPARK tackles each of these problems are included later in this tutorial.

SPARK is best suited for embedded systems in sectors that rely on integrity of software systems including aerospace, security, banking, defence, rail, nuclear, transport and utilities where the cost of any failure ranges from loss of customer confidence to loss of life or national security. Projects using SPARK have also met or exceeded all relevant standards and guidance for high-assurance software at the highest integrity levels.

This tutorial provides a tour of SPARK and contains a series of lessons for you to trial the language and the tools. The lessons demonstrate key features of the SPARK language and how the SPARK Toolset can verify that a SPARK program is free from certain classes of errors.

Tokeneer in a Nutshell

Tokeneer was a successful research project carried out by Altran Praxis and funded by the National Security Agency (NSA) to develop part of an existing secure system (the Tokeneer System) to investigate SPARK’s capabilities to develop high quality and low defect software. Verification using the SPARK Toolset was undertaken at every stage of the development process to guard against errors being introduced.

This development and research work has now been made available by the NSA to the software development and security communities.

What is Special About SPARK Contracts?

Contracts are at the heart of SPARK program design. It is highly recommended to read the section What is Special About SPARK Contracts? before doing the lessons in this tutorial.