Gem #75: Tokeneer Discovery - Lesson 5

by Dean KuoAngela Wallenburg—AltranAltran

Let's get started…


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 Gem about input validation, we saw an example of an arithmetic overflow. In this Gem, 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

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. 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 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 Gem we have seen how the SPARK tools can be used to detect a buffer overflow error. In the next Gem, we will see how SPARK can be used in Ensuring Secure Information Flow.


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/30/2009