The Demoney Case Study

Abstract

So far in this book no specific Java Card examples have been discussed, apart from very simple transactions related examples in Chapter 9. In this chapter we are going to discuss how the KeY system is used to verify real world Java Card programs. The basis and running example for this chapter is the demonstrative Java Card electronic purse application Demoney provided by

Trusted Logic S.A. The purpose of this chapter is not to present full specifications for Demoney and a thorough verification procedure, or give a tutorial on using the KeY system verification facilities ($\Rightarrow$ Chap. 10). Rather, we will discuss general problems associated with Java Card verification attempts: provide advice on what to specify about Java Card applets, how to specify it using different specification languages, and give the reader hints necessary to perform efficient verification of his or her own Java Card applets. Verifications that we are going to discuss were performed on an absolutely unmodified source code of Demoney, thus, the context of this chapter is slightly different from the rest of the book—we do not consider the use of formal methods during the development process, instead we show how one can verify preexisting, legacy Java Card code, in other words, perform post-hoc verification. We also assume that, to a certain extent, the reader is familiar with Java Card technology, described by Chen [2000] ($\Rightarrow$ Chap. 9).

In the next section we present the Demoney application in more detail, in Section 14.3 we discuss different specification techniques and languages available in the KeY system, their advantages and disadvantages in the context of Demoney verification. Section 14.4 discusses modular verification and the use of method contracts in proofs, which is necessary to make the verification process scalable. Then in Section 14.5 different properties related to Java Card applets are presented, example specifications are given based on Demoney and verification is discussed. Finally, Section 14.6 summarises this chapter.