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.
|
 |
On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines
| Book Series | Lecture Notes in Computer Science |
| Publisher | Springer Berlin / Heidelberg |
| ISSN | 0302-9743 (Print) 1611-3349 (Online) |
| Volume | Volume 1503/1998 |
| Book | Static Analysis |
| DOI | 10.1007/3-540-49727-7 |
| Copyright | 1998 |
| ISBN | 978-3-540-65014-0 |
| DOI | 10.1007/3-540-49727-7_2 |
| Pages | 17-32 |
| Subject Collection | Computer Science |
| SpringerLink Date | Thursday, January 01, 1998 |
| |
|
On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines
Masami Hagiya5 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.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|