Abstract
While bringing considerable flexibility and extending the horizons of mobile computing, mobile code raises major security issues. Hence, mobile code, such as Java applets, needs to be analyzed before execution. The byte-code verifier checks low-level security properties that ensure that the downloaded code cannot bypass the virtual machine’s security mechanisms. One of the statically ensured properties is type safety. The type-inference phase is the overwhelming resource-consuming part of the verification process.
This paper addresses the RAM bottleneck met while verifying mobile code in memory-constrained environments such as smart-cards. We propose to modify classic type-inference in a way that significantly reduces the memory consumption in the memory-constrained device at the detriment of its distrusted memory-rich environment.
The outline of our idea is the following, throughout execution, the memory frames used by the verifier are MAC-ed and exported to the terminal and then retrieved upon request. Hence a distrusted memory-rich terminal can be safely used for convincing the embedded device that the downloaded code is secure.
The proposed protocol was implemented on JCOP20 and JCOP30 Java cards using IBM’s JCOP development tool.
This is a preview of subscription content, log in via an institution to check access.
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
Chen, Z.: Java Card Technology for Smart Cards: Architecture and Programmer’s Guide. The Java Series. Addison-Wesley, Reading (2000)
Cohen, R.: The defensive Java virtual machine specification, Technical Report, Computational Logic Inc. (1997)
Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis by Construction or Approximation of Fixpoints. In: Proceedings of POPL 1977, pp. 238–252. ACM Press, Los Angeles (1977)
Leroy, X.: Java Byte-Code Verification: an Overview. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 265–285. Springer, Heidelberg (2001)
Leroy, X.: On-Card Byte-code Verification for Java card. In: Attali, S., Jensen, T. (eds.) E-smart 2001. LNCS, vol. 2140, pp. 150–164. Springer, Heidelberg (2001)
Leroy, X.: Byte-code Verification for Java smart card. Software Practice & Experience 32, 319–340 (2002)
Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. The Java Series. Addison-Wesley, Reading (1999)
Maltesson, N., Naccache, D., Trichina, E., Tymen, C.: Applet Verification Strategies for RAM-constrained Devices. In: Lee, P.J., Lim, C.H. (eds.) ICISC 2002. LNCS, vol. 2587, pp. 118–137. Springer, Heidelberg (2003)
McGraw, G., Felten, E.: Java Security. John Wiley & Sons, Chichester (1999)
Naccache, D., Tchoulkine, A., Tymen, C., Trichina, E.: Reducing the Memory Complexity of Type–Inference Algorithms. In: Deng, R.H., Qing, S., Bao, F., Zhou, J. (eds.) ICICS 2002. LNCS, vol. 2513, pp. 109–121. Springer, Heidelberg (2002)
Necula, G.: Proof-carrying code. In: Proceedings of POPL 1997, pp. 106–119. ACM Press, New York (1997)
Schneier, B.: Applied Cryptography: Second Edition: protocols, algorithms and source code in C. John Wiley & Sons, Chichester (1996)
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
Hyppönen, K., Naccache, D., Trichina, E., Tchoulkine, A. (2003). Trading-Off Type-Inference Memory Complexity against Communication. In: Qing, S., Gollmann, D., Zhou, J. (eds) Information and Communications Security. ICICS 2003. Lecture Notes in Computer Science, vol 2836. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39927-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-39927-8_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20150-2
Online ISBN: 978-3-540-39927-8
eBook Packages: Springer Book Archive