Lesson 1: Dealing with Improper Initialization
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 errors is listed as one of the
top
most dangerous programming errors. How
would you find those? How much would your compiler help?
The SPARK Toolset identifies all variables that have not been initialized prior to them being read. And - if the SPARK automatic source code analysis finds no uninitialized variables then there really are none!
In this lesson, 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 to 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 (follow this link to find out how) for 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.
Re-run the Examiner and notice that the Examiner identifies all uninitialized variables as errors (follow this link to see the reported errors) and it differentiates between variables that are not initialized and variables that may not be initialized.
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.
Start with a fresh copy of the file auditlog.adb by copying the file auditlog_copy.adb in tokeneer/code/core to auditlog.adb in the same directory. 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, on line 529, Index 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);
Examine the file auditlog.adb and notice that it reports that the variable I has not been initialized.
Summary
We have seen that the the SPARK tools can verify that a SPARK program is free from improper initialization errors. In the next lesson, we will study how SPARK handles a related class of errors - Identifying Ineffective Statements.