Gem #71: Tokeneer Discovery - Lesson 1
by Dean KuoAngela Wallenburg —AltranAltran
Let's get started…
Note: This series of Gems makes references to SPARK and the Tokeneer project, which you can find out more about by visiting http://www.adacore.com/home/products/sparkpro/tokeneer/. See also the SPARK tutorial at http://www.adacore.com/home/products/sparkpro/tokeneer/discovery/.
As stated in the SANS Common Weakness Enumeration (http://cwe.mitre.org/top25/#CWE-665): "If you don't properly initialize your data and variables, an attacker might be able to do the initialization for you, or extract sensitive information that remains from previous sessions. When those variables are used in security-critical operations, such as making an authentication decision, then they could be modified to bypass your security. Incorrect initialization can occur anywhere, but it is probably most prevalent in rarely-encountered conditions that cause your code to inadvertently skip initialization, such as obscure errors." Improper initialization is listed as one of the top twenty-five most dangerous programming errors by the SANS Institute. How would you find those? How much would your compiler help?
The SPARK Toolset identifies all variables that have not been initialized prior to being read. And if the SPARK automatic source code analysis finds no uninitialized variables, then there really are none!
In this Gem, we will first inject a couple of initialization errors into some of the Tokeneer code and then show how you can use the SPARK tools to find those errors.
Step-by-Step Instructions
Let us start by first running the Examiner, one of the SPARK tools, on some of the Tokeneer code in the correct version. Then we will inject an uninitialized variable error in the same code and see how the Examiner's data-flow analysis finds it for us.
Step 1: Run the Examiner on the correct version of the code
The code below is from the procedure GetStartAndEndTimeFromFile in auditlog.adb.
264 procedure GetStartAndEndTimeFromFile
265 (TheFile : in out File.T;
266 Description : out AuditTypes.DescriptionT)
267 --# global in out AuditSystemFault;
268 --# derives AuditSystemFault,
269 --# TheFile from *,
270 --# TheFile &
271 --# Description from TheFile;
272 is
273 OK : Boolean;
274 FirstTime : Clock.TimeTextT;
275 LastTime : Clock.TimeTextT;
276 TimeCount : Natural; -- type Natural to match formal parameter
277 -- in call to GetString
278 TimeOK : Boolean := True;
279
...
311 -------------------------------------------------------------------
312 -- begin GetStartAndEndTimeFromFile
313 -------------------------------------------------------------------
314 begin
315
316 FirstTime := Clock.PrintTime(Clock.ZeroTime);
317 LastTime := Clock.PrintTime(Clock.ZeroTime);
...
358 Description := ConvertTimesToText;
359
360 end GetStartAndEndTimeFromFile;
Run the Examiner on auditlog.adb and notice that it reports no errors.
Step 2: Inject an initialization error and find it using the Examiner
Let's introduce two types of uninitialized variables into the code -- variables that are never initialized and variables that may not be initialized.
Lines 316 and 317 initialize the variables FirstTime and LastTime. Put these two lines of code inside an if statement so that the variables are only initialized if the variable OK is true. The modified code is shown below.
316 if OK then
317 FirstTime := Clock.PrintTime(Clock.ZeroTime);
318 LastTime := Clock.PrintTime(Clock.ZeroTime);
319 end if;
The changes introduce a number of improper initialization errors:
* The variable OK is not initialized before it is read;
* The variables FirstTime and LastTime may not be initialized;
* The uninitialized variables FirstTime, LastTime and OK may then
influence the expression that assigns a value to the variable
Description -- the variable OK is indirectly used in the expression.
Rerun the Examiner and notice that the Examiner identifies all uninitialized variables as errors, and it differentiates between variables that are not initialized and variables that may not be initialized:
auditlog.adb:316:10: Flow Error 20 - Expression contains reference(s) to variable OK which has an undefined value. auditlog.adb:316:10: Flow Error 22 - Value of expression is invariant. auditlog.adb:360:7: Flow Error 504 - Statement contains reference(s) to variable FirstTime, which may have an undefined value. auditlog.adb:360:7: Flow Error 504 - Statement contains reference(s) to variable LastTime, which may have an undefined value. auditlog.adb:362:8: Flow Error 602 - The undefined initial value of OK may be used in the derivation of Description. auditlog.adb:362:8: Flow Error 602 - The undefined initial value of FirstTime may be used in the derivation of Description. auditlog.adb:362:8: Flow Error 602 - The undefined initial value of LastTime may be used in the derivation of Description.
Notice also that the compiler already warns against the simplest of these improper initialization errors:
auditlog.adb:316:04: warning: "OK" may be referenced before it has a value
Step 3: Find an array index initialization error
Another common error is accessing an array element with an uninitialized variable as the index. In this example we will inject such an error and demonstrate that the Examiner also finds these errors.
The code below is from the procedure DeleteLogFile in auditlog.adb.
512 procedure DeleteLogFile ( Index : LogFileIndexT)
513 --# global in out AuditSystemFault;
514 --# in out LogFiles;
515 --# in out LogFilesStatus;
516 --# in out LogFileEntries;
517 --# derives AuditSystemFault,
518 --# LogFiles from *,
519 --# LogFiles,
520 --# Index &
521 --# LogFilesStatus,
522 --# LogFileEntries from *,
523 --# Index;
524 is
525 OK : Boolean;
526 TheFile : File.T;
527 begin
528
529 TheFile := LogFiles (Index);
...
543 end DeleteLogFile;
Line 529 of the code accesses the Indexth element of the array LogFiles.
Declare a new variable I of type LogFileIndexT and replace Index, on line 529, with I. The modified code is shown below.
512 procedure DeleteLogFile ( Index : LogFileIndexT)
...
524 is
525 OK : Boolean;
526 TheFile : File.T;
527 I : LogFileIndexT;
528 begin
529
530 TheFile := LogFiles (I);
Run the Examiner on the file auditlog.adb and notice that it reports that the variable I has not been initialized:
auditlog.adb:530:18: Flow Error 20 - Expression contains reference(s) to variable I which has an undefined value. auditlog.adb:544:8: Flow Error 32 - The variable I is neither imported nor defined. auditlog.adb:544:8: Flow Error 50 - AuditSystemFault is not derived from the imported value(s) of Index. auditlog.adb:544:8: Flow Error 602 - The undefined initial value of I may be used in the derivation of AuditSystemFault. auditlog.adb:544:8: Flow Error 602 - The undefined initial value of I may be used in the derivation of LogFiles.
Again, in this very simple case, the compiler is able to spot the error too:
auditlog.adb:530:07: warning: variable "I" is read but never assigned
Although warnings from the compiler and warnings from the Examiner can sometimes overlap, one should keep in mind that the compiler warnings are heuristic, while the Examiner will warn against all possible improper initialization errors.
Summary
We have seen that the the SPARK tools can verify that a SPARK program is free from improper input validation errors. In the next Gem, we will study how SPARK handles a related class of errors -- identifying ineffective statements.