|
Gem #75: Tokeneer Discovery – Lesson 5
Author: Dean Kuo and Angela Wallenburg, Praxis High Integrity Systems
Abstract: Ada Gem #75 — In the previous Gem in this series, we saw how the SPARK Toolset can verify application-specific safety and security properties, based on source code from Tokeneer. In this Gem, we show how to deal with overflow errors.
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.
Posted
in Ada / Ada 2005, Development Log, Devt log - Gem of the Week
Have your own idea for a Gem?
If you have an idea for a Gem you would like to contribute please feel free to contact us at: gems@adacore.com
Siarhei Kirkorau said:
The decision of a problem of overflow of the buffer it is important in the field of safety of information systems. Useful article.