A semantic model of confinement and Locality
Theorem

doi:10.1007/s11704-009-0075-6

Front. Comput. Sci.

2010, Vol. 4

Issue (1) : 28-46 https://doi.org/10.1007/s11704-009-0075-6

Research articles

A semantic model of confinement and Locality Theorem

Shuling WANG¹,Qin SHU²,Yijing LIU²,Zongyan QIU²,

1.LMAM and Department of Informatics, School of Mathematical Sciences, Peking University, Beijing 100872, China；IIST, United Nations University, Macao, China; 2.LMAM and Department of Informatics, School of Mathematical Sciences, Peking University, Beijing 100872, China;

Download: PDF(421 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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

Keywords operational semantics confinement well confined program Locality Theorem confined type ownership

Issue Date: 05 March 2010

Cite this article:

Shuling WANG,Yijing LIU,Qin SHU, et al. A semantic model of confinement and Locality Theorem[J]. Front. Comput. Sci., 2010, 4(1): 28-46.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-009-0075-6
https://academic.hep.com.cn/fcs/EN/Y2010/V4/I1/28

	Hogg J. Islands:aliasing protection in object-oriented languages. In: Proceedings of OOPSLA’91. ACM Press, 1991
	Almeida P S. Balloon types: controlling sharing of state in data types. In: Proceedings of ECOOP’97. Springer, 1997
	Clarke D, Potter J, Noble J. Ownership types for flexible alias protection. In: Proceedings of OOPSLA’98. ACM Press, 1998
	Vitek J, Bokowski B. Confined types in Java. Software Practice and Experience, 2000, 31: 507―532
	Müller P. ModularSpecification and Verification of Objectoriented Programs. PhD thesis, Fern University at Hagen. Springer, 2002, LNCS, 2262
	Grothoff C, Palsberg J, Vitek J. Encapsulating objects with confined types.In: Proceedings of OOPSLA’01. ACM Press, 2001
	Boyland J. Alias burying: unique variables without reads. Software Practice and Experience, 2001, 31(6): 533―553
	Clarke D, Wrigstrad T. External uniqueness. In: Foundations of Object-Oriented Languages (FOOL). 2003
	Banerjee A, Naumann D A. Representation independence,confinement and access control (extended abstract). In: Proceedings of POPL’02. ACMPress, 2002
	Banerjee A, Naumann D A. Ownership confinement ensuresrepresentation independence for object-oriented programs. JACM, 2005, 52(6): 894―960
	Noble J, Biddle R, Tempero E, Potanin A, Clarke D. Towards a model of encapsulation. In: Proceedings of IWACO’03, Darmstadt,Germany, 2003
	Wang S L, Qiu Z Y. A generic model for confinementand its application. In: Proceedings of2nd IEEE Symposium on Theoretical Aspects of Software Engineering. 2008, 57―64
	.	Reynolds J C. Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS’02. IEEE CS, 2002
	Parkinson M. Localreasoning for Java. PhD thesis, ChurchillCollege, 2005
	Zhao T, Palsberg J, Vitek J. Lightweight confinement for featherweight Java. In: Proceedings of OOPSLA’03. ACM Press, 2003
	Clarke D, Noble J, Potter J. Simple ownership types for object containment. In: Proceedings of ECOOP’01. Springer, 2001
	Cameron N R, Noble J, Smith M J. Multiple ownership. In: Proceedingsof OOPSLAŠ 07, ACM SIGPLAN Notices. 2007, volume 42
	Aldrich J, Chambers C. Ownership domains: separatingalias policy from mechanism. In: Proceedingsof ECOOP’04. Springer, 2004
	Boyland J, Noble J, Retert W. Capabilities for sharing: a generalisation of uniquenessand read-only. In: Proceedings of ECOOP’01. Springer, 2001
	Clarke D, Wrigstrad T. External uniqueness is uniqueenough. In: Proceedings of ECOOP’03. Springer, 2003
	Noble J, Vitek J, Potter J. Flexible alias protection. In: Proceedings of ECOOP’98. Springer, 1998
	Banerjee A, Naumann D A. Ownership: transfer, sharing,and encapsulation. In: ECOOP Workshop onFormal Techniques for Java-like Programs (FTfJP). 2003

[1]	Yanhong HUANG,Jifeng HE,Huibiao ZHU,Yongxin ZHAO,Jianqi SHI,Shengchao QIN. Semantic theories of programs with nested interrupts[J]. Front. Comput. Sci., 2015, 9(3): 331-345.
[2]	Qin LI,Yongxin ZHAO,Huibiao ZHU,Jifeng HE. A UTP semantic model for Orc language with execution status and fault handling[J]. Front. Comput. Sci., 2014, 8(5): 709-725.
[3]	Qin SHU, Zongyan QIU, Shuling WANG. Confinement framework for encapsulating objects[J]. Front Comput Sci, 2013, 7(2): 236-256.

Viewed

Full text

Abstract

Cited

Shared

Discussed