Gem #73: Tokeneer Discovery - Lesson 3

by Dean KuoAngela Wallenburg—AltranAltran

Let's get started…


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 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 Gem, the above code will be investigated using the SPARK tools. This Gem 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

The correct lines of code are the following:

         233      if Success and then
         234         (RawDuration <= Integer(DurationT'Last) / 10 and 
         235          RawDuration >= Integer(DurationT'First) / 10) then 
         236         Value := DurationT(RawDuration * 10);
         237      else

Analyse Tokeneer using the following 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, where 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 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 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 Gem we have seen this exemplified with input validation. In the next Gem, we will look into SPARK contracts.


About the Author

Angela Wallenburg has worked as a programmer and researcher since 1998. Early in her career she developed operation control and optimization software. Since program verification captured her interest she has worked on building verification tools at Chalmers and Gothenburg University in Sweden, University of Koblenz-Landau in Germany and Microsoft Research in the US. She joined Altran and the SPARK team in 2009 to continue her quest to build really usable tools for software engineers.
Last Updated: 10/13/2017
Posted on: 11/2/2009