Lesson 4: SPARK Contracts
This lesson extends What is Special About SPARK Contracts to show how the SPARK Toolset can verify application specific safety and security properties.
In this lesson, we will see how the SPARK tools detect any differences between a program’s intended behaviour, as specified in its contract, and its actual behaviour, as implemented in the code. Thus the SPARK tools can be used either to find defects in the contract, to find defects in the implementation, to find defects in both, or to show conformance between intended and actual behaviour.
Step-by-Step Instructions
Step 1: Analyse the Correct Version of the Code
The precondition for the procedure AddElementToCurrentFile in auditlog.adb (lines 772 - 774 in the code below) specifies that the value stored in the CurrentLogFileth element of the array LogFileEntries is less than MaxLogFileEntries and the postcondition specifies that the array element is incremented by 1. The information-flow related contracts (derives annotation) will be dealt with in the lesson about information flow analysis.
751 procedure AddElementToCurrentFile 752 (ElementID : in AuditTypes.ElementT; 753 Severity : in AuditTypes.SeverityT; 754 User : in AuditTypes.UserTextT; 755 Description : in AuditTypes.DescriptionT) 756 ––# global in Clock.Now; 757 ––# in CurrentLogFile; 758 ––# in out AuditSystemFault; 759 ––# in out LogFiles; 760 ––# in out LogFileEntries; 761 ––# derives AuditSystemFault, 762 ––# LogFiles from *, 763 ––# Description, 764 ––# LogFiles, 765 ––# Clock.Now, 766 ––# ElementID, 767 ––# Severity, 768 ––# User, 769 ––# CurrentLogFile & 770 ––# LogFileEntries from *, 771 ––# CurrentLogFile; 772 ––# pre LogFileEntries(CurrentLogFile) < MaxLogFileEntries; 773 ––# post LogFileEntries(CurrentLogFile) = 774 ––# LogFileEntries˜(CurrentLogFile) + 1; 775 776 is 777 TheFile : File.T ; 778 begin 779 TheFile := LogFiles (CurrentLogFile); 780 AddElementToFile 781 (TheFile => TheFile, 782 ElementID => ElementID, 783 Severity => Severity, 784 User => User, 785 Description => Description); 786 LogFiles (CurrentLogFile) := TheFile; 787 788 LogFileEntries(CurrentLogFile) := LogFileEntries(CurrentLogFile) + 1; 789 end AddElementToCurrentFile;
Analyse Tokeneer with the SPARK Toolset. The result of the analysis is logged in core.sum and it shows (see below) that the SPARK Toolset has identified no problems with the code in the procedure AddElementToLogFile - the columns False and TO DO are empty.
659 VCs for procedure_addelementtocurrentfile : 660 ---------------------------------------------------------------------------- 661 | | | -----Proved In----- | | | 662 # | From | To | vcg | siv | plg | prv | False | TO DO | 663 ---------------------------------------------------------------------------- 664 1 | start | rtc check @ 781 | | YES | | | | | 665 2 | start | rtc check @ 782 | | YES | | | | | 666 3 | start | rtc check @ 788 | | YES | | | | | 667 4 | start | rtc check @ 790 | | YES | | | | | 668 5 | start | assert @ finish | | YES | | | | | 669 —————————————————————————-
Step 2: Change the Contract - But not the Implementation
Let us change the postcondition so the procedure’s contract no longer matches its implementation. The SPARK Toolset will then detect the inconsistency. Change the postcondition to specify that the array element LogFileEntries(CurrentLogFile) should be incremented by 10, the modified code is shown below.
772 ––# pre LogFileEntries(CurrentLogFile) < MaxLogFileEntries;
773 ––# post LogFileEntries(CurrentLogFile) =
774 ––# LogFileEntries˜(CurrentLogFile) + 10;
775
Step 3: Re-Analyse and Study the Results
Re-analyse Tokeneer and open the file core.sum. The results of the analysis for the procedure AddElementToLogFile has changed - the columns False and TO DO are no longer empty (see below).
SPARK Toolset has identified a potential problem with the code and the details are described in the file addelementtocurrentfile.siv (siv files are generated by the Simplifier to provide details of its analysis) in the directory tokeneer/code/core/auditlog/addelementtologfile. The problem is that the procedure’s contract and implementation don’t match.
659 VCs for procedure_addelementtocurrentfile :
660 ----------------------------------------------------------------------------
661 | | | -----Proved In----- | | |
662 # | From | To | vcg | siv | plg | prv | False | TO DO |
663 ----------------------------------------------------------------------------
664 1 | start | rtc check @ 781 | | YES | | | | |
665 2 | start | rtc check @ 782 | | YES | | | | |
666 3 | start | rtc check @ 788 | | YES | | | | |
667 4 | start | rtc check @ 790 | | YES | | | | |
668 5 | start | assert @ finish | | | | | YES | |
669 —————————————————————————-
Step 4: Revert the Contract - But Change the Implementation
Undo the changes to the postcondition and change line 788 so that the input value is preserved.
774 ––# pre LogFileEntries(CurrentLogFile) < MaxLogFileEntries;
775 ––# post LogFileEntries(CurrentLogFile) =
776 ––# LogFileEntries~(CurrentLogFile) + 1
…
791 LogFileEntries(CurrentLogFile) := LogFileEntries(CurrentLogFile) + 0;
792 end AddElementToCurrentFile;
Re-analyse Tokeneer and open the file core.sum. The analysis of the procedure is unchanged as the implementation, like previously, does not match the procedure's contract.
Step 5: Strengthen the Contract
Revert the code to its original state.
In SPARK, we can strengthen the procedure’s contract and say more about the properties of the procedure. Let’s add extra code assigning the value in the first element of the array LogFileEntries to 10 if CurrentLogFile is not LogFileIndexType’First (lines 789 - 791 below).
788 LogFileEntries(CurrentLogFile) := LogFileEntries(CurrentLogFile) + 1; 789 if CurrentLogFile /= LogFileIndexType’First then 790 LogFileEntries(LogFileIndexType’First) := 10; 791 end if; 792 end AddElementToCurrentFile;
Re-analyse Tokeneer and open the file core.sum and notice that no errors are reported as the procedure’s implementation is not inconsistent with its contract. The post-condition says nothing about the effects of the procedure on any of the array elements except the one indexed by CurrentLogEntry.
We can strengthen the post-condition (lines 775 and 776 below) to specify that only the entry indexed by CurrentLogFile is incremented and all other elements remain unchanged.
772 ––# pre LogFileEntries(CurrentLogFile) < MaxLogFileEntries;
773 ––# post LogFileEntries = LogFileEntries~[CurrentLogFile => LogFileEntries~(CurrentLogFile)+1];
Re-analyse Tokeneer and open the file core.sum and notice, on lines 659 to 671, that the mismatch between the implementation and contract has been detected. The details of the problem are recorded in the file addelementtocurrentfile.siv in the directory tokeneer/code/core/auditlog/addelementtologfile.
657 VCs for procedure_addelementtocurrentfile :
658 ----------------------------------------------------------------------------
659 | | | -----Proved In----- | | |
660 # | From | To | vcg | siv | plg | prv | False | TO DO |
661 ----------------------------------------------------------------------------
662 1 | start | rtc check @ 783 | | YES | | | | |
663 2 | start | rtc check @ 784 | | YES | | | | |
664 3 | start | rtc check @ 790 | | YES | | | | |
665 4 | start | rtc check @ 792 | | YES | | | | |
666 5 | start | rtc check @ 794 | | YES | | | | |
667 6 | start | assert @ finish | | | | | | YES |
668 7 | start | assert @ finish | | YES | | | | |
669 —————————————————————————-
Summary
This lesson demonstrates that the more precise the specification, the more bugs the SPARK Toolset can detect. The use of the SPARK Toolset during development to verify code is, in our experience, more effective than compiling and testing, since the analysis is for all input data and not just a few specific test cases. Next, we will see how SPARK Deals with Overflow Errors.