|
|
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; |
|
|
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
|
|
|
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
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|