Formal Methods for Smart Cards: an experience report ⋆
Contents
1. 1 Introduction With the emergence of smart cards industry has become more interested in techniques to establish the correctness and security of the applications devel This work is partially supported by the European Union as part of the Verificard project IST 2000 26328 Email addresses ceesb cs kun nl C B Breunesse Nestor Catano inria fr N Catano Marieke Huisman inria fr M Huisman bart cs kun nl B Jacobs Preprint submitted to Elsevier Science 1 February 2008 oped Typical smart card applications like electronic purses and health care information holders contain privacy sensitive information For the acceptance of the use of smart cards in such domains it is necessary that the users trust that details of their private life are not passed on to third parties Industry has realized that the only way to ensure this is by rigorous use of formal tech niques for specification and verification of smart card applications Moreover this is enforced in higher levels of evaluation schemes like Common Criteria This paper does not deal with security aspects like data leakage but inves tigates functional behavior and possible abnormalities such as null pointer exceptions Proper functional behavior and safety properties are a first step towards secure applications Other researchers investigate how JML can be used to specify actual security features 28 However as always the problem is that formal methods are considere2. using automatic tools only can already help to improve an application We show in particular how the formal specification helped to identify ambiguities and inconsistencies in the informal documentation and unnecessary checks in the implementation However this does not mean that full verification is not necessary the verifications as described in the next section fall completely out of the scope of what can be checked with ESC Java On the other hand the verification with ESC Java on the entire purse falls out of the scope of the LOOP tool because the purse simply is too large Manageable parts of source code that can be verified with LOOP are in the order of hundreds of lines of code Elsewhere 5 we have already reported on the different kinds of errors and possibilities for improvement that we found in the case study with ESC Java Here we will not discuss these in full detail but we will give a more general overview of the typical kind of problems that can easily be found by auto matic tools However to give an indication we found roughly 20 errors and possibilities for improvement Further we found approximately 25 unreach able code fragments Notice that most of these errors are straightforward to find requiring only simple specifications When writing the specifications we decided to take the code as it is as a starting point Only when we found real mistakes in the code we would change it but we did not change the desig
3. FREE LOCKED SECRET_CODE SECURE_MESSAGING or SECRET_CODE and SECURE_MESSAGING This last combination is represented by the bitwise or of the two constants This restriction on the variable condition is easily expressed as a class invariant public static final byte FREE byte 1 public static final byte LOCKED byte 2 public static final byte SECRET_CODE byte 4 public static final byte SECURE_MESSAGING byte 8 spec_public private byte condition FREE 22 invariant condition FREE condition LOCKED condition SECRET_CODE condition SECURE_MESSAGING condition SECRET_CODE SECURE_MESSAGING When deciding whether the card is in the appropriate state to perform a certain operation this is basically implemented by a case distinction a Java switch statement as in this method verify signals AccessConditionException false private final boolean verify byte c throws AccessConditionException byte t byte 0 switch condition case FREE return true case SECRET_CODE return case SECURE_MESSAGING return case SECRET_CODE SECURE_MESSAGING return case LOCKED return false default assert false t AccessConditionException CONDITION_COURANTE_INVALIDE AccessConditionException throwIt t return false For our exposition it is not important what this method actually computes but we are interested in its structure The c
4. Next Sect 4 discusses several aspects of specifying Java Card applications and Sect 5 gives an overview of how the purse case study is annotated and checked using ESC Java while Sect 6 focuses on a single class and discusses its verification using LOOP in full detail Finally Sect 7 draws conclusions and sketches a view on further use of formal methods in industry Via http www gemplus com smart r_d publications case study 2 Java Card is a dialect of Java that is used to program smart card applications The Java Card language is an extended subset of Java in particular it does not contain multi threading floats doubles and multi dimensional arrays but it does contain some additional constructs such as shareable interfaces which are used to enable communication between different applets 2 JML 2 1 The language The development of JML short for Java Modeling Language 19 was started by Gary Leavens and his team at Iowa State University but is now a community process with many people involved 20 There is a group of active users and tool developers where new language proposals are discussed before they actually become part of the official language standard The JML language is designed to be easy and accessible for an average Java programmer Therefore the specifications use Java syntax and are written in the source code as specially marked comments Markers and enable the various JML
5. are supplemental to the ones con structed and checked using ESC Java 5 When we refer to the Decimal class we mean our modified variant Note that the specifications for the Decimal class in this section are out of scope for fully automatic tools as ESC Java The Decimal class receives special attention because e it is an independent self contained class Hence the verification is indepen dent of other specifications of the purse as well This simplifies the verifica tion process e the Decimal class is a backbone of the purse applet Therefore verification is important and its correctness is critical to the proper functioning of the purse applet Many classes in the purse use Decimal as a library class e it isnot only a backbone of the applet so is the class that handles the APDU communications for example but it is also a functional class that does the actual arithmetic needed to increase the balance on the card Functional specifications can be expressed well using JML e its size is limited Large Java classes with elaborate methods are very costly to specify and verify The Decimal class consists of 40 methods roughly 1 5 kilobytes whereas the whole purse is 432 kB of source code The Decimal class the header of which is shown in Fig 1 is used in the purse to store real numbers with a precision of three digits Because floats do not exists in Java Card the Decimal class is the place where this kind of arithmetic
6. exception is thrown 10 Further at MIT one uses JML as specification language for Daikon 9 which is a tool for invariant detection Based on several test runs this tool tries to establish possible class invariants There are also several tools which are inspired by ESC Java Chase 6 devel oped at INRIA Sophia Antipolis is a tool for checking the modifies clauses an aspect of JML which is not treated by ESC Java At Compaq a tool called Calvin 13 has been developed Calvin can be used to check properties about multi threaded programs It uses a technique to reduce the proof obligations to proof obligations on single threads using appropriate annotations which then can be checked using ESC Java Further at Gemplus a tool called Jack has been developed 4 Jack works similar to ESC Java in that it generates proof obligations based on the an notations and then sends those off to a prover but it aims at being sound and complete Jack has been designed in such a way that it can interface different proof tools currently AtelierB Simplify and Coq Further Jack has been in tegrated with a standard IDE which makes it easy to use for a Java developer Other tools for full program verification using interactive theorem provers are Jive and Krakatoa The Jive tool 26 which is developed in Kaiserslautern implements a Hoare logic for Java 29 and generates proof obligations for PVS or Isabelle The Krakatoa tool 24 is devel
7. interface to the outside world For example for a pri vate method it might still be possible to write an offensive specification if all calls to this method guarantee the precondition In this case study we started writing specifications for existing code At first we decided to leave the code unchanged Therefore we write defensive speci fications for methods that make explicit tests on the values of their arguments 6 However when writing formal specifications one gets a good idea about possible improvements Therefore Sect 6 presents the verification of an improved version of the code for the Decimal class only 15 thus following the implementation However as discussed in Sect 5 we also found several places where unnecessary tests were made and the exceptional cases never could occur 4 1 3 Level of abstraction of specifications When writing readable specifications it is important to have a reasonable level of abstraction Two techniques for achieving a higher level of abstraction are the use of pure methods t e side effect free methods and the use of model variables in specifications Both are provided by JML and supported by the LOOP compiler but ESC Java does not support them except for the use of ghost variables which is a more limited variation of model variables Since within this case study most of the specifications are checked using ESC Java the specifications often are more verbose than we would have
8. liked In particular most of the specifications are written in terms of the concrete variables and without introducing any abstractions However for the class Decimal specifications with and without model variables exist Figure 1 in Sect 2 1 contains part of the specification of Decimal with model variables As an example the same method setValue is specified as follows for checking with ESC Java Q requires true modifies intPart decPart ensures intPart v ensures decPart short 0 ensures result this signals DecimalException v lt 0 public Decimal setValue short v throws DecimalException An example where abstraction could improve the readability of the specifica tion is in the communication between card and terminal As explained above this communication takes place by sending so called APDUs which are com mands encoded as arrays However when writing specifications one would prefer to do this in terms of the abstract notion of commands instead of in terms of the contents of the APDU buffer 4 2 Specifications for the Java Card API We used the specifications for the Java Card API written by Erik Poll and other members of the LOOP project 30 as basis for this work In short 16 these are offensive specifications that describe when methods are guaranteed not to throw unwanted runtime exceptions We cannot present here the JML specifications for the whole Java Card API but as a
9. no exceptions will occur or does one also want to specify exactly which postconditions are established 7 e the complete behavior of a method or class Naturally the more information is given by a specification the better it re flects the behavior of a program However in some cases the postcondition of a method might be too complicated to formulate or would basically require repeating the method implementation One also has to remember that giving specifications only makes sense when one has reasonable confidence that the specification is correct Thus when specifying methods with complicated con trol structures or data manipulations and checking these specifications with an automatic tool as ESC Java it might not make sense to specify compli cated postconditions because one can never rely on their correctness given the limitations of such tools If one wishes to actually specify and verify such complex postconditions one should use e g LOOP and do full verification 13 Additionally it is also important to consider what is the return of the invest ment put into writing specifications 7 e how does the number of bugs found relate to the amount of time spent on writing the specifications If most bugs can be found by writing lightweight specifications only one seriously has to consider whether it is worth the extra effort of making heavier specifications This issue is very important in industry where every investment has to be e
10. short e2 short a2 f d2 100 10 short e3 short a3 f d3 1000 short rest short e1 e2 e3 add short 0 short gross rest 1000 The rest part of the new mul is computed by two shorts gross and rest which are both additions of 3 shorts d1 d2 d3 and e1 e2 e3 respectively The construction of these shorts is explained by unfolding the rest part decPart x 1000 below In the following equations decPart and f are called a and b respectively When we write a we mean the it digit of a counting from left to right a x b 1000 a az az b 1000 28 Number a consists of 3 digits 100 a b 10 a b 1000 a3 b Multiplication a b can therefore be split in 3 c Cg C3 C4 0 0 d amp eh 0 1000 fh eh The results of each of the 3 multiplications are named c c and c cy Cg C3 00 0 c4 0 0 4 amp 000 e 0 1000 F ci 0 0 0 c3 amp c4 Numbers c c and c are split in 2 cy C2 C3 c4 0 0 ad 6 0 1000 FPL g cz c3 c4 The division by 1000 is distributed over these two components d1 el a2 e2 1000 d3 e3 29 The names in tt font correspond to fields in the mul method All the parts of this multiplication can be computed without the risk of overflow The specification of the mul method has been verified by a combination o
11. then this is because the argument v is less than 0 In this case the value of decimal and implicitly of intPart and decPart is unchanged 2 2 The tools As mentioned before there is a wide range of tools available using JML as specification language This is one of the reasons why JML is becoming the de facto standard specification language for source code level specification of Java programs For our case study we have used the Extended Static Checker for Java ESC Java 22 12 and the LOOP compiler 23 We will describe these tools in some detail followed by a brief description of other tools that are available for JML Again for a more extensive overview of the various tools see 3 2 2 1 ESC Java ESC Java has been developed at Compaq Research in the group led by Rus tan Leino 22 12 Currently it is no longer maintained by Compaq but it is available as open source software An improvement making it compatible with official JML ESC Java 2 is done by David Cok Kodak and Joseph Kiniry Nijmegen 10 At the time of writing and verifying the ESC Java specifica tions in this paper version 2 was not yet available Therefore the ESC Java version used here is Compaq release 1 2 4 The initial design goal of ESC Java was to develop a tool which could effi ciently find common programming errors such as indexing an array out of bounds or null pointer dereferencing The user can guide the search for errors by putting appropri
12. tools to recognize the comments as JML annotations A simple JML specification consists of pre and post conditions for meth ods denoted by the keywords requires and ensures and class invariants restricting the reachable state space of an object However if wanted and needed much more complicated properties can be expressed Here we present only a few language constructs that are necessary for understanding this pa per we refer to the standard language documents for a full description of the language 19 20 First of all a method specification can contain exceptional postconditions so called exsures or signals clauses An exceptional postcondition specifies which conditions should hold if a method terminates abruptly because of an exception A typical usage of exceptional postconditions is to specify that the exception is thrown before any instance variables have been changed thus implicitly preserving the class invariants see the example in Fig 1 below Method specifications also can contain modifies clauses also known as as signable or modifiable clauses or frame conditions that restrict which variables may be changed by a method call Modifies clauses are crucial when doing modular program verification 21 It is also possible to restrict the reachable state space of an object by spec ifying a constraint In JML this denotes a relation between the pre and post state of a method restricting how a variable might change
13. two shorts an integer and a decimal part These values are multiplied with the intPart and decPart of the this object The ensures clause defines the 4 multiplications of 1 where the rest part is constructed by some complicated rounding The Gemplus multiplication code satisfies the specification below but mathematically speaking it is not defining a multiplication requires 0 lt f amp amp f lt PRECISION amp amp difficult rest part given by four options f gt 100 amp amp old decPart gt 100 O lt e amp amp e lt MAX_DECIMAL_NUMBER amp amp e 1 intPart 1 lt MAX_DECIMAL_NUMBER modifies decimal ensures decimal e old intPart PRECISION old intPart f e old decPart 26 old decPart 10 10 10 gt 100 amp amp old decPart lt 100 old decPart 10 100 f lt 100 amp amp old decPart gt 100 old decPart 10 f 100 old decPart f 1000 signals Exception e false eeOeAOAOOeOOO8OC eC e private void mul short e short f The rest part above is composed of case distinctions Suppose we multiply 0 998 with itself the answer given according to the above spec is 0 980 In precision arithmetic the answer to this multiplication is 0 998001 Rounded to 3 digits this makes 0 998 In the Nijmegen implementation we
14. value When writing specifications this aspect of the method s behavior will be made explicit An offensive specification will state in its precondition under which conditions the method will function correctly i e as specified Nothing is guaranteed on the behavior of the method if the precondition is not respected When the program is verified for each method call to the method one will be obliged to show that the precondition is respected A defensive specification however will not make any requirements on the caller of the method i e its precondition will be requires true but it will typically specify which ex ceptions are thrown when the input parameters are invalid Figure 6 sketches an offensive and a defensive specification for the same method When verifying the program in the offensive case one has to verify that the precondition a null is respected for each call to the method m In the defensive case no proof obligation exists for the precondition but one has to take into account that the method might finish abruptly because of an exception if it is called with a null Often offensive specifications are considered as the better way to write spec ifications see e g 25 However it might be the case that it is prescribed explicitly that no assumptions may be made on the state of the caller In such cases it is necessary to write defensive specifications This choice is ultimately governed by an object s
15. which typically occur in natural language documentation To il lustrate this we take an example from the class Transaction In this class an instance variable type is declared as follows the transaction type debit or credit spec_public private byte type Since the class also contains the following constant declarations the transaction status public static final byte TYPE_CREDIT byte 50 the transaction status 20 public static final byte TYPE_DEBIT byte 51 it seems natural to specify the following class invariant invariant type TYPE_CREDIT type TYPE_DEBIT However when checking whether this invariant is respected by all methods in the class it turns out that it is not the class contains a method reset which contains the assignment type INDETERMINE where INDETERMINE is another constant declared in the class One could consider this as an error given the documentation but it also seems reasonable that this is done on purpose After all when initializing or resetting a transaction one cannot say whether it will be a credit or debit operation and also neither of them is a typical default value Having a formal specification would clarify the initial intention of the developer and would allow to signal this problem earlier To summarize we would like to stress that writing a relatively easy formal specification instead of informal documentation hel
16. Again to keep performance and simplicity of the tool and to avoid many spurious warnings the designers of the tool do not always generate all the necessary verification conditions For example a loop statement by default is approximated by a single loop iteration The ESC Java manual 22 contains a detailed list of known sources of unsoundness and incompleteness of the original ESC Java The specification language that is used by ESC Java is not exactly a subset of JML Already some work has been done on integrating the two languages 8 and currently work on this is continued However for this paper the exact differences are not relevant It is sufficient to know that ESC Java supports the specification constructs described above except for the constraint and modifies construct and the support for model variables 2 2 2 LOOP tool The LOOP tool has been developed at the University of Nijmegen Its purpose is to offer a sound environment within the theorem prover PVS 27 in which formal verification of JML specifications written for Java source code can 4 See http research compaq com SRC esc Simplify html semantic prelude Java source code logical theories Loop compiler sa QED p p proof obligations Pys Q JML specifications Fig 3 LOOP tool schema be performed What is usually called the LOOP tool actually consists of a collection of tools The relation between the different parts is shown in Fi
17. Formal Methods for Smart Cards an experience report C B Breunesse N Catafio M Huisman B Jacobs INRIA Sophia Antipolis France gt University of Nijmegen the Netherlands Abstract This paper presents a case study in formal specification and verification of a smart card application The application is an electronic purse implementation developed by the smart card producer Gemplus as a test case for formal methods for smart cards It has been annotated by the authors with specifications using the Java Modeling Language JML a language designed to specify the functional behavior of Java classes The reason for using JML as a specification language is that several tools are available to check parts of the specification w r t an implementation These tools vary in their level of automation and in the level of correctness they ensure Several of these tools have been used for the Gemplus case study We discuss how the usage of these different tools is complementary large parts of the specifi cation can be checked automatically while more precise verification methods can be used for the more intricate parts of the specification and implementation We believe that having such a range of tools available for a single specification language is an important step towards acceptance of formal methods in industry Key words Formal specification languages smart cards Java Card formal verification JML ESC Java annotations
18. Journal of Logic and Algebraic Programming 58 1 2 89 106 2004 25 B Meyer Object Oriented Software Construction Prentice Hall 2 rev edition 1997 26 J Meyer and A Poetzsch Heffter An architecture of interactive program provers In S Graf and M Schwartzbach editors Tools and Algorithms for the Construction and Analysis of Systems TACAS 2000 number 1785 in LNCS pages 63 77 Springer 2000 27 S Owre S Rajan J M Rushby N Shankar and M K Srivas PVS Combining specification proof checking and model checking In R Alur and T A Henzinger editors Computer Aided Verification CAV 96 number 1102 in LNCS pages 411 414 Springer 1996 33 28 M Pavlova L Burdy G Barthe M Huisman and J L Lanet Enforcing high level security properties for applets In CARDIS 2004 2004 To appear 29 A Poetzsch Heffter and P M ller A programming logic for sequential Java In S D Swierstra editor Programming Languages and Systems ESOP 99 number 1576 in LNCS pages 162 176 Springer 1999 30 E Poll Formal interface Java specifications for the Java Card API 2 1 1 http www cs kun nl erikpoll publications jc211_specs html with contributions by other members of the LOOP project 34
19. One can for example specify that a variable is constant or that it can only increase No tice that invariants and constraints could be expressed as pre post condition specifications for each method but by specifying them explicitly one gets a higher level of abstraction Moreover in this way they immediately carry over to subclasses i e all methods in subclasses have to respect the invariants and constraints of superclasses Sometimes one also likes to specify explicitly that a condition holds at a partic ular point in a method body For this JML provides the assert annotation If a method body contains such an assert annotation this means that whenever control reaches this point in the method body the associated condition should hold This can be used for example to add outlines of correctness proofs to the implementation of a method body as is used by the LOOP compiler see below but also to state that a particular control point never can be reached using assert false As mentioned before the JML specifications use Java syntax More precisely the various conditions are written as side effect free boolean typed Java ex pressions To make the language more expressive and usable several additional specification constructs are available Again we mention only the few that are relevant for this paper For further information we refer to the JML documen tation 20 First of all there is a special keyword result that refers
20. also be used on such lightweight specifications but it is typically applied to more detailed functional specifications in selected smaller code fragments In this case study a precise high level specification for the Decimal class underlying the purse was developed implemented in a different way than the purse developers originally did and proven correct The verification was done interactively via a combination of Hoare logic and weakest precondition reasoning This has demonstrated that using different levels of verification with corresponding tools gives an attractive and feasi ble combination of global checking and selected local verification Part of this verification effort was developing the specifications One would hope that in the future advanced programmers will write such specifications themselves This would considerably reduce the effort spent on such verifica tion projects The whole verification underwent several updates and adapta tions w r t 2 5 so it is hard to estimate the investment But if we would have to start from scratch the application of ESC Java to the whole purse involves a couple of weeks work Applying the LOOP tool to the Decimal class only involves a similar investment As a result of this and other work JML has developed into the standard specification language for Java Card e g within the European project Verifi Card 14 Future work involves a further development of the JML language
21. amp amp d intPart 1 intPart 1 lt MAX_DECIMAL_NUMBER modifies decimal ensures decimal old decimal d decimal 1000 signals Exception e false public Decimal mul Decimal d mul d getIntPart d getDecPart return this Unfortunately this specification can not be proved using bounded 32 bit in tegral semantics The result of old decimal d decimal possibly does not fit in an integer When the JML community agrees on how to deal with bounded and unbounded specifications the LOOP tool will be adjusted appro 30 priately Until then the integral semantics of JML and Java remain coupled in LOOP technology so it is either all bounded or all unbounded semantics 7 Conclusions This paper discusses experiences with specification and verification of an in dustrial smart card case study using JML One of the advantages of the JML specification language is that it comes with a spectrum of validation tools ranging from runtime assertion checking through static checking to interactive verification The case study in this experience report was handled by the two latter verification techniques using Compaq s ESC Java tool and the LOOP tool from the University of Nijmegen It turned out that ESC Java works best for relatively lightweight specifications for which it can give immediate feed back It filtered out many common programming errors from the entire purse applet The LOOP tool can
22. ansactionException but the method will never raise a NullPointerException or ArrayIndex0utOfBoundsException excep tion This is the kind of specifications that can be checked efficiently automati cally a strong precondition about array variables ranges of values in which arrays can be accessed and conditions preventing the array variables of be ing null This strong precondition allows one to specify that certain excep tions never can be raised in this case ArrayIndexOutOfBoundsException and NullPointerException However notice that this is not the case for the exception TransactionException this exception can occur if for example the card holder decides to remove his card before the session is finished 17 5 Checking the specifications for the Electronic Purse After having discussed the general issues involved in writing specifications for smart card applications this section focuses on the actual specifications for the electronic purse As said before we wrote a formal specification using JML for most classes of the Gemplus electronic purse case study The majority of these specifications have been checked only with ESC Java but the specifications for the class Decimal have been verified completely using LOOP technology The next section discusses the LOOP verification in more detail this section presents the general ideas behind the specification and in particular it shows how relatively lightweight use of formal methods
23. ase distinction distinguishes all possible values of the variable condition as specified by the class invariant Thus the default clause will never be reached Again this is emphasized by our assert false annotation Notice that since the default clause never will be reached the method will never throw an exception as expressed by the exceptional postcondition In fact because of the class invariant it is possible to remove completely the throws clause from this method declaration Thus to summarize we would like to emphasize that many class invariants can be specified fairly easily they directly reflect the informal documentation and do not contain any complicated specification constructs Moreover they also can be checked efficiently Automatic checking techniques such as ESC Java can easily find places where invariants are violated Finally an additional advantage of properly specifying class invariants is that it allows to avoid unnecessary tests because objects are known to respect their class invariants 23 6 Focus on a single class the verification of Decimal Next we switch our attention to the specification and full verification of a sin gle class Decimal The specification and verification of the original Decimal class was done earlier 2 This section is about the specification and verifica tion of a modified Decimal class one that fulfills our wishes in terms of clearer shorter Java code and specifications that
24. ate annotations in the code For example a user might specify that some method argument should always be a non null reference 3 Thus by default this method has precondition requires true requires o null void p Object o void m Object o o jQ o n ESC Java checks whether o is not ESC Java finds no problem null requires true Fig 2 ESC Java example the requires clause of method m in Fig 2 When checking the method body the tool will then assume that this is actually the case thus the call o n in Fig 2 will not raise a null pointer exception but for every call to this method it will check whether the assumption actually holds thus ESC Java will warn for a potential problem in the call m x in method p in Fig 2 because it cannot ensure that x is non null ESC Java proceeds by generating verification conditions based on the annota tions and the code The verification conditions are sent to a dedicated theorem prover called Simplify ESC Java issues a warning if Simplify cannot estab lish the proof obligation However such a warning does not necessarily mean that the program is incorrect as both Simplify and the modeling of the Java semantics underlying ESC Java are unsound and incomplete The designers chose to accept this in order to keep simplicity and good performance of the tool Also if the tool does not issue any warning this does not necessarily mean that the program is correct
25. biguities in the documentation and e formally specifying class invariants which exist often implicitly in the programmer s mind allows to show the redundancy of tests on the well formedness of object states We will illustrate these aspects with some examples 5 1 Informal documentation vs formal specification Over time the electronic purse case study has been developed by several people trainees and employees of Gemplus Looking at the documentation and the implementation it is evident that these different developers have not always worked with the same ideas in mind For example in the class Decimal the informal documentation reads Two important notes about a decimal number it is limited to 32767 short representation and the decimal part must be done in the interval 000 999 This informal documentation immediately suggests that an appropriate class invariant would be the following where MAX_DECIMAL_NUMBER is 32767 and PRECISION is 1000 invariant O lt intPart amp amp intPart lt MAX_DECIMAL_NUMBER amp amp O lt decPart amp amp decPart lt PRECISION Notice that this class invariant is straightforward to write given the informal class documentation no difficult formalizations are needed However having T See http www sop inria fr lemme verificard electronic_purse 19 written this formal class invariant enables one to use the different JML tools to check whether this invariant is
26. cation Model Checking and Abstract Interpretation VMCAI 03 number 2575 in LNCS pages 26 40 Springer 2003 P Chalin JML support for primitive arbitrary precision numeric types Definition and semantics In Workshop on Formal Techniques for Java Programs FTfJP 2003 2003 Also available as Technical Report Concordia University 002 2a Differences between Esc Java and JML 2000 Comes with JML distribution in file esc jml diffs txt M D Ernst J Cockrell W G Griswold and D Notkin Dynamically discovering likely program invariants to support program evolution IEEE Transactions on Software Engineering 27 2 1 25 2001 10 ESC Java 2 http www cs kun nl sos research escjava 11 J C Filliatre Verification of non functional programs using interpretations in type theory Journal of Functional Programming 13 4 709 745 2003 12 C Flanagan K R M Leino M Lillibridge G Nelson J B Saxe and R Stata Extended static checking for Java In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI volume 37 5 of SIGPLAN Notices pages 234 245 ACM 2002 32 13 C Flanagan S Qadeer and S A Seshia A modular checker for multithreaded programs In E Brinksma and K G Larsen editors Computer Aided Verification CAV 02 number 2404 in LNCS pages 180 194 Springer 2002 14 VerifiCard Project homepage http www verificard org 15 M Hui
27. chose precision arithmetic An advantage is that the specification of the rest part becomes trivial The private specifi cation for the new mul is shown below requires 0 lt f amp amp f lt PRECISION amp amp O lt e amp amp e lt MAX_DECIMAL_NUMBER amp amp e 1 intPart 1 lt MAX_DECIMAL_NUMBER modifies decimal ensures decimal e old intPart PRECISION old intPart f e old decPart old decPart PRECISION signals Exception e false The only problem left is to write an implementation that conforms to this specification without overflow Note again that an implementation would be trivial same as the spec if Java Card would have integers The new code for mul is shown below void mul short e short f intPart decPart e f 27 intPart e O decPart e intPart f O decPart 0 f short a intPart short b decPart intPart short 0 decPart short 0 a xet 0O0 b e for short i short 0 i lt e i add a b a 0 f for short i short 0 i lt a i add short 0 f 0 b O f short al short b 100 short a2 short b al 100 10 short a3 short b al 100 a2 10 short di short al f 10 short d2 short a2 f 100 short d3 short a3 f 1000 short gross short di d2 d3 short e1 short a1l f di 10 100
28. conomically justified Thus it is important to find the right balance between completeness and reliability of a specification To illustrate this Fig 5 contains a heavyweight specification of remove Notification in class LoyaltiesTable The precise behavior of this method is not so important but what is important to see is that this method contains two loops one explicitly in the while statement and one implicitly in the call aid equals and the postcondition aims at describing precisely the intended behavior of these loops However in this case ESC Java is not able to establish whether the postcondition is correct one would need full verification using e g LOOP for this With respect to this we also would like to emphasize that even so called light weight specifications are useful because they describe exactly under which conditions no exceptions will occur For the correct functioning of a program unexpected exceptions are often a bigger threat than the risk of incorrect calculations Also programmers tend to pay more attention to the correctness of a computation than to whether it will handle all possible cases and will not throw an unexpected exception The work that is done in this case study illustrates how the tools that one has at hand influence the level of detail in the specifications Most of the speci fications have been checked with ESC Java so that one cannot rely on the correctness of postconditions for metho
29. d dif ficult to use There is a wide range of tools available that can be used to establish different properties of an implementation In general each tool uses its own specification language Thus with every new tool one has to under stand the techniques underlying theory and the specification language used And if one wishes to use different validation techniques on the same appli cation one has to adapt the specification accordingly each time This large overhead to apply new techniques makes industry reluctant to apply formal methods if they use formal methods at all then preferably with a single tool using a specification language that they master well Therefore a first step to make formal methods more accessible would be to have a single specification language and different tools that can match different aspects of this spec ification with an implementation These tools can then vary in their level of precision but also in their ease of use In general tools that are very precise and allow to check arbitrarily complicated specifications will need more user interaction than tools that check a limited subset of the specifications An interesting development in this direction is the JML project JML short for Java Modeling Language 19 20 is an annotation language for Java It allows one to write functional behavior specifications for Java programs using a Java like syntax JML is designed to be relatively easy to understand f
30. d using the add method because a and e are natural numbers For example a e is computed by for short i short 0 i lt e i add a 0 which means in English do e times add a The tricky part is the last multiplication in 1 namely 0 b x 0 f which is called the rest part Because b and f are less than 1000 we know that 0 b 0 f bx f 10 The result of bx f 10 is always less than 1 and because we are only interested in the 3 most significant digits out of 6 we want to calculate the truncated value of the rest part b f 10 which thus lies within 0 1000 This truncated value must then be stored in decPart A very reasonable solution is thus to write add O b f 1000 Unfortunately this is not possible in Java Card Arguments b and f are shorts and the result of their multiplication possibly does not fit in a short which is the biggest type available We also cannot write add 0 b 1000 1000 because in Java b 1000 is not always equal to b 1000 1000 due to premature rounding of b 1000 and 1000 Remember in Java 347 10 10 340 Gemplus circumvented the above problem in their mul method for which we wrote a specification 2 Unfortunately their calculation of the rest part is in precise The specification for a slightly simplified version of Gemplus s private mul is given below The original code 2 is not very relevant here The arguments of mul are
31. ds with complicated control structures or data manipulations such as removeNotification in Fig 5 Similarly for the addition and multiplication methods in the class Decimal ESC Java can not establish any postcondition other than true In contrast using the LOOP tool specifications describing the complete behavior of these two methods have been verified as discussed in Sect 6 4 1 2 Defensive vs offensive specifications Independently of the question how complete one s specifications should be one also has to decide whether to write defensive or offensive specifications An offensive method implementation requires that its input parameters are valid and correct It will not test whether this is the case it is up to the caller of the method to ensure it If the method is called with inappropriate param eters nothing can be guaranteed about its behavior In contrast a defensive 14 Offensive specification for m Defensive specification for m requires a null requires true ensures Q ensures Q signals E false signals E old a null void m int a void m int a F Fig 6 Offensive vs defensive specification method implementation does not make any requirements on its input parame ters before manipulating them it will check for their validity Typically it will throw an exception if the input is invalid or do some sort of error recovery e g replacing it by some default
32. ends clause For more information on depends and represents clauses and their use in modular ver ification we refer to the work of Leino 21 ESC Java provides a lightweight variation of model variables called ghost variables However since it is not possible to specify represents and depends clauses their use is limited To conclude this section Fig 1 shows part of the JML specification of the class Decimal from the case study at hand The class Decimal represents decimal numbers as composed of an integer and decimal part intPart and public class Decimal extends Object public static final short MAX_DECIMAL_NUMBER short 32767 public static final short PRECISION short 1000 spec_public private short intPart short 0 spec_public private short decPart short 0 invariant 0 lt intPart amp amp intPart lt MAX_DECIMAL_NUMBER amp amp O lt decPart amp amp decPart lt PRECISION represents decimal lt intPart PRECISION decPart depends decimal lt intPart decPart model int decimal behavior requires true modifies decimal ensures decimal v PRECISION signals DecimalException e v lt 0 amp decimal old decimal public Decimal setValue short v throws DecimalException if v lt 0 DecimalException throwIt DecimalException DECIMAL_OVERFLOW intPart v decPart short 0 return this Fig 1 Fragment of
33. er in fact we think they should be used both Given an implementation for large parts of a specification it might be sufficient to use static checking techniques to gain confidence in its correctness but for the crucial algorithms full verification is necessary However the effort needed for verification is actually reduced by using static checking beforehand because this can already identify the errors that are relatively easy to find The electronic purse case study that forms the basis for this work has been provided by Gemplus It has been developed by several trainees and later been extended by some members of the Gemplus research lab The case study is publicly available It is intended to be an example of a Java Card applet on which different formal methods could be tested Gemplus provides the applet without a formal specification the JML specifications are ours It was known beforehand that the code contained bugs but it gives a reasonable impression of how Java Card applets are structured The work done on this case study both with ESC Java and LOOP convinced smart card manufacturers to adopt JML and at least static checking in their development process This paper is structured as follows In the next section the language JML is introduced together with several tools using JML as input language In partic ular ESC Java and the LOOP tool are introduced Then Sect 3 gives more details about the electronic purse case study
34. ermediate pred icates in PVS is painstaking because one has to write these in terms of the semantic prelude Fortunately we can avoid constructing such a predicate in PVS by writing intermediate predicates in the Java code using in line JML as sertions The LOOP tool converts these assertions to intermediate predicates in terms of the semantic prelude Implementing support for in line assertions is part of the plan to reduce user interaction Apart from in line assertions there is also support for loop variants JML keyword decreasing and invari ants JML keyword maintaining The JML used by the LOOP compiler is a subset of JML We do for example not cover quantifications outside behav ior specifications The core of JML is supported though We also added some modifiers for JML assert statements assert saying whether the previous assert still holds 2 2 8 Other tools To illustrate the wide range of formal techniques that are available when one decides to use JML as specification language we briefly survey several other tools that use JML as specification language When the development of JML started it was intended to be used with a runtime assertion checker as advocated in the Design by Contract approach in Eiffel 25 The JML tool which is developed at Iowa State University does exactly this it translates annotations into runtime checks When running the translated code on example input every time an assertion is violated an
35. f Hoare logic and Weakest Precondition reasoning Suitable intermediate pred icates are inserted as JML assertions in the method body not shown and proved The two for loops require appropriate in variants not shown A 32 bit bounded representation for Java s numeric types has been used see 16 in the translations of both Java and JML expressions The semantics of 16 bit Java Card is preserved because in the code no integer types are declared and all casts are explicit 6 2 Integral semantics in specifications By evaluating all JML expressions in a bounded integral representation over flow can occur in specifications It is an issue under debate in the JML com munity what the right semantics of integral types in specifications should be see 7 Ideally one would want to use the unbounded mathematical inte gers in specifications This has the advantage that one does not have to worry about overflow in specifications The disadvantage is that by using two differ ent kinds of integral semantics expressions can have different values in Java and JML for example Integer MAX_VALUE 1 Integer MIN_VALUE is true in Java but false in unbounded JML The mul method specified and verified in the previous subsection is invoked by a public mul method which has a Decimal object d as argument instead of two shorts Its post condition can be written completely in terms of model fields decimal and d decimal requires d null
36. g 3 Java source code and associated JML specifications are fed into the LOOP compiler which generates PVS code The Java source code is translated to PVS logical theories which are based on the handwritten semantic prelude This prelude defines sequential Java in all its details The JML specifications are translated into PVS predicates The aim is to show that the predicates generated from the JML annotation hold for the translated Java source code The actual interactive verification work thus takes place inside PVS In the LOOP translation of Java methods to PVS theories the structure of the methods remains intact While proving we can therefore step through the method body using different techniques The following list gives an overview of available techniques for proving the correctness of a method given its spec ification 1 All Java language constructs have appropriate Hoare rules associated with them 18 All these rules are proved correct in terms of the un derlying semantics The Hoare rules are used to split up the proof obli gation in several smaller proof obligations For example the Hoare rule for composition splits up the proof obligation in two parts The down side of reasoning with Hoare rules is that they require user interaction The Hoare rule for composition needs an intermediate predicate which is the post condition for the first statement and the pre condition for the second one 2 To avoid excessive use
37. integration of tools around JML and addressing scalability issues especially for interac tive tools such as LOOP 31 References 1 E Bretagne A El Marouani P Girard and J L Lanet Pacap purse and loyalty specification Technical Report V 0 4 Gemplus 2000 C Breunesse B Jacobs and J van den Berg Specifying and Verifying a Decimal Representation in Java for Smart Cards In H Kirchner and C Ringeissen editors Algebraic Methodology And Software Technology AMAST 02 number 2422 in LNCS pages 304 318 Springer 2002 L Burdy Y Cheon D Cok M Ernst J Kiniry G T Leavens K R M Leino and E Poll An overview of JML tools and applications In Th Arts and W Fokkink editors Formal Methods for Industrial Critical Systems FMICS 03 number 80 in ENTCS Elsevier Amsterdam 2003 www elsevier nl locate entcs volume80 html L Burdy A Requet and J L Lanet Java Applet Correctness a Developer Oriented Approach In Formal Methods FME 03 number 2805 in LNCS pages 422 439 Springer 2003 N Catano and M Huisman Formal specification and static checking of Gemplus s electronic purse using ESC Java In L H Eriksson and P A Lindsay editors Formal Methods Europe FME 02 number 2391 in LNCS pages 272 289 Springer 2002 N Cata o and M Huisman Chase a Static Checker for JML s Assignable Clause In L D Zuck P C Attie A Cortesi and S Mukhopadhyay editors Verifi
38. is defined Two fields of type short are used for storage When storing value 3 493 the floored value 3 is put in field intPart and the rest value as whole number 493 is stored in field decPart Negative numbers are not allowed This information is reflected in the class invariant invariant O lt intPart amp amp intPart lt MAX_DECIMAL_NUMBER amp amp O lt decPart amp amp decPart lt PRECISION To ease reasoning an abstract field is added to the Decimal class specification to denote the stored value The value of the abstract field has a one on one relationship with intPart and decPart denoted by its represents clause 10 They are not allowed in our version Whether or not they could occur in the original version of Gemplus remains unclear see Sect 5 1 24 repeated here for convenience model int decimal represents decimal lt intPart PRECISION decPart This so called representation function is a function over the instance vari ables intPart and decPart The abstract value of 3 493 is equal to 3493 Out of the 40 members that make up Decimal in the next subsection we give an outline of the specification and verification of only one method the one that multiplies decimals This method is interesting because it is the most complicated one and because its original implementation is incorrect Fur thermore it uses Java rounding tricks which give us the possibility to sh
39. maintained everywhere This is useful because from the implementation of the class it becomes clear that not all developers have adhered to this design decision about decimal numbers For example having this formal invariant allows one to detect immediately that there is a problem with the method oppose public Decimal oppose intPart short intPart decPart short decPart return this This method should not be declared public because it can break the class invariant by making intPart and decPart negative Having a formal class specification instead of informal documentation only cannot avoid all inconsistencies For example the class Decimal also contains methods isPositif and isNegatif which denote whether the value is pos itive or negative respectively Since these methods do not break the class invariant one does not immediately detect that they are useless given the informal documentation However using the different JML tools it is easy to show that the results of these methods actually are constant values and thus that these methods do not give any new information For example the method isNegatif can be specified as follows ensures result false public boolean isNegatif return compareTo short 0 lt short O Formal specifications do not only help to maintain an implementation over time but because of their precise semantics they can also help to avoid the ambiguities
40. n example we discuss the method arrayCopy of the Java Card API requires src null amp srcOff gt 0 amp srcOff length lt src length amp dest null amp destOff gt 0 amp destOff length lt dest length amp length gt 0 modifies dest ensures forall int i i lt 0 amp i lt dest length gt destOff lt i amp i lt xdestOfftlength dest i src srcOff i destOff dest i old dest i ensures result destOff length signals TransactionException e e _reason TransactionException BUFFER_FULL amp JCSystem _transactionDepth 1 signals NullPointerException false signals ArrayIndexOutOfBoundsException false e9eOOO8O0O0O8O 0CO OC Oe public static final native short arrayCopy byte src short srcOff byte dest short destOff short length throws ArrayIndexOutOfBoundsException NullPointerException TransactionException The method arrayCopy copies length bytes located at position srcOff in array src to position destOff in destination array dest The precondition for this method requires that src and dest have the right size and that the num ber of bytes for copying is a positive number The postcondition specifies that if the method terminates without raising any exception then the method will have copied length bytes from src starting in the position srcOff to dest starting in the position destOff Otherwise the method terminates abruptly raising an exception of type Tr
41. n or general structure However writing formal specifications forces one to think carefully about the code and often it makes one aware of possibilities for improvement Therefore the verifications in the next section are actually done on an improved version of the class Decimal Since most of the specifications are checked only with ESC Java we can not have unlimited trust in their correctness Therefore we aimed at writing specifications that were as heavy as possible but where we still could feel confident in the outcome of the tool The full annotations with an overview 18 of remaining warnings are available on a web site Typically if one wishes to do full verification on fragments of the code the remaining warnings and the methods containing loops or recursion are the most interesting i e they are the most likely to still contain errors When checking the specifications one is often forced to work in a bottom up manner First one has to annotate the classes that are at the bottom of the class hierarchy and that are used by many of the other classes e g in this case study the utility classes Afterwards using these specifications one can go up higher in the class hierarchy We found that writing and checking the formal specifications in particular was important for the following two reasons e formal specifications help to maintain the consistency between documenta tion and implementation and to avoid am
42. ns of shared interfaces the standard mechanism of communication between applets When the purse applet wishes to call a method of a loyalty applet it requests the loyalty applet for an object implementing the loyalty shareable interface The loyalty applet then decides whether to give the purse a reference to such a shareable interface object The card issuer applet keeps information of the card holder such as name and identifier and PIN code which is necessary to initialize the card The purse applet implements the basic operations of credit debit and cur rency change and also implements mechanisms for installing selection and de selection of the applet The purse applet interacts with loyalty applets in such a way that whenever the card holder has made a purchase the loyalty ap plet can use this information to increase an internal counter of loyalty points These loyalty points can be used later to make purchases The purse applet keeps track of the balance of the purse the transactions done by the purse the different currency changes that have taken place and the different loyalty programs that the card holder is subscribed to Certain op erations can be done only for a restricted set of users which can be recognized for instance by requiring a PIN code The purse applet defines the different ac cess conditions and also binds these access conditions to operations So when the card holder wishes to do some operation the purse applica
43. oped at INRIA Rocquen court It uses the Why tool 11 to generate verification conditions as Coq proof obligations 3 The Gemplus electronic purse The Gemplus electronic purse is a smart card application that has been devel oped to serve as a realistic example for researchers working on formal methods for the Java Card platform 1 However it is too big to fit on most of the cards that are currently available Any Java Card application consists of two parts the terminal side imple menting the configuration and communication functionalities and the card side implementing the Java Card application itself see Fig 4 These two sides communicate with each other by sending APDU Application Protocol Data Unit messages which is an ISO standard defining the way in which commands and data are structured In Java Card the APDU is a class with a member of type byte array containing the raw data On the card side the electronic purse provides the card holder with banking 5 In fact Jive does not use JML but it uses a JML like language 11 2 Loyalty applets Shared f APDU interfaces Card issuer applet lt gt terminal side messages Purse applet Fig 4 The electronic purse functionalities such as credit debit and currency change The card side of the purse application contains three kinds of applets loyalty applets the card issuer applet and the purse applet These applets communicate with each other by mea
44. or an experienced Java programmer In fact by now JML has become the de facto standard source code level specification language for functional behavior of Java programs in the academic community As a result more and more tools that aim at the verification of Java programs are adopting JML as property specification language see 3 for an overview This paper reports on work done in this context using different tools on parts of a single JML specification For a single applet consisting of 42 classes and 432 kB in total of code and documentation a specification has been writ ten in JML The specification for this applet has been checked using ESC Java 22 12 a tool for automatic static checking of Java programs aiming at finding efficiently the most common program errors Parts of the specification and implementation also have been verified within the LOOP project 23 a project that aims at full verification of Java programs using interactive theo rem proving The LOOP approach has been applied to some algorithms that manipulate data in an intricate way and whose verification falls completely out of the scope of ESC Java and other automatic tools Elsewhere the authors have reported on the individual case studies in two separate papers 2 5 with two separate tools but here we want to show how the different techniques complement and contribute to each other in a natural way We do not want to argue that a certain approach is bett
45. ow our LOOP techniques w r t reasoning with bounded arithmetic Last but not least it shows the need of unbounded integral types in specifications which is further discussed in Subsect 6 2 Method mul uses method add to produce its result The specification of add is shown below Details about its verification can be found elsewhere 2 requires 0 lt f amp amp f lt PRECISION amp amp O lt e amp amp e lt MAX_DECIMAL_NUMBER amp amp e intPart 1 lt MAX_DECIMAL_NUMBER modifies decimal ensures decimal old decimal e PRECISION f signals Exception e false x private void add short e short f Arguments e and f contain respectively the integer and decimal part of the number to add Because the argument to add is not a Decimal object the pre condition explicitly describes to which bounds e and f must adhere For Decimal objects these same bounds are described in the invariant 6 1 Implementation and specification of mul Multiplication of decimals is difficult because of rounding Suppose we have two Decimal objects which represent decimal numbers a b and e f where a and e are the corresponding values of intPart and b and f are the corresponding values of decPart Mathematically speaking multiplication of a b and e f can be written as the sum of 4 simpler multiplications a bxe f axe ax0 f 0 b e 0 5 0 f 1 25 The first three of these multiplications can be compute
46. ps to maintain the consis tency of an implementation over time and to avoid ambiguities When design decisions such as restricting the possible range of a variable are specified for mally each time the implementation is modified the various JML tools can be used to check whether the design decisions have not been violated And if they are violated one is forced to decide whether the design decision or the implementation has to be changed Notice that many of these violations can be detected by automatic tools thus they can be found with quick checks over and over again during the development process 5 2 Class invariants In fact class invariants do not only serve to formally specify certain design decisions they can also be used as a formal motivation that certain tests are unnecessary To illustrate this we consider the method setTaux also from the class Transaction void setTaux Decimal tx throws ISOException try taux setValue tx 8 Notice that there exist several programming languages in which this class invari ant could be described precisely using enumeration types Violations are then found immediately by type checking 9 Tauz is the French word for rate 21 catch DecimalException e assert false ISOException throwIt PurseApplet DECIMAL_OVERFLOW F This method has a parameter tx which is an instance of class Decimal Thus we know that tx respects the class invariant for Decimal a
47. r interaction several Weakest Precondition WP techniques 17 can be applied to enable automatic proofs of non recursive programs Like the Hoare rules the Weakest Precondition rules are also proved correct in terms of the underlying Java semantics 3 When a proof is completely split up and decomposed after applying Hoare or Weakest Precondition rules the remaining proof obligations if any must be verified by semantic rules and logical deduction These se mantic rules are either generated by the LOOP compiler or present in the semantic prelude 15 The semantic rules describe the actual Java semantics Applying these rules eventually brings a Q E D or an un provable formula The three proof methods above are used in combination Sometimes a method body is too long to be handled by WP PVS might fail due to lack of resources The body is then split up by Hoare rules When a proof obligation is on the granular level i e assignments we revert to using semantic rules Because the whole system is sound modulo the soundness of PVS and the handwritten semantic prelude of course specifications verified by LOOP can be trusted The biggest downside of doing such heavyweight verification work is the cost of user interaction For example when applying the Hoare rule for composition on statement s1 s2 an intermediate predicate has to be constructed to serve as a post condition for s1 and a pre condition for s2 Constructing int
48. s specified The method then assigns tx to the instance variable taux using the setValue method of the class Decimal Since this method can throw an exception the call to setValue is put in a try catch statement However given the spec ification of setValue and since the argument tx is a legal instance of class Decimal respecting its invariant we can actually prove that this exception will never be thrown This is emphasized by the assert false annota tion which means that this part of the program text will never be reached In fact because of the class invariant of Decimal we can give the following method specification for setTaux requires tx null modifies taux intPart taux decPart ensures taux intPart tx intPart ensures taux decPart tx decPart signals ISOException false Notice in particular that we do not have to specify any conditions on tx int Part or tx decPart it is sufficient that we know that tx respects its class invariant As another example on the use of class invariants we consider the class AccessCondition The electronic purse is implemented in such a way that certain operations only can be performed when the card is in a particular state The class AccessCondition implements operations to check whether the card is in the appropriate state Following the documentation of the elec tronic purse there is a variable condition which can have only one of the following constant values
49. sman Reasoning about Java Programs in Higher Order Logic with PVS and Isabelle PhD thesis University of Nijmegen 2001 16 B Jacobs Java s integral types in PVS In E Najim U Nestmann and P Stevens editors Formal Methods for Open Object Based Distributed Systems FMOODS 2008 number 2884 in LNCS pages 1 15 Springer 2003 17 B Jacobs Weakest precondition reasoning for Java programs with JML annotations Journal of Logic and Algebraic Programming 58 1 2 61 88 2004 18 B Jacobs and E Poll A logic for the Java Modeling Language JML In H Hussmann editor Fundamental Approaches to Software Engineering FASE 2001 number 2029 in LNCS pages 284 299 Springer 2001 19 G T Leavens A L Baker and C Ruby Preliminary design of JML a behavioral interface specification language for Java Technical Report 98 06i Iowa State University Department of Computer Science 2000 20 G T Leavens E Poll C Clifton Y Cheon and C Ruby JML reference manual http www jmlspecs org jmlrefman 21 K R M Leino Toward Reliable Modular Programs PhD thesis California Institute of Technology 1995 22 K R M Leino G Nelson and J B Saxe ESC Java user s manual Technical Report SRC 2000 002 Compaq System Research Center 2000 23 The LOOP project http www cs kun nl sos research loop 24 C March C Paulin Mohring and X Urbain The Krakatoa tool for JML Java program certification
50. the annotated class Decimal decPart respectively As JML does not allow to include private fields in public specifications we add spec_public immediately before the declarations of these two fields This keyword causes the fields to be included in the scope of every specification The class invariant restricts the possible values of these variables intPart is a positive number less than the constant MAX_DECIMAL_NUMBER the maximal value of a short while decPart ranges between 0 and the constant PRECISION The value of PRECISION is 1000 thus the class Decimal will represent decimal numbers up to three decimal places To denote the value of the decimal number represented a model variable decimal has been declared The value of this variable depends on intPart and decPart and the represents clause shows how As an example we show the specification of the method setValue which takes a single argument v and as a result sets the decimal number to represent v 000 We do not explicitly specify any precondition for this method it is a defensive specification as discussed in Sect 4 The method may modify decimal thus implicitly it may modify the variables intPart and decPart If the method terminates normally the value of decimal is set appropriately and because of the represents clause and the class invariant this implies that decPart and intPart are set appropriately If the method terminates abruptly with a DecimalException
51. tion will check whether the card holder has the appropriate permissions Finally the electronic purse contains several classes implementing crypto graphic concepts In this case study we did not study this 4 Specifications for Smart Card Applets When writing behavioral specifications several issues concerning the style of specifications have to be considered Notice that many of these issues are relatively independent of the typicalities of smart card applications However 12 requires aid null modifies data ensures forall int i 0 lt i amp i lt nbLoyalties gt forall int k 0 lt k amp k lt data i aid length gt datali aid k aid theAID k gt data i logfullInformation void removeNotification AID aid byte i 0 while i lt nbLoyalties AllowedLoyalty al datal i if al getAID equals aid al dontKeepInformed else i Fig 5 Example heavyweight specification the choices that we make often are influenced by the application domain The first subsection discusses several of these issues and explains our choices for this case study The second subsection discusses the existing specifications for the Java Card API 4 1 Specification style 4 1 1 Lightweight vs heavyweight specifications The first point one has to decide upon is how heavy a specification should be That is does one just want to specify under which conditions
52. to the return value This keyword can only be used in ensures clauses One can refer to the value of an expression F in the pre state before method body execution by writing olda E This keyword can be used both in the ensures and signals clauses Keyword old is used to see how an expression differs from its original value Finally to have a higher level of abstraction in specifications JML allows one to declare so called model variables These are variables that exist only at the level of the specification Declarations of model variables have the same format as declarations of normal variables but are preceded by the keyword model Model variables can be related to concrete variables or other model variables by represents and depends clauses A represents clause specifies how the value of a model variable can be calculated from the values of the concrete variables A depends clause only specifies on which concrete variables the value of the model variable depends Hence if all the concrete variables in the depends clause are unchanged one can assume that the value of the model variable is also unchanged and if the model variable may be modified the concrete variables implicitly also may be modified If a represents clause is given the information in the depends clause is redundant However since often it is not possible to give the represents clause for example when speci fying an abstract class it is useful to also have the dep
Download Pdf Manuals
Related Search