A static type system for JVM access control

Tomoyuki Higuchi; Atsushi Ohori

doi:10.1145/944746.944726

A static type system for JVM access control

Tomoyuki Higuchi, Atsushi Ohori

Research output: Contribution to journal › Conference article › peer-review

Abstract

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 develop 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.

Original language	English
Pages (from-to)	227-237
Number of pages	11
Journal	ACM SIGPLAN Notices
Volume	38
Issue number	9
DOIs	https://doi.org/10.1145/944746.944726
Publication status	Published - 2003 Sept
Externally published	Yes
Event	Proceedings of the 2003 ACM SIGPLAN International Conference on Functional Programming - Uppsala, Sweden Duration: 2003 Aug 25 → 2003 Aug 29

Keywords

Access control
JVM
Stack inspection
Type inference
Type system

ASJC Scopus subject areas

Software
Computer Graphics and Computer-Aided Design

Access to Document

10.1145/944746.944726

Cite this

@article{856538f4fd1048c9a7bb34e23accf85c,

title = "A static type system for JVM access control",

abstract = "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 develop 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.",

keywords = "Access control, JVM, Stack inspection, Type inference, Type system",

author = "Tomoyuki Higuchi and Atsushi Ohori",

year = "2003",

month = sep,

doi = "10.1145/944746.944726",

language = "English",

volume = "38",

pages = "227--237",

journal = "ACM SIGPLAN Notices",

issn = "0362-1340",

number = "9",

note = "Proceedings of the 2003 ACM SIGPLAN International Conference on Functional Programming ; Conference date: 25-08-2003 Through 29-08-2003",

}

TY - JOUR

T1 - A static type system for JVM access control

AU - Higuchi, Tomoyuki

AU - Ohori, Atsushi

PY - 2003/9

Y1 - 2003/9

N2 - 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 develop 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.

AB - 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 develop 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.

KW - Access control

KW - JVM

KW - Stack inspection

KW - Type inference

KW - Type system

UR - http://www.scopus.com/inward/record.url?scp=1442264133&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=1442264133&partnerID=8YFLogxK

U2 - 10.1145/944746.944726

DO - 10.1145/944746.944726

M3 - Conference article

AN - SCOPUS:1442264133

SN - 0362-1340

VL - 38

SP - 227

EP - 237

JO - ACM SIGPLAN Notices

JF - ACM SIGPLAN Notices

IS - 9

T2 - Proceedings of the 2003 ACM SIGPLAN International Conference on Functional Programming

Y2 - 25 August 2003 through 29 August 2003

ER -

A static type system for JVM access control

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this