Java Bytecode Verification: Algorithms and Formalizations |
| |
Authors: | Xavier Leroy |
| |
Affiliation: | (1) INRIA Rocquencourt and Trusted Logic S.A, France |
| |
Abstract: | Bytecode verification is a crucial security component for Java applets, on the Web and on embedded devices such as smart cards.
This paper reviews the various bytecode verification algorithms that have been proposed, recasts them in a common framework
of dataflow analysis, and surveys the use of proof assistants to specify bytecode verification and prove its correctness.
This revised version was published online in August 2006 with corrections to the Cover Date. |
| |
Keywords: | bytecode verification Java Virtual Machine dataflow analysis abstract interpretation subroutines |
本文献已被 SpringerLink 等数据库收录! |