A static type system for JVM access control

9 years 7 months ago
A static type system for JVM access control
This paper presents a static type system for JAVA Virtual Machine (JVM) code that enforces an access control mechanism similar to the one found, for example, in a JAVA implementation. In addition to verifying type consistency of a given JVM code, the type system statically verifies that the code accesses only those resources that are granted by the prescribed access policy. The type system is proved to be sound with respect to an operational semantics that enforces access control dynamically, similarly to JAVA stack inspection. This result ensures that "well typed code cannot violate access policy." The paper then develops a type inference algorithm and shows that it is sound with respect to the type system and that it always infers a minimal set of access privileges. These results allows us to develop a static system for JVM access control without resorting to costly runtime stack inspection. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitio...
Tomoyuki Higuchi, Atsushi Ohori
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2003
Where ICFP
Authors Tomoyuki Higuchi, Atsushi Ohori
Comments (0)