Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

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 WANG1,Qin SHU2,Yijing LIU2,Zongyan QIU2,
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