Advanced

Applet verification strategies for RAM-constrained devices

Maltesson, Nils LU ; Naccache, D; Trichina, E and Tymen, C (2002) Information Security and Cryptology - ICISC 2002. 5th International Conference. In Information Security and Cryptology - ICISC 2002: 5th International Conference, Seoul, Korea, November 28-29, 2002. Revised Papers 2587. p.118-137
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 memory consumption.... (More)
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 memory consumption. Our algorithm is inspired by bit-slice data processing and consists in running the verifier on each variable in turn. In other words, instead of running the fix-point calculation algorithm once on M variables, we re-launch the algorithm M/l times, verifying each time only l variables. Parameter l can then be tuned to suit the RAM resources available on board whereas M/l upper-bounds the computational effort (expressed in re-runs of the usual fix-point calculation algorithm). The resulting RAM economy, as experimented on a number of popular applets, is around 40%. (Less)
Please use this url to cite or link to this publication:
author
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
in
Information Security and Cryptology - ICISC 2002: 5th International Conference, Seoul, Korea, November 28-29, 2002. Revised Papers
volume
2587
pages
118 - 137
publisher
Springer
conference name
Information Security and Cryptology - ICISC 2002. 5th International Conference.
external identifiers
  • wos:000182856200009
ISSN
0302-9743
1611-3349
language
English
LU publication?
yes
id
356361d0-c433-43f9-92f7-50258ca94ee3 (old id 310882)
alternative location
http://www.springerlink.com/content/ydddy993whevgykd/
date added to LUP
2007-11-30 14:10:00
date last changed
2016-04-15 20:27:17
@inproceedings{356361d0-c433-43f9-92f7-50258ca94ee3,
  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 memory consumption. Our algorithm is inspired by bit-slice data processing and consists in running the verifier on each variable in turn. In other words, instead of running the fix-point calculation algorithm once on M variables, we re-launch the algorithm M/l times, verifying each time only l variables. Parameter l can then be tuned to suit the RAM resources available on board whereas M/l upper-bounds the computational effort (expressed in re-runs of the usual fix-point calculation algorithm). The resulting RAM economy, as experimented on a number of popular applets, is around 40%.},
  author       = {Maltesson, Nils and Naccache, D and Trichina, E and Tymen, C},
  booktitle    = {Information Security and Cryptology - ICISC 2002: 5th International Conference, Seoul, Korea, November 28-29, 2002. Revised Papers},
  issn         = {0302-9743},
  language     = {eng},
  pages        = {118--137},
  publisher    = {Springer},
  title        = {Applet verification strategies for RAM-constrained devices},
  volume       = {2587},
  year         = {2002},
}