×

Source code verification of a secure payment applet. (English) Zbl 1066.68005

Summary: This paper discusses a case study in formal verification and development of secure smart card applications. An elementary Java Card electronic purse applet is presented whose specification can be simply formulated as “in normal operation, the applet’s balance field can only be decreased, never increased”. The applet features a challenge-response mechanism which allows legitimate terminals to increase the balance by putting the applet into a special operation mode. A systematic approach is used to guarantee a secure flow of control within the applet: appropriate transition properties are first formalized as a finite state machine, then incorporated in the specification, and finally formally verified using the Loop translation tool and the PVS theorem prover.

MSC:

68M12 Network protocols

Software:

Casper; FDR2; JML; LOOP; PVS; ESC/Java
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Anderson, R., The formal verification of a payment system, (Hinchey, M. G.; Bowen, J. P., Industrial Strength Formal Methods (1999), Springer-Verlag), 43-52
[2] van den Berg, J.; Jacobs, B., The LOOP compiler for Java and JML, (Margaria, T.; Yi, W., Tools and Algorithms for the Construction and Analysis of Software (TACAS). Tools and Algorithms for the Construction and Analysis of Software (TACAS), LNCS, vol. 2031 (2001), Springer-Verlag), 299-312 · Zbl 0978.68708
[3] van den Berg, J.; Jacobs, B.; Poll, E., Formal specification and verification of Java Card’s application identifier class, (Attali, I.; Jensen, T., Java on Smart Cards: Programming and Security (JavaCard Workshop 2000). Java on Smart Cards: Programming and Security (JavaCard Workshop 2000), LNCS, vol. 2041 (2001), Springer-Verlag), 137-150 · Zbl 0980.68685
[4] C.-B. Breunesse, J. van den Berg, B. Jacobs, Specifying and verifying a decimal representation in Java for smart cards, in: Algebraic Methodology and Software Technology, LNCS, Springer, Berlin, in press; C.-B. Breunesse, J. van den Berg, B. Jacobs, Specifying and verifying a decimal representation in Java for smart cards, in: Algebraic Methodology and Software Technology, LNCS, Springer, Berlin, in press
[5] R. Brinkman, J.-H. Hoepman, Secure method invocation in Jason, in: Proceedings of Cardis 2002, pp. 29-40 (USENIX Assoc., 2002); R. Brinkman, J.-H. Hoepman, Secure method invocation in Jason, in: Proceedings of Cardis 2002, pp. 29-40 (USENIX Assoc., 2002)
[6] Burrows, M.; Abadi, M.; Needham, R., A logic of authentication, Proc. Royal Soc. Series A, 426, 233-271 (1989) · Zbl 0687.68007
[7] Chen, Z., Java Card Technology for Smart Cards: Architecture and Programmer’s Guide (2000), Addison-Wesley, June
[8] Ernst, M. D.; Cockrell, J.; Griswold, W. G.; Notkin, D., Dynamically discovering likely program invariants to support program evolution, IEEETSE, 27, 2, 99-123 (2001)
[9] Flanagan, C.; Leino, K. R.M.; Lillibridge, M.; Nelson, G.; Saxe, J. B.; Stata, R., Extended static checking for Java, (in: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). in: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), SIGPLAN Notices, vol. 37 (2002), ACM), 234-245
[10] Formal Systems (Europe) Ltd., Failures-Divergence Refinement, FDR2 user manual, May 2000; Formal Systems (Europe) Ltd., Failures-Divergence Refinement, FDR2 user manual, May 2000
[11] Global Platform, Open platform card specification version 2.1, June 2001. Available from <>; Global Platform, Open platform card specification version 2.1, June 2001. Available from <>
[12] Haneberg, D.; Reif, W.; Stenzel, K., A method for secure smartcard applications, (in: Proceedings of AMAST 2002. in: Proceedings of AMAST 2002, LNCS, vol. 2422 (2002), Springer-Verlag), 319-333
[13] E. Hubbers, M. Oostdijk, E. Poll, From finite state machines to provably correct Java Card applets, in: Proceedings of the 18th IFIP Information Security Conference, Kluwer Academic Publishers, in press; E. Hubbers, M. Oostdijk, E. Poll, From finite state machines to provably correct Java Card applets, in: Proceedings of the 18th IFIP Information Security Conference, Kluwer Academic Publishers, in press
[14] Huisman, M.; Jacobs, B., Java program verification via a Hoare logic with abrupt termination, (Maibaum, T., Fundamental Approaches to Software Engineering (FASE’00). Fundamental Approaches to Software Engineering (FASE’00), LNCS, vol. 1783 (2000), Springer-Verlag), 284-303
[15] B. Jacobs, Weakest precondition reasoning for Java programs with JML annotations, J. Logic Algebraic Program., this issue; B. Jacobs, Weakest precondition reasoning for Java programs with JML annotations, J. Logic Algebraic Program., this issue
[16] B. Jacobs et al., Reasoning about classes in Java (preliminary report), in: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), ACM Press, 1998, pp. 329-340; B. Jacobs et al., Reasoning about classes in Java (preliminary report), in: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), ACM Press, 1998, pp. 329-340
[17] Leavens, G. T.; Baker, A. L.; Ruby, C., JML: a notation for detailed design, (Kilov, H.; Rumpe, B.; Harvey, W., Behavioral Specifications for Businesses and Systems (1999), Kluwer Academic Publishers), 175-188
[18] G.T. Leavens, A.L. Baker, C. Ruby, Preliminary design of JML: a behavioral interface specification language for Java, Techn. Rep. 98-06q, Dep. of Comp. Sci., Iowa State Univ., 2002. Available from < >; G.T. Leavens, A.L. Baker, C. Ruby, Preliminary design of JML: a behavioral interface specification language for Java, Techn. Rep. 98-06q, Dep. of Comp. Sci., Iowa State Univ., 2002. Available from < >
[19] Lowe, G., Casper: a compiler for the analysis of security protocols, J. Comp. Security, 6, 53-84 (1998)
[20] R. Marlet, D. Le Métayer, Security properties and Java Card specificities to be studied in the SecSafe project, Technical Report SECSAFE-TL-006, Trusted Logic, August 2001; R. Marlet, D. Le Métayer, Security properties and Java Card specificities to be studied in the SecSafe project, Technical Report SECSAFE-TL-006, Trusted Logic, August 2001
[21] W. Mostowski, Rigorous development of JavaCard applications, in: T. Clarke, A. Evans, K. Lano (Eds.), Proceedings of the Fourth Workshop on Rigorous Object-Oriented Methods, London, 2002; W. Mostowski, Rigorous development of JavaCard applications, in: T. Clarke, A. Evans, K. Lano (Eds.), Proceedings of the Fourth Workshop on Rigorous Object-Oriented Methods, London, 2002
[22] S. Owre, N. Shankar, J.M. Rushby, D.W.J. Stringer-Calvert, PVS System Guide, Computer Science Laboratory, SRI International, Menlo Park, CA, USA, September 1999. Available from <>; S. Owre, N. Shankar, J.M. Rushby, D.W.J. Stringer-Calvert, PVS System Guide, Computer Science Laboratory, SRI International, Menlo Park, CA, USA, September 1999. Available from <>
[23] Poll, E.; van den Berg, J.; Jacobs, B., Specification of the Java Card API in JML, (Domingo-Ferrer, J.; Chan, D.; Watson, A., Fourth Smart Card Research and Advanced Application Conference (CARDIS’2000) (2000), Kluwer), 135-154
[24] Poll, E.; van den Berg, J.; Jacobs, B., Formal specification of the Java Card API in JML: the APDU class, Comp. Network., 36, 4, 407-421 (2001)
[25] The Krakatoa team, The proof tool, 2002. Available from < >; The Krakatoa team, The proof tool, 2002. Available from < >
[26] European IST-2000-26328 Project VerifiCard. Available from <>; European IST-2000-26328 Project VerifiCard. Available from <>
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.