Confinement framework for encapsulating objects

Abstract

Confinement is used to prohibit safety-critical objects from unintended access. Approaches for specifying and verifying confinement have been proposed in the last twenty years but their application has been help back. We develop a novel framework for specifying and verifying object confinement in object-oriented (OO) programs. Instead of expressing the confinement requirements within a class for possible future usage, as with ownership types, we specify confinement requirements of the class in its usage class which actually intends to confine the parts, i.e., internal representations. Syntactically, an optional conf clause is introduced in class declarations for annotating the confined attribute-paths. A “same type and confinement” notation is introduced for expressing type and confinement dependence among variables, parameters, and return values of methods. Based on the extension to a Java-like language and existing techniques of alias analysis, we define a sound type-system for checking the wellconfinedness of OO programswith respect to the confinement specifications.

Keywords

object-oriented / aliasing / confinement / ownership / type system / well-confined program

References

[1] Hogg J, Lea D, Wills A, Dechampeaux D, Holt R. The geneva convention on the treatment of object aliasing. ACM SIGPLAN OOPS Messenger, 1992, 3(2): 11-16

[2] Clarke D, Drossopoulou S, Noble J, Wrigstad T. Aliasing, confinement, and ownership in object-oriented programming. Lecture Notes in Computer Science, 2008, 4906: 40

[3] Grothoff C, Palsberg J, Vitek J. Encapsulating objects with confined types. In: Proceedings of ACMSIGPLAN Notices, 2001, 36(11): 241-255

[4] Hogg J. Islands: aliasing protection in object-oriented languages. In: Proceedings of ACM SIGPLAN Notices. 1991, 271-285

[5] Almeida P. Balloon types: controlling sharing of state in data types. In: Proceedings of ECOOP’97-Object-Oriented Programming. 1997, 32-59

[6] Vitek J, Bokowski B. Confined types. In: Proceedings of ACM SIGPLAN Notices. 1999, 82-96

[7] Vitek J, Bokowski B. Confined types in Java. Software: Practice and Experience, 2001, 31(6): 507-532

[8] Zhao T, Palsberg J, Vitek J. Lightweight confinement for featherweight Java. In: Proceedings of ACM SIGPLAN Notices. 2003, 135-148

[9] Clarke D, Potter J, Noble J. Ownership types for flexible alias protection. In: Proceedings of ACMSIGPLAN Notices, 1998, 33(10): 48-64

[10] Clarke D. Ownership types and containment. Dissertation for Doctoral Degree. Australia: University of New South Wales, 2001

[11] Müller P, Poetzsch-Heffter A. Universes: a type system for controlling representation exposure. Technical Report 263, FernUniversitat Hagen. 1999

[12] Müller P. Modular specification and verification of object-oriented programs. Lecture Notes in Computer Science 2262, Springer, 2002

[13] Aldrich J, Chambers C. Ownership domains: separating aliasing policy from mechanism. In: Proceedings of ECOOP 2004 Object-Oriented Programming. 2004, 1-25

[14] Meyer B. Eiffel: the language. Object-Oriented Series. New York: Prentice Hall, 1992

[15] Wang S, Shu Q, Liu Y, Qiu Z. A semantic model of confinement and locality theorem. Frontiers of Computer Science in China, 2010, 4(1): 28-46

[16] Boyapati C, Liskov B, Shrira L. Ownership types for object encapsulation. In: Proceedings of ACM SIGPLAN Notices, 2003, 38(1): 213-223

[17] Qiu Z, Wang S, Long Q. Sequential Java: formal foundations. Technical Report, School of Mathematics, Peking University, 2007

[18] Meyer B. Towards a theory and calculus of aliasing. Journal of Object Technology, 2010, 9(2): 37-74

[19] Naeem N, Lhotàk O. Faster alias set analysis using summaries. Compiler Construction, 2011, 82-103

[20] Clarke D, Noble J, Potter J. Simple ownership types for object containment. In: Proceedings of ECOOP 2001 Object-Oriented Programming. 2001, 53-76

[21] Smith M, Drossopoulou S. Cheaper reasoning with ownership types. In: Proceedings of the 1st International Workshop on Aliasing, Confinement and Ownership in Object-oriented Programming (IWACO). 2003

[22] Clarke D, Drossopoulou S. Ownership, encapsulation and the disjointness of type and effect. In: Proceedings of ACM SIGPLAN Notices, 2002, 37(11): 292-310

[23] Aldrich J, Kostadinov V, Chambers C. Alias annotations for program understanding. In: Proceedings of ACM SIGPLAN Notices, 2002, 311-330

[24] Chin W, Khoo S, Qin S, Popeea C, Nguyen H. Verifying safety policies with size properties and alias controls. In: Proceedings of the 27th International Conference on Software Engineering. 2005, 186-195

[25] Dietl W, Drossopoulou S, Müller P. Generic universe types. In: Proceedings of ECOOP 2007 Object-Oriented Programming. 2007, 28-53

[26] Dietl W, Müller P. Universes: lightweight ownership for JML. Journal of Object Technology, 2005, 4-5-32

[27] Dietl W, Ernst M, Müller P. Tunable static inference for generic universe types. In: Proceedings of ECOOP 2011 Object-Oriented Programming. 2011, 333-357

[28] Cameron N, Drossopoulou S, Noble J, Smith M. Multiple ownership. In: Proceedings of ACM SIGPLAN Notices. 2007, 441-460

[29] Potanin A, Noble J, Clarke D, Biddle R. Generic ownership for generic Java. In: Proceedings of SIGPLAN Notices, 2006, 41(10): 311-324

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg