Encapsulating objects with confined types

ABSTRACT

Object-oriented languages provide little support for encapsulating objects. Reference semantics allows objects to escape their defining scope, and the pervasive aliasing that ensues remains a major source of software defects. This paper presents Kacheck/J, a tool for inferring object encapsulation properties of large Java programs. Our goal is to develop practical tools to assist software engineers, thus we focus on simple and scalable techniques. Kacheck/J is able to infer confinement—the property that all instances of a given type are encapsulated in their defining package. This simple property can be used to identify accidental leaks of sensitive objects, as well as for compiler optimizations. We report on the analysis of a large body of code and discuss language support and refactoring for confinement.

REFERENCES

• 1: Jonathan Aldrich , Valentin Kostadinov , Craig Chambers, Alias annotations for program understanding, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 2: Almeida, P. S. 1997. Balloon types: Controlling sharing of state in data types. In ECOOP'97---Object-Oriented Programming, 11th European Conference (Jyväskylä, Finland, June 9--13). Lecture Notes in Computer Science, vol. 1241. Springer-Verlag, New York, 32--59.
• 3: Almeida, P. S. 1999. Type-checking balloon types. Elect. Notes Theoret. Comput. Sci. 20.
• 4: Anindya Banerjee , David A. Naumann, Representation independence, confinement and access control [extended abstract], Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.166-177, January 16-18, 2002, Portland, Oregon
• 5: Barnett, M., DeLine, R., Fähndrich, M., Rustan, K., Leino, M., and Schulte, W. 2004. Verification of object-oriented programs with invariants. J. Obj. Tech. 3, 27--56. (Preliminary version in Proceedings of 5th Workshop on Formal Techniques for Java-like Programs, 2003).
• 6: Bruno Blanchet, Escape analysis for object-oriented languages: application to Java, ACM SIGPLAN Notices, v.34 n.10, p.20-34, Oct. 1999
• 7: Bruno Blanchet, Escape analysis for Java^TM: Theory and practice, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.6, p.713-775, November 2003 [doi>10.1145/945885.945886]
• 8: Jeff Bogda , Urs Hölzle, Removing unnecessary synchronization in Java, ACM SIGPLAN Notices, v.34 n.10, p.35-46, Oct. 1999
• 9: Boris Bokowski, CoffeeStrainer: statically-checked constraints on the definition and use of types in Java, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.355-374, September 06-10, 1999, Toulouse, France
• 10: Jan Vitek , Boris Bokowski, Confined types, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.82-96, November 01-05, 1999, Denver, Colorado, United States
• 11: Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 12: Chandrasekhar Boyapati , Alexandru Salcianu , William Beebee, Jr. , Martin Rinard, Ownership types for safe region-based memory management in real-time Java, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 13: John Boyland, Alias burying: unique variables without destructive reads, Software—Practice & Experience, v.31 n.6, p.533-553, May 2001 [doi>10.1002/spe.370]
• 14: John Boyland , James Noble , William Retert, Capabilities for Sharing: A Generalisation of Uniqueness and Read-Only, Proceedings of the 15th European Conference on Object-Oriented Programming, p.2-27, June 18-22, 2001
• 15: David Gerard Clarke, Object ownership and containment, University of New South Wales, New South Wales, Australia, 2003
• 16: Dave Clarke , Michael Richmond , James Noble, Saving the world from bad beans: deployment-time confinement checking, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 17: Clarke, D. and Wrigstad, T. 2003. External uniqueness. In Proceedings of the 10th Workshop on Foundations of Object-Oriented Languages (FOOL), (New Orleans, LA, Jan.).
• 18: David G. Clarke , John M. Potter , James Noble, Ownership types for flexible alias protection, ACM SIGPLAN Notices, v.33 n.10, p.48-64, Oct. 1998
• 19: Ian Clarke , Scott G. Miller , Theodore W. Hong , Oskar Sandberg , Brandon Wiley, Protecting Free Expression Online with Freenet, IEEE Internet Computing, v.6 n.1, p.40-49, January 2002 [doi>10.1109/4236.978368]
• 20: Ian Clarke , Oskar Sandberg , Brandon Wiley , Theodore W. Hong, Freenet: a distributed anonymous information storage and retrieval system, International workshop on Designing privacy enhancing technologies: design issues in anonymity and unobservability, p.46-66, January 2001, Berkeley, California, United States
• 21: Detlefs, D., Leino, K., Leino, M., and Nelson, G. 1996. Wrestling with rep exposure. Tech. rep. Digital Equipment Corporation Systems Research Center.
• 22: Alain Deutsch, Semantic models and abstract interpretation techniques for inductive data structures and pointers, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.226-229, June 21-23, 1995, La Jolla, California, United States [doi>10.1145/215465.215594]
• 23: Dowling, W. F. and Gallier, J. H. 1984. Linear-time algorithms for testing the satisfiability of propositional horn formulae. J. Logic Prog. 1, 3 (Oct.), 267--284.
• 24: Refactoring: improving the design of existing code, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 25: Gamma, E., Helm, R., Johnson, R. E., and Vlissides, J. 1994. Design Patterns. Addison-Wesley, Reading, MA.
• 26: Daniela Genius , Martin Trapp , Wolf Zimmermann, An Approach to Improve Locality Using Sandwich Types, Proceedings of the Second International Workshop on Types in Compilation, p.194-214, March 25-27, 1998
• 27: Stephan Herrmann, Object Teams: Improving Modularity for Crosscutting Collaborations, Revised Papers from the International Conference NetObjectDays on Objects, Components, Architectures, Services, and Applications for a Networked World, p.248-264, October 07-10, 2002
• 28: John Hogg, Islands: aliasing protection in object-oriented languages, Conference proceedings on Object-oriented programming systems, languages, and applications, p.271-285, October 06-11, 1991, Phoenix, Arizona, United States
• 29: John Hogg , Doug Lea , Alan Wills , Dennis deChampeaux , Richard Holt, The Geneva convention on the treatment of object aliasing, ACM SIGPLAN OOPS Messenger, v.3 n.2, p.11-16, April 1992 [doi>10.1145/130943.130947]
• 30: Atsushi Igarashi , Benjamin C. Pierce , Philip Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.396-450, May 2001 [doi>10.1145/503502.503505]
• 31: Kent, S. and Maung, I. 1995. Encapsulation and aggregation. In Proceedings of TOOLS PACIFIC 95 (TOOLS 18), Prentice-Hall, Englewood Cliffs, NJ, 227--238.
• 32: Müller, P. 2002. Modular specification and verification of object-oriented programs. Ph.D. dissertation. FernUniversität Hagen (Also in Lecture Notes in Computer Science, vol. 2262. Springer-Verlag, New York, 2002).
• 33: Müller, P. and Poetzsch-Heffter, A. 1999. Universes: A type system for controlling representation exposure. In Programming Languages and Fundamentals of Programming, A. Poetzsch-Heffter and J. Meyer, Eds. Fernuniversität Hagen.
• 34: James Noble , Jan Vitek , John Potter, Flexible Alias Protection, Proceedings of the 12th European Conference on Object-Oriented Programming, p.158-185, July 20-24, 1998
• 35: Potanin, A., Noble, J., Clarke, D. and Biddle, R. 2004. Featherweight generic confinement. In Proceedings of the Workshop on Foundations of Object-Oriented Languages.
• 36: Rustan, K., Leino, M., and Müller, P. 2004. Object invariants in dynamic contexts. In Proceedings of ECOOP'04, 16th European Conference on Object-Oriented Programming, 491--516.
• 37: Skalka, C. and Smith, S. F. 2005. Static use-based object confinement. Int. J. Inf. Secur. 4, 1--2, 87--104 (Preliminary version in Proceedings of Foundations of Computer Security, volume 02-12 of DIKU technical reports 2002. 117--126).
• 38: Sun Microsystems. 2000. Support for extensions and applications in the version 1.2 of the Java platform. http://java.sun.com/products/jdk/1.2/docs/guide/extensions/spec.html.
• 39: Jan Vitek , Boris Bokowski, Confined types in Java, Software—Practice & Experience, v.31 n.6, p.507-532, May 2001 [doi>10.1002/spe.369]
• 40: Ayal Zaks , Vitaly Feldman , Nava Aizikowitz, Sealed calls in Java packages, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.83-92, October 2000, Minneapolis, Minnesota, United States
• 41: Tian Zhao , James Noble , Jan Vitek, Scoped Types for Real-Time Java, Proceedings of the 25th IEEE International Real-Time Systems Symposium, p.241-251, December 05-08, 2004 [doi>10.1109/REAL.2004.51]
• 42: Tian Zhao , Jens Palsberg , Jan Vitek, Lightweight confinement for featherweight java, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

General Terms:
Languages