Abstract
Java is a popular development platform for mobile code systems, because it ensures application portability and mobility. The Java Virtual Machine verifies statically(during the loading phase) the program is well-behaved with intermediate(as called bytecode). This is done by a software security module called the bytecode verifier. Smart card that provide a Java Virtual Machine, called Java Card, are not supplied with such a verifier because of its complexity. In this paper, we propose a bytecode verifier with efficient algorithm to adapt to the hardware constraints of smart card.
This work is supported by Kyungnam University Research Fund, 2003.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Z. Chen. Java Card Technology for Smart Cards. Addison Wesley, 2000.
Ludovic Casset. Formal Development of an Embedded Verifier for Java Card Byte Code.
X. Leroy. Java bytecode verification: an overview. In Computer Aided Verification, 2001.
Damien Deville. Building an “impossible” verifier on a Java Card.
Sun Microsystem. Java Card 2.1.1 Virtual Machine Specification, 2000.
B. Venners, Inside Java Virtual Machine, McGraw-Hill, 1997.
X. Leroy. On-card bytecode verification for java card. In Esmart, 2001.
X. Leroy. Bytecode verification for Java smart card. Software Practice & Experience, 2002.
G. C. Necula and P. Lee. Proof carrying code. In Proceedings of the 24th ACM SIGPLAN-SICACT Symposium on Principles of Programming Languages (POPL’ 97), 1997.
E. Rose and K.H. Rose. Lightweight bytecode verification. In Workshop of the Formal Underpinnings of the Java Paradigm, OOPSLA’98 1998.
Sun Microsystem. Connected Limited Device Configuration and K Virtual Machine. http://java.sun.com/products/cldc/.
Trusted Logic. Formal methods, smart card, security. http://www.trustedlogic.com/.
Sun Microsystems, http://java.sun.com/, Java Home Page.
Java Card Forums, http://www.javacardforum.org Java Card Forum Home Page.
Sun Microsystems. JavaCard 2.2 Development Kit User’s guide specification, 2002.
Sun Microsystems. JavaCard 2.2 Application Programming notes, 2002.
Sun Microsystems. JavaCard 2.2 Off-Card Verifier, White paper, 2002.
Sun Microsystems. Java Virtual Machine Specs, 2002.
C. Colby, G. C. Necula, and P. Lee. A Proof Carrying Code Architecture for Java. In Computer Aided Verification, 2000.
Gong L. Inside Java 2 platform security: architecture, API design, and implementation. The Java Series. Addison-Wesley, 1999.
Sun Microsystems. Java 2 platform micro edition technology for creating mobile devices. White paper, http://java.sun.com/products/cldc/wp/KVMwp.pdf, 2000.
Jeung-Bo Cho. Design and implementation of On-Card Verifier for Java card based on smart card, 2002.
Wook-Chul Hwang. A study on the optimization of the Java Card Virtual Machine based on smart card, 2001.
Alessando Coglio, Toward a Provably-Correct Implementation of the JVM Bytecode Verifier, 2001.
L.T. Walczowski and F. Deravi, Training in the use of Java Smart Cards for embedded applications, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cho, JB., Jung, MS. (2003). A Very Small Bytecode-Verifier Based on PCC Algorithm for Smart Card. In: Chung, CW., Kim, CK., Kim, W., Ling, TW., Song, KH. (eds) Web and Communication Technologies and Internet-Related Social Issues — HSI 2003. HSI 2003. Lecture Notes in Computer Science, vol 2713. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45036-X_11
Download citation
DOI: https://doi.org/10.1007/3-540-45036-X_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40456-9
Online ISBN: 978-3-540-45036-8
eBook Packages: Springer Book Archive