|
|
|
 |
Eva Rose
Post Doctoral Researcher
IBM T. J. Watson Research Center
Friday, March 12, 2004, 11:00am - 12:00pm
LC 102, Brooklyn Campus, Polytechnic University
During this seminar, we will present a recent improvement, the lightweight bytecode verifier, to the existing bytecode verification technology, a critical component of the Java security model, for mobile code used with the Java "micro edition" (J2ME).
On Java platforms, remotely loaded Java class files of virtual machine bytecode are required to be safety verified before execution, that is, to undergo a static type analysis that protects the platform's Java run-time system from so-called type confusion attacks such as pointer or object manipulations. The data flow analysis which carries out the bytecode verification, however, is beyond the capacity of most embedded devices because of the extensive memory requirements that the typical (standard) verification algorithm will need.
To meet this problem, we propose to take a proof-carrying code approach to bytecode verification in defining an alternative technique called "Lightweight bytecode verification". The idea is to define a notion of a "certificate" for previously verified code, so that the code can be >> reverified<< on even poorly resourced platforms in a "tamper proof" manner. (By "tamper proof" in this context we mean that the type safety guarantees of the original code cannot be broken by crafting a "false" certificate or by altering the analyzed code.)
We will begin our talk by explaining these ideas from Java examples, run on a prototype lightweight verifier. Then we formulate the technique in the case where static program safety is seen as a general data flow problem, and briefly argue that the two approaches provides the same static safety guarantees. We give a brief overview of how the Java bytecode verifier fits into the general framework for an important subset of the Java Virtual Machine. Finally, we discuss how the technique generalizes and simulates the J2ME verifier (to be expected as Sun's J2ME "K-Virtual Machine" verifier was directly based on an early version of this work), as well as Leroy's on card bytecode verifier, which is specifically targeted for Java Cards.
Further details are available from URL http://www.evarose.net.
For further information contact Bob Flynn [flynn@west.poly.edu]