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.