Abstract
The new Gemplus smart card is based on the Java technology, embedding a virtual machine. The security policy uses mechanisms that are based on Java properties. This language provides segregation between applets. But due to the smart card constraints a byte code verifier can not be embedded. Moreover, in order to maximise the number of applets the byte code must be optimised. The security properties must be guaranteed despite of these optimisations. For this purpose, we propose an original manner to prove the equivalence between the interpreter of the JVM and our Java Card interpreter. It is based on the refinement and proof process of the B formal method.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: The B Book. Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Cohen, Defensive Java Virtual Machine, http://www.cli.com/software/djvm
Freud, S.N., Mitchell, J.C.: A type System for Object Initializatio In the Java Byte Code Language, http://theory.standford.edu/~freunds
Golberg, A.: A Specification of Java Loading and Bytecode Verification Kestrel Institute (December 1997), http://www.kestrel.edu/HTML/people/goldberg/
Hartel, P., Butler, M., Levy, M.: The operational semantics of a Java Secure Processor
Qian A formal specification of Java Virtual Machine Instruction. Technical Report (abstract), Universitat Bremen (1997), http://www.informatik.unibremen.de/~qian/abs-fsjvm.html
Stata, R., Abadi, M.: A Type System for Byte Code Subroutines. In: Proc. 25th ACM Symposium on Principles of Programming Language (January 1998)
Yellin, F., Lindholm, T.: The Java Virtual Machine Specification. Addison Wesley, Reading (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lanet, JL., Requet, A. (2000). Formal Proof of Smart Card Applets Correctness. In: Quisquater, JJ., Schneier, B. (eds) Smart Card Research and Applications. CARDIS 1998. Lecture Notes in Computer Science, vol 1820. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721064_7
Download citation
DOI: https://doi.org/10.1007/10721064_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67923-3
Online ISBN: 978-3-540-44534-0
eBook Packages: Springer Book Archive