A semantic model of confinement and Locality theorem

Confinement is required in object-oriented programming in order to protect sensitive object references. Recently a range of confinement schemes have been proposed to achieve object encapsulation by defining static type systems, but unavoidably, with strong restrictions. On the other hand, no similar...

Full description

Saved in:
Bibliographic Details
Published in:Frontiers of Computer Science 2010-03, Vol.4 (1), p.28-46
Main Authors: Wang, Shuling, Shu, Qin, Liu, Yijing, Qiu, Zongyan
Format: Article
Language:English
Subjects:
Computer Science
Confinement
Object oriented programming
Research Article
Semantics
Theorems
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Confinement is required in object-oriented programming in order to protect sensitive object references. Recently a range of confinement schemes have been proposed to achieve object encapsulation by defining static type systems, but unavoidably, with strong restrictions. On the other hand, no similarity in concepts makes assessing of these schemes a difficulty. We build in this paper a semantic model for confinement in μ Java, a subset of sequential Java that offers most object-oriented features. This model has limited restriction for programs. From a semantic view, confinement is defined with respect to a given context that specifies partition of the object pool and confinement constraint among them. Moreover, we present the main Locality theorem for checking well confinement of programs locally. By applying this theorem, we have solved a security breach problem from Java JDK 1.1.1, and furthermore, proved the soundness of two widely used confinement schemes: confined types and ownership types.
ISSN:1673-7350
2095-2228
1673-7466
2095-2236
DOI:10.1007/s11704-009-0075-6