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.
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.
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.
About the AuthorAngela 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: 10/5/2009