Roberto Barbuti
ABSTRACT
A Java program is usually translated into an intermediate language, known as Java Virtual Machine Language (JVML), which is then executed by a Java Virtual Machine (JVM). Before its execution a JVML program is verified to prevent a wide range of run-time errors. Nowadays, Java applets are available for various kinds of portable devices, including modern Java smart cards. However, Java cards cannot execute the classical verification algorithms, due to their very small amount of working memory.We present a new algorithm to verify a subset of the Java bytecode language, suitable to be executed in low-memory environments, such as Java smart cards. The method is based on abstract interpretation of the language operational semantics. We define an abstract small-step semantics of the language, able to keep information regarding the modifications of data during Java constructs execution. We state the equivalence between our verification algorithm and the "standard" one. Moreover, we discuss the low memory requirements of the algorithm.
- R. Barbuti, C. Bernardeschi, and N. D. Francesco. Abstract interpretation of operational semantics for secure information flow. Information Processing Letters, 83(2):101--108, 2002.]] Google Scholar
Digital Library
- R. Barbuti, C. Bernardeschi, and N. D. Francesco. Checking security of java bytecode by abstract interpretation. In ACM Symposium on Applied Computing (SAC), 2002.]] Google ScholarDigital Library
- R. Barbuti, C. Bernardeschi, N. D. Francesco, and L. Tesei. Fixing the java bytecode verifier by a suitable type domain. In International Conference on Software Engineering and Knowledge Engineering (SEKE), 2002.]] Google ScholarDigital Library
- R. Barbuti and S. Cataudella. Verifica di java bytecode su java card, 2003. Internal note, Dip. to di Informatica - Università di Pisa - (In italian).]]Google Scholar
- M. Hagiya and A. Tozawa. On a new method for dataflow analysis of java virtual machine subroutines. IN SAS'98, Levi G, LNCS 1503, pages 17--32, Springer-Verlag 1998.]]Google ScholarCross Ref
- X. Leroy. Bytecode verification on java smart cards. Software Practice & Experience, 32:319--340, 2002.]] Google ScholarDigital Library
- T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996.]] Google ScholarDigital Library
- R. O'Callahan. A simple, comprehensive type system for java bytecode subroutines. In Proc. 26th ACM Symposium on Principles of Programming Languages, 1999.]] Google ScholarDigital Library
- Z. Qian. Standard fixpoint iteration for java bytecode verification. ACM Transactions on Programming Languages and Systems, 22(4):638--672, July 2000.]] Google ScholarDigital Library
- E. Rose and K. Rose. Lightweight bytecode verification. In Workshop "Formal Underpinnings of the Java Paradigm", OOPSLA'98, 1998.]]Google Scholar
- R. Stata and M. Abadi. A type system for java bytecode subroutines. ACM Transactions on Programming Languages and Systems, 21(1):90--137, January 1999.]] Google ScholarDigital Library
- Sun Microsystems Inc. Java Card 2.1 Language Subset and Virtual Machine Specification, 1998. http://java.sun.com:80/products/javacard/.]]Google Scholar
Index Terms
- Java bytecode verification on Java cards
Recommendations
Bytecode verification on Java smart cards
This article presents a novel approach to the problem of bytecode verification for Java Card applets. By relying on prior off-card bytecode transformations, we simplify the bytecode verifier and reduce its memory requirements to the point where it can ...
A Study on the Optimization of Class File for Java Card Platform
ICOIN '02: Revised Papers from the International Conference on Information Networking, Wireless Communications Technologies and Network Applications-Part IThe Java Card technology enables programs written in the Java programming language to run on smart cards and other resource-constrained devices. Smart cards represent one of the smallest platforms in use today. The memory configuration of a smart card ...
From CIL to Java bytecode: Semantics-based translation for static analysis leveraging
Highlights- A formal translation of CIL (.Net) bytecode into Java bytecode is introduced and proved sound w.r.t. the language semantics
AbstractA formal translation of CIL (i.e., .Net) bytecode into Java bytecode is introduced and proved sound with respect to the language semantics. The resulting code is then analyzed with Julia, an industrial static analyzer of Java bytecode. ...
Comments