On JML: topics in tool-assisted verification of Java programs
Cees-Bart Breunesse · Radboud Repository (Radboud University) · 2006
Background meant to strengthen the position of Europe in information technology For Nijmegen, the Veri-fiCard project was an opportunity to continue the work in the LOOP project the author of this thesis was funded by the VenfiCard project One of the project's goals was to develop methods and tools for the specification and verification of Java Card applets and to evaluate these methods using the case studies provided by the industrial partners in the project Several universities, research labs and a smart card manufacturer worked together in the VenfiCard project In Nijmegen we focused on source code verification and specification, other partners looked at byte code verification, security and confidentiality properties, and platform (virtual machine) verification The work presented in this thesis is a result of the VenfiCard project, but would be impossible without the prior work done in the LOOP project Contents of this thesisWe now give a description of the contents of each chapter in this thesis Chapter 2: BackgroundChapter 2 introduces the required background needed to understand the rest of the thesis this includes the semantics of Java, Java Card, and JML The source code verification in the LOOP project is performed using the theorem prover PVS developed at SRI, an independent research institute PVS provides mechanized support for formal specification and verification The specification language of PVS is based on classical, typed higher-order logic The PVS theorem prover provides a collection of powerful primitive inference procedures that can be applied interactively and automatically The initial goal in the early days of the LOOP project was to dehne a formal semantics of Java This semantics was given by a shallow embedding of sequential Java in the higher-order logic of PVS Once this semantics was defined, it seemed logical to attempt program verification taking the formal semantics of Java in PVS as a basis A compiler was developed that takes a Java program as input, and outputs the translation of that Java program in terms of the semantics of Java in PVS Desired properties of the Java program were then specified in PVS, after which a proof could be attemptedThe downside of specifying properties of Java programs in PVS is that this is not easily readable and a great deal of knowledge of the semantics of Java in PVS is needed to read and understand it This means that software engineers can only annotate their program with formal specifications when they have expert knowledge of a verification tool The appearance of JML provided an interesting alternative approach JML allows programmers to write formal specification in a Java-like syntax This has as greatest benefit that formal specifications become readable (and writable) for the average programmer Another advantage of JML is that the grammar is close to Java which makes it relatively easy to implement as a spécification language in other tools Thismeans that the same specification and code could now be checked by different tools In the LOOP approach, two steps were taken to adopt JML firstly, the semantics of JML was formalized in PVS, and secondly, the LOOP compiler was adapted to handle specific JML syntax Formally specifying the semantics of JML is ongoing work, which this thesis is a part of In Chapter 2 the semantics of method specifications is defined by means of Hoare triples Hoare triples play an important role in LOOP verifications a Java method and its specification are trans lated to a Hoare triple This Hoare triple for the entire method can then be split up in Hoare triples for smaller parts of the program using traditional Hoare [22] and weakest precondition 117| rules An advantage of LOOP over some other formal verification approaches is that all our Hoare and weakest precondition rules are proved correct with relation to our semantics of Java The LOOP approach consists of a compiler and many PVS files describing the semantics of Java and JML This thesis does not describe the many changes and adaptations the author made to the compiler and PVS files in full detail Many changes were made in the semantics of JML, meaning that a lot of time and effort was put in creating and optimizing PVS hies Furthermore, the compiler was heavily adapted by the author to cope with JML inline assertions Chapter 3: Λ semantics of model variablesThis chapter is about the semantics of the most important abstraction mechanism provided by JML The importance of abstraction is recognized for a long time already In 1972 Hoare pub lished his paper titled "Proof of Correctness of Data Representations" [211 in which he argues that programmers should write abstract programs working on abstract datastructures from which concrete programs can be derived automatically We are not so much interested in automatic program derivation, but we are interested in abstract specifications Specifications need to be abstract for several reasons • Specifications describe "what" but not "how" By using an abstract representation one is not distracted by implementation details • Specifications of classes may be used in other classes This is the so called implementorchent or producer-consumer model A class supplies a specification and an interface to an implementation on the basis of which a consumer decides how to use this class If the specifications show too many implementation details, these specifications lack robustness, and are too close to a specific implementation This implementation cannot be changed for another, perhaps more efficient, implementation without rewriting the specification as well, which is bad practice Furthermore, specifications serve as a contract between the implementing class and the consumer class abstract specifications enable us to hide many confusing and irrelevant implementation details from consumers The most important abstraction mechanism that JML provides is the use of model fields in spec ifications Model fields in JML specifications look like normal Java fields, but they have a dif ferent semantics Assignments to model fields are not allowed This does not mean that model 4 fields cannot have a value a model field can be associated with a representation function, as in [21J This representation function expresses the value of the abstract model field in terms of the concrete representation Specifications with model fields bring along a whole range of new possibilities, but also new problems, which we discuss in Chapter 3 Chapter 4: Λ semantics of Java and JML integral types The semantics of JML expressions is very close to Java expressions In particular, JML uses the Java integral types Java integral types are bounded they are 8,16,32, or 64 bit integers for types byte, short, int, and long, respectively In some cases, using these bounded integral types in specifications is very awkward or even confusing, an issue first noted by Patrice Chahn [15] Chapter 4 discusses the integration of the normal mathematical integers (i e elements of type Z) in JML and Java Their integration is not trivial, and we have not been the only research group investigating this topic The first two proposal extensions of JML with type Ζ were called JMLd and JMLb [15], both created by Patrice Chalin Our own proposal is called JMLc, which has the same syntax and almost the same semantics as JMLb, but has a different design philosophy In Chapter 4 we discuss JMLc and the difference with JMLb and JMLa Chapter 5: Decimal class case study This chapter discusses a Java Card case study which is relevant from the perspectives of both model fields (Chapter 3) and integral types (Chapter 4) The case study was provided in the VenfiCard project by Gemplus, a member of the End User Panel The case study is a fully oper ational Java Card electronic purse Other participants analysed this case study as well, resulting in a joint paper [13] with Nestor Calano and Marieke Huisman covering the entire case study In Chapter 5 we focus only on a small, but important, portion of the electronic purse the Decimal class We do not consider the entire case study, because specifying and verifying the entire case study is too much work with the LOOP approach The Decimal class is used to represent deci mal numbers for example, the global balance of the electronic purse is a Decimal object The Decimal class case study is important from both the perspectives of model fields and integral types Therefore, lessons learned in Chapter 3 and Chapter 4 are applied in Chapter 5 Chapter 6: Conclusions This chapter evaluates the achievements and shortcomings of the LOOP project Is the LOOP approach of software verification the way to go, or do we need other techniques to scale up software verification to industrial size 9In this thesis, we use a language very similar to PVS [38], which we call pseudo-PVS, to describe the semantics of Java and JML.The main difference of pseudo-PVS compared to PVS is that we prefer to use mathematical characters wherever possible to increase readability.In this section we present pseudo-PVS by means of some examples.It is by no means an exhaustive demonstra tion of what is possible with (pseudo-)PVS, but sufficient to understand the pseudo-PVS code snippets throughout the rest of the thesis.Keywords of pseudo-PVS are always shown in an upright non-slanted font, everything else is shown in a slanted font.