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.