Tokeneer Discovery - A SPARK Tutorial

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:

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.