Introduction
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.
What is Special About SPARK Contracts?
The following simple example shows why contracts are so special to the SPARK language. Let’s examine the following Ada subprogram declaration for the procedure Inc.
procedure Inc (X : in out Integer);
The declaration says very little. It only tells us that the procedure has a single in and out parameter X of type Integer – that is, the value may be read and may be updated. There is no way to determine what effect, if any, the subprogram has on parameter X or any other global variables (variables that are in-scope). Nothing can be inferred from the name of the procedure. The procedure could add or subtract one, a hundred or any other integer value to the variable X, do nothing at all, or update any global variable without contradicting the procedure’s declaration.
SPARK contracts provide the mechanism to specify properties about subprograms (procedures and functions).
Let’s first specify that the procedure reads and updates the global variable CallCount to record the number of times this procedure is called, and that no other global variables are read or updated. In SPARK, contracts are expressed with the prefix ––#
.
procedure Inc (X : in out Integer);
––# global in out CallCount;
The contract above specifies that the formal parameter X and global variable CallCount must be read by at least one path and must be updated by at least one path through the procedure.
SPARK static analysis will report an error if the implementation of the procedure:
- does not read the variable CallCount on at least one path through the procedure; or
- does not write to the variable CallCount on at least one path through the procedure; or
- reads or updates any other global variables; or
- does not read the variable X on at least one path through the procedure; or
- does not write to the variable X on at least one path through the procedure.
SPARK contracts can specify, using postconditions, even more about the effects on the parameter X and global variable CallCount – see code below.
procedure Inc (X : in out Integer); ––# global in out CallCount; ––# post X = X~ + 1 and ––# CallCount = CallCount~+ 1;
The postconditions specify that both variables are incremented by one. In SPARK, X~ refers to the initial value of X – similarly for CallCount. This is a far more precise statement about the procedure than what we initially started with. The SPARK Toolset will raise an error if the implementation contradicts the procedure’s contract.
Contracts can also specify preconditions to express properties that must hold when the subprogram is called. The code below specifies the condition that both variables must be less than Integer'Last. The purpose of adding this precondition is to prevent integer overflow errors. The SPARK Toolset, during source code analysis, will attempt to verify that all calls to this procedure satisfy this precondition.
procedure Inc (X : in out Integer); ––# global in out CallCount; ––# pre X < Integer'Last and ––# CallCount < Integer'Last; ––# post X = X~ + 1 and ––# CallCount = CallCount~ + 1;
This brief introduction gives an insight into the precision at which we can specify program behaviours through contracts. This ability distinguishes SPARK from other standard programming languages.
The remainder of this tutorial contains a series of lessons using the Tokeneer source code to demonstrate key capabilities of the SPARK Toolset and why SPARK is ideally suited for high-assurance software. The lessons show why the SPARK Toolset can verify that a SPARK program is free from certain classes of common and potentially dangerous errors.
Preamble
This tutorial can be read as a stand-alone document. You may also choose to follow this tutorial by running and experimenting with SPARK. If so, you will need to have the SPARK tools installed. To install the SPARK tools follow the instructions on the installation page.
The step-by-step instructions in this tutorial are written so that they can be followed by SPARK users with different editing preferences. You can either choose the combination of your favourite editor plus command-line versions of the SPARK tools, or you can choose to run the integrated development environment GPS with the SPARK plugin (how to start GPS and open the Tokeneer project).
Lesson 1
Dealing with Improper Initialization
If you don’t properly initialize your data and variables, an attacker might be able to do the initialization for you, or extract sensitive information that remains from previous sessions. When those variables are used in security-critical operations, such as making an authentication decision, then they could be modified to bypass your security. Incorrect initialization can occur anywhere, but it is probably most prevalent in rarely-encountered conditions that cause your code to inadvertently skip initialization, such as obscure errors.
Improper initialization errors is listed as one of the top most dangerous programming errors. How would you find those? How much would your compiler help?
The SPARK Toolset identifies all variables that have not been initialized prior to them being read. And – if the SPARK automatic source code analysis finds no uninitialized variables then there really are none!
In this lesson, we will first inject a couple of initialization errors into some of the Tokeneer code and then show how you can use the SPARK tools to find those errors.
Step-by-Step Instructions
Let us start by first running the Examiner, one of the SPARK tools, on some of the Tokeneer code in the correct version. Then we will inject an uninitialized variable error to the same code and see how the Examiner’s data flow analysis finds it for us.
Step 1: Run the Examiner on the Correct Version of the Code
The code below is from the procedure GetStartAndEndTimeFromFile in auditlog.adb.
264 procedure GetStartAndEndTimeFromFile 265 (TheFile : in out File.T; 266 Description : out AuditTypes.DescriptionT) 267 ––# global in out AuditSystemFault; 268 ––# derives AuditSystemFault, 269 ––# TheFile from *, 270 ––# TheFile & 271 ––# Description from TheFile; 272 is 273 OK : Boolean; 274 FirstTime : Clock.TimeTextT; 275 LastTime : Clock.TimeTextT; 276 TimeCount : Natural; -- type Natural to match formal parameter 277 -- in call to GetString 278 TimeOK : Boolean := True; 279 ... 311 ------------------------------------------------------------------- 312 -- begin GetStartAndEndTimeFromFile 313 ------------------------------------------------------------------- 314 begin 315 316 FirstTime := Clock.PrintTime(Clock.ZeroTime); 317 LastTime := Clock.PrintTime(Clock.ZeroTime); ... 358 Description := ConvertTimesToText; 359 360 end GetStartAndEndTimeFromFile;
Run the Examiner (follow this link to find out how) for auditlog.adb and notice that it reports no errors.
Step 2: Inject an Initialization Error and Find It Using the Examiner
Let’s introduce two types of uninitialized variables into the code – variables that are never initialized and variables that may not be initialized.
Lines 316 and 317 initialize the variables FirstTime and LastTime. Put these two lines of code inside an if statement so that the variables are only initialized if the variable OK is true. The modified code is shown below.
316 if OK then 317 FirstTime := Clock.PrintTime(Clock.ZeroTime); 318 LastTime := Clock.PrintTime(Clock.ZeroTime); 319 end if;
The changes introduce a number of improper initialization errors:
- The variable OK is not initialized before it is read;
- The variables FirstTime and LastTime may not be initialized;
- The uninitialized variables FirstTime, LastTime and OK may then influence the expression that assigns a value to the variable Description – the variable OK is indirectly used in the expression.
Re-run the Examiner and notice that the Examiner identifies all uninitialized variables as errors (follow this link to see the reported errors) and it differentiates between variables that are not initialized and variables that may not be initialized.
Step 3: Find an Array Index Initialization Error
Another common error is accessing an array element with an uninitialized variable as the index. In this example we will inject such an error and demonstrate that the Examiner also finds these errors.
Start with a fresh copy of the file auditlog.adb by copying the file auditlog_copy.adb in tokeneer/code/core to auditlog.adb in the same directory. The code below is from the procedure DeleteLogFile in auditlog.adb.
512 procedure DeleteLogFile ( Index : LogFileIndexT) 513 ––# global in out AuditSystemFault; 514 ––# in out LogFiles; 515 ––# in out LogFilesStatus; 516 ––# in out LogFileEntries; 517 ––# derives AuditSystemFault, 518 ––# LogFiles from *, 519 ––# LogFiles, 520 ––# Index & 521 ––# LogFilesStatus, 522 ––# LogFileEntries from *, 523 ––# Index; 524 is 525 OK : Boolean; 526 TheFile : File.T; 527 begin 528 529 TheFile := LogFiles (Index); ... 543 end DeleteLogFile;
Line 529 of the code accesses the Indexth element of the array LogFiles.
Declare a new variable I of type LogFileIndexT and replace, on line 529, Index with I. The modified code is shown below.
512 procedure DeleteLogFile ( Index : LogFileIndexT) ... 524 is 525 OK : Boolean; 526 TheFile : File.T; 527 I : LogFileIndexT; 528 begin 529 530 TheFile := LogFiles (I);
Examine the file auditlog.adb and notice that it reports that the variable I has not been initialized.
Summary
We have seen that the the SPARK tools can verify that a SPARK program is free from improper input validation errors. In the next lesson, we will study how SPARK handles a related class of errors – Identifying Ineffective Statements.
Lesson 2
Identifying Ineffective Statements
Every statement should have a purpose. An ineffective statement has no effect on any output variable and therefore has no effect on the behaviour of the code. The presence of ineffective statements reduces the quality and the maintainabiliy of the code. The SPARK Toolset identifies all ineffective statements.
In this lesson, we will show how the SPARK Toolset finds ineffective statements to ensure that SPARK programs are free from them.
Step-by-Step Instructions
We will inject an ineffective statement into the Tokeneer code and use the Examiner to find it.
Step 1: Inject an Ineffective Statement
Start with a fresh copy of the file auditlog.adb by copying the file auditlog_copy.adb in tokeneer/code/core to auditlog.adb in the same directory.
Let us inject an ineffective statement into the implementation of the function NextListIndex (shown below) in auditlog.adb.
189 function NextListIndex(Value : LogFileIndexT) return LogFileIndexT 190 is 191 Result : LogFileIndexT; 192 begin 193 if Value = LogFileIndexT'Last then 194 Result := LogFileIndexT'First; 195 else 196 Result := Value + 1; 197 end if; 198 return Result; 199 end NextListIndex;
Modify the above code by adding the new variable Result_Tmp of type LogFileTypeT (line 191) and change line 196 so that Value + 1 is assigned to the variable Result_Tmp instead of Result (see code below).
189 function NextListIndex(Value : LogFileIndexT) return LogFileIndexT 190 is 191 Result, Result_Tmp: LogFileIndexT; 192 begin 193 if Value = LogFileIndexT'Last then 194 Result := LogFileIndexT'First; 195 else 196 Result_Tmp := Value + 1; 197 end if; 198 return Result; 199 end NextListIndex;
The statement on line 196 is ineffective as Result_Tmp is never used. Furthermore, the value for Result may be undefined when Value /= LogFileIndexT'Last.
Step 2: See How the Examiner Finds the Problem
Re-run the Examiner for auditlog.adb and, as expected, it finds the ineffective statement as well as the possible undefined value for Result.
Summary
In this lesson we have seen an example of the SPARK tools finding an ineffective statement. The SPARK tools will find all ineffective statements. In the next lesson, we will study Input Validation.
Lesson 3
Validating Input
Input validation ensures that your program’s input conforms to expectations – for example, to ensure that the input has the right type. But validation requirements can be much more complicated than that. Incorrect input validation can lead to security and safety problems since many applications live in a “hostile” environment and the input might be constructed by an attacker. It’s the number one killer of healthy software…
according to the CWE/SANS list of the top twenty-five most dangerous programming errors.
For example, consider the following few lines of code from the original release of the Tokeneer code:
233 if Success and then 234 (RawDuration * 10 <= Integer(DurationT'Last) and 235 RawDuration * 10 >= Integer(DurationT'First)) then 236 Value := DurationT(RawDuration * 10); 237 else
This code has a check that the input RawDuration is in the right range before the value is updated – an example of so called defensive coding, according to the advice on mitigations from the software experts who compiled the list of dangerous programming errors. Can you see the problem with this code?
The SPARK tools will identify a serious defect in this code, which could impact on security.
In this lesson, the above code will be investigated using the SPARK tools. This lesson shows the challenges in ensuring the absence of input validation errors, and the benefits of using SPARK to do so.
Step-by-Step Instructions
First, we will familiarize ourselves with two more advanced SPARK tools by running them on the correct version of the code. Then we inject the defect shown above into the Tokeneer code, rerun the SPARK tools, and interpret the results.
Step 1: Analyse the Correct Version of the Code
Analyse Tokeneer using the following steps (details on the SPARK analysis steps):
- Run the Examiner on the file configdata.adb.
- Run the Simplifier, a more advanced tool in the SPARK tool suite, which tries to show the absence of certain run-time errors by theorem proving.
- Run POGS, which gives a summary of the verification just performed.
Now let us inspect the verification summary, which is written in file core.sum in the directory tokeneer/code/core. At the end of that file, an overall summary of the Tokeneer verification is given. It shows that there are no errors which is expected as we ran the tools on the correct version of the code. Furthermore, it shows a number of tables describing details for the verification. For example, lines 2750 to 2766 of core.sum, shown below, are the results from the analysis of the procedure ReadDuration.
2750 VCs for procedure_readduration : 2751 ---------------------------------------------------------------------------- 2752 | | | -----Proved In----- | | | 2753 # | From | To | vcg | siv | plg | prv | False | TO DO | 2754 ---------------------------------------------------------------------------- 2755 1 | start | rtc check @ 220 | | YES | | | | | 2756 2 | start | rtc check @ 221 | | YES | | | | | 2757 3 | start | rtc check @ 221 | | YES | | | | | 2758 4 | start | rtc check @ 233 | | YES | | | | | 2759 5 | start | rtc check @ 237 | | YES | | | | | 2760 6 | start | rtc check @ 243 | | YES | | | | | 2761 7 | start | rtc check @ 243 | | YES | | | | | 2762 8 | start | assert @ finish | YES | | | | | | 2763 9 | start | assert @ finish | YES | | | | | | 2764 10 | start | assert @ finish | YES | | | | | | 2765 11 | start | assert @ finish | YES | | | | | | 2766 ----------------------------------------------------------------------------
Note that the columns False and TO DO are empty, which means that the SPARK tools found no errors in the verification of procedure ReadDuration.
Step 2: Inject Erroneous Input Validation Code
Now, replace lines 234 and 235 in the file configdata.adb with the erroneous code:
233 if Success and then 234 (RawDuration * 10 <= Integer(DurationT'Last) and 235 RawDuration * 10 >= Integer(DurationT'First)) then 236 Value := DurationT(RawDuration * 10); 237 else
Essentially this code concerns the validation of an input – an integer value RawDuration – that is read from a file, and is expected to be in the range 0..200 seconds before it is converted into a number of tenths of seconds in the range 0..2000.
Step 3: Re-Analyse the Faulty Code
Re-analyse Tokeneer.
The results from the analysis of the procedure ReadDuration in the summary file core.sum is shown below.
2750 VCs for procedure_readduration :
2751 ----------------------------------------------------------------------------
2752 | | | -----Proved In----- | | |
2753 # | From | To | vcg | siv | plg | prv | False | TO DO |
2754 ----------------------------------------------------------------------------
2755 1 | start | rtc check @ 220 | | YES | | | | |
2756 2 | start | rtc check @ 221 | | YES | | | | |
2757 3 | start | rtc check @ 221 | | YES | | | | |
2758 4 | start | rtc check @ 233 | | | | | | YES |
2759 5 | start | rtc check @ 237 | | YES | | | | |
2760 6 | start | rtc check @ 243 | | YES | | | | |
2761 7 | start | rtc check @ 243 | | YES | | | | |
2762 8 | start | assert @ finish | YES | | | | | |
2763 9 | start | assert @ finish | YES | | | | | |
2764 10 | start | assert @ finish | YES | | | | | |
2765 11 | start | assert @ finish | YES | | | | | |
2766 ----------------------------------------------------------------------------
Notice that this time there is one YES in the TO DO column. The SPARK Toolset has detected a potential problem with the procedure ReadDuration.
Step 4: Investigate the Verification Output
Now, let us have look into what the error that the SPARK tools have found really means.
The file readduration.siv contains the Simplifier’s analysis of the procedure. Lines 38 to 55 (shown below) of the file show the potential problem the SPARK Toolset has identified. The Simplifier, on line 54, is trying to check no arithmetic overflow errors will occur when evaluating the expression RawDuration * 10 – that is, when Success is True then RawDuration * 10 >= -2147483648 (Integer'First) and RawDuration * 10 <= 2147483648 (Integer'Last).
38 procedure_readduration_4. 39 H1: rawduration__1 >= - 2147483648 . 40 H2: rawduration__1 <= 2147483647 . ... 52 -> 53 C1: success__1 -> rawduration__1 * 10 >= - 2147483648 and rawduration__1 * 54 10 <= 2147483647 . 55
Here the SPARK theorem prover is trying to prove that RawDuration times 10 (note that rawduration__1 * 10 is a mathematical multiplication, as opposed to a computation) is within the limits of Integer, assuming only that it was within the limits before it was multiplied by 10. This should not be possible to prove. Think about a scenario where Tokeneer was given an input floppy disk where RawDuration was set to 1000000000. Both the assumptions H1 and H2 would be true, but C1 - the conclusion - would be false!
This is a serious defect since a malicious user holding the "security officer" role can deliberately attack the system by supplying a file that contains a malformed configuration data file - one that contains a value for RawDuration that is greater than Integer'Last/10.
Summary
In SPARK, developers need to be explicit about the intended input and output of program components. This has the benefit of the SPARK tools being able to automatically find defects that are hard to prevent, hard to detect, and with important security consequences. In this lesson we have seen this exemplified with input validation. Next, we will look into SPARK Contracts.
Lesson 4
SPARK Contracts
This lesson extends What is Special About SPARK Contracts to show how the SPARK Toolset can verify application specific safety and security properties.
In this lesson, we will see how the SPARK tools detect any differences between a program’s intended behaviour, as specified in its contract, and its actual behaviour, as implemented in the code. Thus the SPARK tools can be used either to find defects in the contract, to find defects in the implementation, to find defects in both, or to show conformance between intended and actual behaviour.
Step-by-Step Instructions
Step 1: Analyse the Correct Version of the Code
The precondition for the procedure AddElementToCurrentFile in auditlog.adb (lines 772 - 774 in the code below) specifies that the value stored in the CurrentLogFileth element of the array LogFileEntries is less than MaxLogFileEntries and the postcondition specifies that the array element is incremented by 1. The information-flow related contracts (derives annotation) will be dealt with in the lesson about information flow analysis.
751 procedure AddElementToCurrentFile 752 (ElementID : in AuditTypes.ElementT; 753 Severity : in AuditTypes.SeverityT; 754 User : in AuditTypes.UserTextT; 755 Description : in AuditTypes.DescriptionT) 756 ––# global in Clock.Now; 757 ––# in CurrentLogFile; 758 ––# in out AuditSystemFault; 759 ––# in out LogFiles; 760 ––# in out LogFileEntries; 761 ––# derives AuditSystemFault, 762 ––# LogFiles from *, 763 ––# Description, 764 ––# LogFiles, 765 ––# Clock.Now, 766 ––# ElementID, 767 ––# Severity, 768 ––# User, 769 ––# CurrentLogFile & 770 ––# LogFileEntries from *, 771 ––# CurrentLogFile; 772 ––# pre LogFileEntries(CurrentLogFile) < MaxLogFileEntries; 773 ––# post LogFileEntries(CurrentLogFile) = 774 ––# LogFileEntries˜(CurrentLogFile) + 1; 775 776 is 777 TheFile : File.T ; 778 begin 779 TheFile := LogFiles (CurrentLogFile); 780 AddElementToFile 781 (TheFile => TheFile, 782 ElementID => ElementID, 783 Severity => Severity, 784 User => User, 785 Description => Description); 786 LogFiles (CurrentLogFile) := TheFile; 787 788 LogFileEntries(CurrentLogFile) := LogFileEntries(CurrentLogFile) + 1; 789 end AddElementToCurrentFile;
Analyse Tokeneer with the SPARK Toolset. The result of the analysis is logged in core.sum and it shows (see below) that the SPARK Toolset has identified no problems with the code in the procedure AddElementToLogFile – the columns False and TO DO are empty.
659 VCs for procedure_addelementtocurrentfile : 660 ---------------------------------------------------------------------------- 661 | | | -----Proved In----- | | | 662 # | From | To | vcg | siv | plg | prv | False | TO DO | 663 ---------------------------------------------------------------------------- 664 1 | start | rtc check @ 781 | | YES | | | | | 665 2 | start | rtc check @ 782 | | YES | | | | | 666 3 | start | rtc check @ 788 | | YES | | | | | 667 4 | start | rtc check @ 790 | | YES | | | | | 668 5 | start | assert @ finish | | YES | | | | | 669 ----------------------------------------------------------------------------
Step 2: Change the Contract – But not the Implementation
Let us change the postcondition so the procedure’s contract no longer matches its implementation. The SPARK Toolset will then detect the inconsistency. Change the postcondition to specify that the array element LogFileEntries(CurrentLogFile) should be incremented by 10, the modified code is shown below.
772 ––# pre LogFileEntries(CurrentLogFile) < MaxLogFileEntries;
773 ––# post LogFileEntries(CurrentLogFile) =
774 ––# LogFileEntries˜(CurrentLogFile) + 10;
775
Step 3: Re-Analyse and Study the Results
Re-analyse Tokeneer and open the file core.sum. The results of the analysis for the procedure AddElementToLogFile has changed – the columns False and TO DO are no longer empty (see below).
SPARK Toolset has identified a potential problem with the code and the details are described in the file addelementtocurrentfile.siv (siv files are generated by the Simplifier to provide details of its analysis) in the directory tokeneer/code/core/auditlog/addelementtologfile. The problem is that the procedure’s contract and implementation don’t match.
659 VCs for procedure_addelementtocurrentfile :
660 ----------------------------------------------------------------------------
661 | | | -----Proved In----- | | |
662 # | From | To | vcg | siv | plg | prv | False | TO DO |
663 ----------------------------------------------------------------------------
664 1 | start | rtc check @ 781 | | YES | | | | |
665 2 | start | rtc check @ 782 | | YES | | | | |
666 3 | start | rtc check @ 788 | | YES | | | | |
667 4 | start | rtc check @ 790 | | YES | | | | |
668 5 | start | assert @ finish | | | | | YES | |
669 ----------------------------------------------------------------------------
Step 4: Revert the Contract – But Change the Implementation
Undo the changes to the postcondition and change line 788 so that the input value is preserved.
774 ––# pre LogFileEntries(CurrentLogFile) < MaxLogFileEntries;
775 ––# post LogFileEntries(CurrentLogFile) =
776 ––# LogFileEntries~(CurrentLogFile) + 1
...
791 LogFileEntries(CurrentLogFile) := LogFileEntries(CurrentLogFile) + 0;
792 end AddElementToCurrentFile;
Re-analyse Tokeneer and open the file core.sum. The analysis of the procedure is unchanged as the implementation, like previously, does not match the procedure’s contract.
Step 5: Strengthen the Contract
Revert the code to its original state.
In SPARK, we can strengthen the procedure’s contract and say more about the properties of the procedure. Let’s add extra code assigning the value in the first element of the array LogFileEntries to 10 if CurrentLogFile is not LogFileIndexType'First (lines 789 – 791 below).
788 LogFileEntries(CurrentLogFile) := LogFileEntries(CurrentLogFile) + 1; 789 if CurrentLogFile /= LogFileIndexType'First then 790 LogFileEntries(LogFileIndexType'First) := 10; 791 end if; 792 end AddElementToCurrentFile;
Re-analyse Tokeneer and open the file core.sum and notice that no errors are reported as the procedure’s implementation is not inconsistent with its contract. The post-condition says nothing about the effects of the procedure on any of the array elements except the one indexed by CurrentLogEntry.
We can strengthen the post-condition (lines 775 and 776 below) to specify that only the entry indexed by CurrentLogFile is incremented and all other elements remain unchanged.
772 ––# pre LogFileEntries(CurrentLogFile) < MaxLogFileEntries;
773 ––# post LogFileEntries = LogFileEntries~[CurrentLogFile => LogFileEntries~(CurrentLogFile)+1];
Re-analyse Tokeneer and open the file core.sum and notice, on lines 659 to 671, that the mismatch between the implementation and contract has been detected. The details of the problem are recorded in the file addelementtocurrentfile.siv in the directory tokeneer/code/core/auditlog/addelementtologfile.
657 VCs for procedure_addelementtocurrentfile :
658 ----------------------------------------------------------------------------
659 | | | -----Proved In----- | | |
660 # | From | To | vcg | siv | plg | prv | False | TO DO |
661 ----------------------------------------------------------------------------
662 1 | start | rtc check @ 783 | | YES | | | | |
663 2 | start | rtc check @ 784 | | YES | | | | |
664 3 | start | rtc check @ 790 | | YES | | | | |
665 4 | start | rtc check @ 792 | | YES | | | | |
666 5 | start | rtc check @ 794 | | YES | | | | |
667 6 | start | assert @ finish | | | | | | YES |
668 7 | start | assert @ finish | | YES | | | | |
669 ----------------------------------------------------------------------------
Summary
This lesson demonstrates that the more precise the specification, the more bugs the SPARK Toolset can detect. The use of the SPARK Toolset during development to verify code is, in our experience, more effective than compiling and testing, since the analysis is for all input data and not just a few specific test cases. Next, we will see how SPARK Deals with Overflow Errors.
Lesson 5
Dealing with Overflow Errors
An overflow error occurs when the capacity of a device is exceeded. Overflow errors are a source of quality and security concerns. For instance, when an arithmetic overflow occurs, a calculated value does not fit in its specified size, and the calculation (and the program) just stops. Buffer overflow happens when a process stores data in a buffer outside of the memory that the programmer set aside for it. Buffer overflow errors are widely known to present a vulnerability to malicious hackers, who might exploit the error to sneak their own code onto a victim’s disk, storing it outside of the intended buffer.
The SPARK tools detect all potential arithmetic and buffer overflow errors. In the lesson about input validation, we saw an example of an arithmetic overflow. In this lesson, we will study how the SPARK tools find a buffer overflow error that we have injected into the Tokeneer code.
Step-by-Step Instructions
We will introduce a buffer overflow error into auditlog.adb and show how the SPARK Toolset detects it.
Step 1: Inject a Buffer Overflow Error
Start with a fresh copy of the file auditlog.adb by copying the file auditlog_copy.adb in tokeneer/code/core to auditlog.adb.
The procedure AddElementToCurrentFile increments the element indexed by CurrentLogFile in the array LogFileEntries – see below.
775 ––# post LogFileEntries(CurrentLogFile) = 776 ––# LogFileEntries~(CurrentLogFile) + 1; ... 790 LogFileEntries(CurrentLogFile) := LogFileEntries(CurrentLogFile) + 1;
Change the code on line 790 and the postcondition on 775 to 776 so the procedure copies the value in the CurrentLogFile+1th element into the CurrentLogFileth element of the array. The modified code is shown below.
774 ––# pre LogFileEntries(CurrentLogFile) < MaxLogFileEntries; 775 ––# post LogFileEntries(CurrentLogFile) = 776 ––# LogFileEntries˜(CurrentLogFile+1); ... 790 LogFileEntries(CurrentLogFile) := LogFileEntries(CurrentLogFile+1) ;
Step 2: Analyse and Study the Verification Output
Analyse Tokeneer and open the file core.sum. The SPARK Toolset identifies, on lines 587 to 597 (see below), that there is a potential problem with the procedure AddElementToCurrentFile.
659 VCs for procedure_addelementtocurrentfile :
660 ----------------------------------------------------------------------------
661 | | | -----Proved In----- | | |
662 # | From | To | vcg | siv | plg | prv | False | TO DO |
663 ----------------------------------------------------------------------------
664 1 | start | rtc check @ 781 | | YES | | | | |
665 2 | start | rtc check @ 782 | | YES | | | | |
666 3 | start | rtc check @ 788 | | YES | | | | |
667 4 | start | rtc check @ 790 | | | | | | YES |
668 5 | start | assert @ finish | | YES | | | | |
669 ----------------------------------------------------------------------------
The details of the problem are described on line 79 in addelementtocurrentfile.siv. The Simplifier failed to show that CurrentLogFile+1 is always within range of the index type because it is not true – it goes outside its range when CurrentLogFile = LogFileIndexType'Last which then causes a buffer overflow.
Summary
Buffer overflow errors are common and present a security vulnerability. The SPARK Toolset can verify that a SPARK program is free from arithmetic as well as buffer overflow errors. In this lesson we have seen how the SPARK tools can be used to detect a buffer overflow error. In the next lesson, we will see how SPARK can be used in Ensuring Secure Information Flow.
Lesson 6
Ensuring Secure Information Flow
Error message information leak occurs when secure data is leaked, through error messages, to unauthorised users and is one of the top twenty-five most dangerous programming errors. The general problem is ensuring that information flow adheres to certain policies - for example, certain data should never be written in an error message to a log file that may be accessible by unauthorised users.
The objective of this lesson is to demonstrate that the Examiner detects information flow violations.
Step-by-Step Instructions
Step 1: Study a Contract from an Information Flow Perspective
The code below is from the procedure Verify in bio.adb. The out variable MatchResult returns the result of whether a person’s fingerprint matched their template. The local variable NumericReturn is set to the enumerated value BioApiOk if the fingerprint successfully matched; otherwise it returns an error code.
When a match is unsuccessful, a log record is written including the variable NumericReturn, which is derived from the person’s Template – see bio-interface.ads’s specification for the procedure Verify.
221 procedure Verify(Template : in IandATypes.TemplateT;
222 MaxFAR : in IandATypes.FarT;
223 MatchResult : out IandATypes.MatchResultT;
224 AchievedFAR : out IandATypes.FarT)
...
230 ––# derives AuditLog.State,
231 ––# AuditLog.FileState from AuditLog.State,
232 ––# AuditLog.FileState,
233 ––# Template,
234 ––# Clock.Now,
235 ––# ConfigData.State,
236 ––# Interface.Input &
...
242 is
243 NumericReturn : BasicTypes.Unsigned32T;
244 begin
245 Interface.Verify(Template => Template,
246 MaxFAR => MaxFAR,
247 MatchResult => MatchResult,
248 AchievedFAR => AchievedFAR,
249 BioReturn => NumericReturn);
250
251 if NumericReturn /= ValueOf(BioAPIOk) then
252 -- An error occurred, overwrite match information.
253 MatchResult := IandATypes.NoMatch;
254 AuditLog.AddElementToLog
255 (ElementID => AuditTypes.SystemFault,
256 Severity => AuditTypes.Warning,
257 User => AuditTypes.NoUser,
258 Description => MakeDescription ("Biometric device failure ",
259 NumericReturn));
260 end if;
261 end Verify;
If the log was accessible to potential hackers, which is not the case for Tokeneer, then this is an example of an error message information leak. Fingerprint templates should never be accessible by hackers.
Step 2: Change an Information Flow Aspect of the Contract
Change the contract for the procedure Verify to specify that no information written to the log is derived from Template by deleting line 233.
230 ––# derives AuditLog.State,
231 ––# AuditLog.FileState from AuditLog.State,
232 ––# AuditLog.FileState,
233 ––#
234 ––# Clock.Now,
235 ––# ConfigData.State,
236 ––# Interface.Input &
The corresponding line (line 73) of code needs to be removed from the file bio.ads.
60 procedure Verify(Template : in IandATypes.TemplateT;
61 MaxFAR : in IandATypes.FarT;
62 MatchResult : out IandATypes.MatchResultT;
63 AchievedFAR : out IandATypes.FarT);
...
69 ––# derives AuditLog.State,
70 ––# AuditLog.FileState from Input,
71 ––# AuditLog.State,
72 ––# AuditLog.FileState,
73 ––#
74 ––# Clock.Now,
75 ––# ConfigData.State &
Step 3: Use the SPARK Tools to Detect the Information Leak
Examine the file bio.adb and notice the Examiner reports the error that information derived from the variable Template is written to the log. This means that data derived from the template is being written to the log!
Step 4: Introduce a Malicious Hack
The Examiner also detects when data has been incorrectly used. The file bio_bad.adb contains a back door code in the procedure Verify (lines 248-251). It now returns a positive match independent of the user’s fingerprint when the clock is at midnight.
223 procedure Verify(Template : in IandATypes.TemplateT; 224 MaxFAR : in IandATypes.FarT; 225 MatchResult : out IandATypes.MatchResultT; 226 AchievedFAR : out IandATypes.FarT) ... 232 ––# derives AuditLog.State, 233 ––# AuditLog.FileState from AuditLog.State, 234 ––# AuditLog.FileState, 235 ––# Template, 236 ––# Clock.Now, 237 ––# ConfigData.State, 238 ––# Interface.Input & ... 244 is 245 NumericReturn : BasicTypes.Unsigned32T; 246 T : Clock.TimeT; 247 begin 248 T := Clock.GetNow; 249 if T = Clock.ZeroTime then 250 MatchResult := IandATypes.Match; 251 AchievedFAR := 0; 252 else 253 254 Interface.Verify(Template => Template, 255 MaxFAR => MaxFAR, 256 MatchResult => MatchResult, 257 AchievedFAR => AchievedFAR, 258 BioReturn => NumericReturn); 259 ... 272 end if; ... 275 end Verify;
Step 5: Use the SPARK Tools to Detect the Weakness
Examine the file bio_bad.adb and notice that the Examiner reports the error that MatchResult is dependent on the current time (Clock.now) which is inconsistent with the procedure’s contract. The Examiner has identified an information flow inconsistency due to the presence of the back-door.
Summary
In this lesson we have learnt about information flow contracts and we have seen the SPARK tools detect a malicious hack. SPARK programs are free from information leaks when the contract accurately specifies the desired information flow between variables.
Summary
This tutorial demonstrates the key capabilities of the SPARK and how it can verify SPARK programs are free from certain classes of bugs. A number of these are listed in the top twenty five most dangerous programming errors, including buffer overflow, input validation and uninitialized variables. SPARK is more suitable than other standard imperative programming languages such as C and C++ in engineering software for sectors that rely on the integrity of their software systems.
Finding More Information
Further information on SPARK and SPARK Pro can be obtained from the following sources.
- Purchase a copy of the book High Integrity Software The SPARK Approach to Safety and Security from Pearson.
- Introducing SPARK Pro (Webinar)
- SPARK Pro Website
- SPARK Training
- SPARK Engineering Services
- Supported Evaluation
Tools Installation
If you are a SPARK Pro customer, the tools can be downloaded from AdaCore’s website via GNAT Tracker. If you are a free software developer or an academic you can use the SPARK GPL toolset available on AdaCore’s Libre site. Visit the Tokeneer tools page for more information.
For GPS users, you need to also install the suitable GPS plug-in for SPARK.
-
For GPS 4.4.1, Replace the file
spark.pyin the directorygnatpro/share/gps/plug-ins/with the copy in the directorytokeneer/tools/plug_ins/gps4.4.1/. -
For GPS 4.3.1, Replace the file
spark.pyin the directorygnatpro/share/gps/plug-ins/with the copy in the directorytokeneer/tools/plug_ins/gps4.3.1/.
For users using versions below GPS 4.3.1, please upgrade your GPS to the latest version.
Open Tokeneer With GPS
Start GPS. In the Welcome Dialog, select Open Existing Project and open
-
tis_spark_tut.gpr located in the directory
tokeneer/code/core.
Check that the SPARK menu is in the menu bar. If it is not, make sure that the SPARK toolset’s bin directory is on your path, then restart GPS.
Alternately, if you did not open the project with the Welcome Dialog then select Open in the Project menu and open tis_spark_tut.gpr.
Running the SPARK Examiner
GPS
In the Project View, in the directory “.”, open the file you wish to Examine by double clicking on it.
Select Examine File in the SPARK menu.
The results of the analysis is displayed in the SPARK Output tab.
Command Line
Ensure that the SPARK toolset’s bin directory is in your path.
To Examine a file
spark <filename>
To Examine all files in Tokeneer
spark @tis
Analyse Tokeneer
This page describes how to analyse Tokeneer using the SPARK toolset – Examiner, Simplifier and POGS.
GPS
Run the SPARK Examiner on the file you wish to Examine.
Select Simplify All in the SPARK menu. The output is displayed in the SPARKSimp Output tab.
It may take a few minutes when you run the Simplifier the first time. Subsequent runs should be much faster as it only re-analyses files that have changed.
Run POGS by selecting POGS in the SPARK menu. A verification summary is then displayed in the core.sum tab and saved to the file core.sum.
Command Line
Run the Examiner against the modified file and then run the Simplifier. Run POGS to then generate a summary file that shows the result of the analysis. The sequence of commands are shown below.
It may take a few minutes when you run the Simplifier the first time. Subsequent runs should be much faster as it only re-analyses files that have changed.
spark <modified_filename>
sparksimp -l
pogs
Chapters
- Introduction
- What is Special About SPARK Contracts?
-
Preamble
Getting Started -
Lesson 1
Dealing with Improper Initialization -
Lesson 2
Identifying Ineffective Statements -
Lesson 3
Validating Input -
Lesson 4
SPARK Contracts -
Lesson 5
Dealing with Overflow Errors -
Lesson 6
Ensuring Secure Information Flow -
Summary
Finding More Information - Installing SPARK and GPS
- Starting GPS
- Running the Examiner
- Analyse Tokeneer