product_tokeneerdiscovery

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.

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.py in the directory gnatpro/share/gps/plug-ins/ with the copy in the directory tokeneer/tools/plug_ins/gps4.4.1/.
  • For GPS 4.3.1, Replace the file spark.py in the directory gnatpro/share/gps/plug-ins/ with the copy in the directory tokeneer/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