A semantic model of confinement and Locality theorem

作者：Wang Shuling^*; Shu Qin; Liu Yijing; Qiu Zongyan

来源：Frontiers of Computer Science in China, 2010, 4(1): 28-46.

DOI：10.1007/s11704-009-0075-6

• operational semantics
• confinement
• well confined program
• Locality theorem
• confined type
• ownership

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

• 出版日期2010-3
• 单位北京大学