Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines

Masami HagiyaContact Information and Akihiko Tozawa5

(5)  Department of Information Science, Graduate School of Science, University of Tokyo, Japan
Abstract
The bytecode verifier of the Java Virtual Machine, which statically checks the type safety of Java bytecode, is the basis of the security model of Java and guarantees the safety of mobile code sent from an untrusted remote host. However, the type system for Java bytecode has some technical problems, one of which is in the handling of sub-routines. Based on the work of Stata and Abadi and that of Qian, this paper presents yet another type system for Java Virtual Machine sub-routines. Our type system includes types of the form last(x). A value whose type is last(x) is the same as that of the x-th variable of the caller of the subroutine. In addition, we represent the type of a return address by the form return(n), which means returning to the n-th outer caller. By virtue of these types, we can analyze instructions purely in terms of type, and as a result the correctness proof of bytecode verification becomes extremely simple. Moreover, for some programs, our method is more powerful than existing ones. In particular, our method has no restrictions on the number of entries and exits of a subroutine.

Contact Information Masami Hagiya
Email: hagiya@is.s.u-tokyo.ac.jp
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Referenced by
3 newer articles

  1. Klein, Gerwin (2001) Verified lightweight bytecode verification. Concurrency and Computation Practice and Experience 13(13)
    [CrossRef]
  2. Leroy, Xavier (2002) Bytecode verification on Java smart cards. Software Practice and Experience 32(4)
    [CrossRef]
  3. Coglio, Alessandro (2003) Improving the official specification of Java bytecode verification. Concurrency and Computation Practice and Experience 15(2)
    [CrossRef]
Remote Address: 38.107.191.109 • Server: mpweb02
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)