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.