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