Tokeneer Discovery - A SPARK Tutorial

Lesson 6: Ensuring Secure Information Flow

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. 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 lesson 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 - see bio-interface.ads's specification for the procedure Verify.


       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 was accessible to potential hackers, which is not the case for Tokeneer, then this is 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!

Step 4: Introduce a Malicious Hack

The Examiner also detects when data has been incorrectly used. The file bio_bad.adb contains a back door code in the procedure Verify (lines 248-251). It now 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.

Summary

In this lesson 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.