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.


About the Author

Angela 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