Gem #76: Tokeneer Discovery - Lesson 6

by Dean KuoAngela Wallenburg—AltranAltran

Let's get started…


Error message information leak occurs when secure data is leaked, through error messages, to unauthorised users, and is one of the top twenty-five most dangerous programming errors according to SANS Institute. The general problem is ensuring that information flow adheres to certain policies -- for example, certain data should never be written in an error message to a log file that may be accessible by unauthorised users.

The objective of this Gem is to demonstrate that the Examiner detects information flow violations.

Step-by-Step Instructions

Step 1: Study a Contract from an Information Flow Perspective

The code below is from the procedure Verify in bio.adb. The out variable MatchResult returns the result of whether a person's fingerprint matched their template. The local variable NumericReturn is set to the enumerated value BioApiOk if the fingerprint successfully matched; otherwise it returns an error code.

When a match is unsuccessful, a log record is written including the variable NumericReturn, which is derived from the person's Template.

      221  procedure Verify(Template       : in     IandATypes.TemplateT;
      222                   MaxFAR         : in     IandATypes.FarT;
      223                   MatchResult    :    out IandATypes.MatchResultT;
      224                   AchievedFAR    :    out IandATypes.FarT)
             ...
      230  --# derives AuditLog.State,
      231  --#         AuditLog.FileState from AuditLog.State,
      232  --#                                 AuditLog.FileState,
      233  --#                                 Template,
      234  --#                                 Clock.Now,
      235  --#                                 ConfigData.State,
      236  --#                                 Interface.Input &
             ...
      242  is
      243     NumericReturn : BasicTypes.Unsigned32T;
      244  begin
      245     Interface.Verify(Template     => Template,
      246                      MaxFAR       => MaxFAR,
      247                      MatchResult  => MatchResult,
      248                      AchievedFAR  => AchievedFAR,
      249                      BioReturn    => NumericReturn);
      250
      251     if NumericReturn /= ValueOf(BioAPIOk) then
      252        -- An error occurred, overwrite match information.

      253        MatchResult := IandATypes.NoMatch;
      254        AuditLog.AddElementToLog
      255          (ElementID    => AuditTypes.SystemFault,
      256           Severity     => AuditTypes.Warning,
      257           User         => AuditTypes.NoUser,
      258           Description  => MakeDescription ("Biometric device failure ",
      259                                            NumericReturn));
      260        end if;
      261  end Verify;

If the log were accessible to potential hackers, which is not the case for Tokeneer, then this would be an example of an error message information leak. Fingerprint templates should never be accessible by hackers.

Step 2: Change an Information Flow Aspect of the Contract

Change the contract for the procedure Verify to specify that no information written to the log is derived from Template by deleting line 233.

       230   --# derives AuditLog.State,
       231   --#         AuditLog.FileState from AuditLog.State,
       232   --#                                 AuditLog.FileState,
       233   --#                                                     
       234   --#                                 Clock.Now,
       235   --#                                 ConfigData.State,
       236   --#                                 Interface.Input &

The corresponding line (line 73) of code needs to be removed from the file bio.ads.

       60   procedure Verify(Template       : in     IandATypes.TemplateT;
       61                    MaxFAR         : in     IandATypes.FarT;
       62                    MatchResult    :    out IandATypes.MatchResultT;
       63                    AchievedFAR    :    out IandATypes.FarT);
            ...
       69   --# derives AuditLog.State,
       70   --#         AuditLog.FileState from Input,
       71   --#                                 AuditLog.State,
       72   --#                                 AuditLog.FileState,
       73   --#                                                     
       74   --#                                 Clock.Now,
       75   --#                                 ConfigData.State &

Step 3: Use the SPARK Tools to Detect the Information Leak

Examine the file bio.adb and notice the Examiner reports the error that information derived from the variable Template is written to the log. This means that data derived from the template is being written to the log!

bio.adb:261:8:
    Flow Error 601 - AuditLog.State may be derived from the imported value(s) of Template.
bio.adb:261:8:
    Flow Error 601 - AuditLog.FileState may be derived from the imported value(s) of Template.

Step 4: Introduce a Malicious Hack

The Examiner also detects when data has been incorrectly used. We now add back door code in the procedure Verify (lines 248-251 below). It returns a positive match independent of the user's fingerprint when the clock is at midnight.

      223  procedure Verify(Template       : in     IandATypes.TemplateT;
      224                   MaxFAR         : in     IandATypes.FarT;
      225                   MatchResult    :    out IandATypes.MatchResultT;
      226                   AchievedFAR    :    out IandATypes.FarT)
            ...
      232  --# derives AuditLog.State,
      233  --#         AuditLog.FileState from AuditLog.State,
      234  --#                                 AuditLog.FileState,
      235  --#                                 Template,
      236  --#                                 Clock.Now,
      237  --#                                 ConfigData.State,
      238  --#                                 Interface.Input &
               ...
      244  is
      245     NumericReturn : BasicTypes.Unsigned32T;
      246     T             : Clock.TimeT;
      247  begin
      248     T := Clock.GetNow;
      249     if T = Clock.ZeroTime then
      250        MatchResult := IandATypes.Match;
      251        AchievedFAR := 0;
      252     else
      253
      254        Interface.Verify(Template     => Template,
      255                         MaxFAR       => MaxFAR,
      256                         MatchResult  => MatchResult,
      257                         AchievedFAR  => AchievedFAR,
      258                         BioReturn    => NumericReturn);
      259
              ...
      272    end if; 
             ...
      275  end Verify;

Step 5: Use the SPARK Tools to Detect the Weakness

Examine the file bio_bad.adb and notice that the Examiner reports the error that MatchResult is dependent on the current time (Clock.now), which is inconsistent with the procedure's contract. The Examiner has identified an information flow inconsistency due to the presence of the back door.

bio_bad.adb:243:40:
    Flow Error   4 - The dependency of the exported value of AuditLog.State on the imported value
    of  Verify.Template has not been previously stated.
bio_bad.adb:243:40:
    Flow Error   4 - The dependency of the exported value of AuditLog.FileState on the imported value
    of Verify.Template has not been previously stated.
bio_bad.adb:275:8:
    Flow Error 601 - MatchResult may be derived from the imported value(s) of Clock.Now.
bio_bad.adb:275:8:
    Flow Error 601 - AchievedFAR may be derived from the imported value(s) of Clock.Now.

Summary

In this Gem we have learnt about information flow contracts and we have seen the SPARK tools detect a malicious hack. SPARK programs are free from information leaks when the contract accurately specifies the desired information flow between variables.


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: 12/14/2009