Representation independence, confinement and access control [extended abstract]

ABSTRACT

Denotational semantics is given for a Java-like language with pointers, subclassing and dynamic dispatch, class oriented visibility control, recursive types and methods, and privilege-based access control. Representation independence (relational parametricity) is proved, using a semantic notion of confinement similar to ones for which static disciplines have been recently proposed.

REFERENCES

• 1: Martín Abadi , Anindya Banerjee , Nevin Heintze , Jon G. Riecke, A core calculus of dependency, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.147-160, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292555]
• 2: A. Banerjee and D. A. Naumann. A static analysis for instance-based confinement in Java. In preparation.
• 3: A. Banerjee and D. A. Naumann. A simple semantics and static analysis for Java security. Technical Report CS Report 2001-1, Stevens Institute of Technology.
• 4: 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]
• 5: 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
• 6: A. Cavalcanti and D. A. Naumann. Forward simulation for data refinement of classes. Submitted, 2001.
• 7: David G. Clarke , James Noble , John Potter, Simple Ownership Types for Object Containment, Proceedings of the 15th European Conference on Object-Oriented Programming, p.53-76, June 18-22, 2001
• 8: W.-P. de Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, 1998.
• 9: D. Detlefs and K. R. M. Leino and G. Nelson. Wrestling with rep exposure. Research Report 156, COMPAQ Systems Research Center, July 1998.
• 10: Krishna Kishore Dhara , Gary T. Leavens, Forcing behavioral subtyping through specification inheritance, Proceedings of the 18th international conference on Software engineering, p.258-267, March 25-29, 1996, Berlin, Germany
• 11: Li Gong, Inside Java 2 platform security architecture, API design, and implementation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 12: Andrew D. Gordon , Andrew M. Pitts, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 13: Dan Grossman , Greg Morrisett , Steve Zdancewic, Syntactic type abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.6, p.1037-1080, Nov. 2000 [doi>10.1145/371880.371887]
• 14: Marieke Huisman , Bart Jacobs, Java Program Verification via a Hoare Logic with Abrupt Termination, Proceedings of the Third Internationsl Conference on Fundamental Approaches to Software Engineering: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.284-303, March 25-April 02, 2000
• 15: Atshushi Igarashi , Benjamin Pierce , Philip Wadler, Featherwieght Java: a minimal core calculus for Java and GJ, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.132-146, November 01-05, 1999, Denver, Colorado, United States
• 16: Samin S. Ishtiaq , Peter W. O'Hearn, BI as an assertion language for mutable data structures, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-26, January 2001, London, United Kingdom
• 17: Douglas Lea, Concurrent Programming in Java(TM): Design Principles and Patterns (3rd Edition) (Java (Addison-Wesley)), Addison-Wesley Professional, 2006
• 18: K. Rustan M. Leino , Greg Nelson, Data abstraction and information hiding, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.5, p.491-553, September 2002 [doi>10.1145/570886.570888]
• 19: Barbara H. Liskov , Jeannette M. Wing, A behavioral notion of subtyping, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.6, p.1811-1841, Nov. 1994 [doi>10.1145/197320.197383]
• 20: Nancy Lynch , Frits Vaandrager, Forward and backward simulations I.: untimed systems, Information and Computation, v.121 n.2, p.214-233, Sept. 1995 [doi>10.1006/inco.1995.1134]
• 21: A. R. Meyer , K. Sieber, Towards fully abstract semantics for local variables, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-203, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73577]
• 22: John C. Mitchell, Representation independence and data abstraction, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.263-276, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512669]
• 23: John C. Mitchell, On the equivalence of data representations, Artificial intelligence and mathematical theory of computation: papers in honor of John McCarthy, Academic Press Professional, Inc., San Diego, CA, 1991
• 24: John C. Mitchell, Foundations of programming languages, MIT Press, Cambridge, MA, 1996
• 25: P. M. uller. Modular Specification and Verification of Object-Oriented Programs. PhD thesis, FernUniversity at Hagen, 2001. Available from www.informatik.fernuni-hagen.de/pi5/publications.
• 26: Peter Müller , Arnd Poetzsch-Heffter, Modular specification and verification techniques for object-oriented software components, Foundations of component-based systems, Cambridge University Press, New York, NY, 2000
• 27: P. M. uller and A. Poetzsch-Heffter. A type system for controlling representation exposure in Java. ECOOP Workshop on Formal Techniques for Java Programs, Technical Report 269, Fernuniversit. at Hagen, 2000.
• 28: David A. Naumann, Soundness of data refinement for a higher-order imperative language, Theoretical Computer Science, v.278 n.1-2, p.271-301, May 6, 2002 [doi>10.1016/S0304-3975(00)00339-X]
• 29: P. W. O'Hearn , R. D. Tennent, Parametricity and local variables, Journal of the ACM (JACM), v.42 n.3, p.658-709, May 1995 [doi>10.1145/210346.210425]
• 30: Peter O'Hearn , Robert D. Tennent, ALGOL-like languages (v.2), Birkhauser Boston Inc., Cambridge, MA, 1996
• 31: G. Plotkin. Lambda definability and logical relations. Technical Report SAI-RM-4, University of Edinburgh, School of Artificial Intelligence, 1973.
• 32: U. S. Reddy. Objects and classes in Algol-like languages. In FOOL, 1998.
• 33: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 34: J. C. Reynolds. The essence of Algol. In J. W. de Bakker and J. C. van Vliet, editors, Algorithmic Languages. North-Holland, 1981.
• 35: J. C. Reynolds. Types, abstraction, and parametric polymorphism. In R. Mason, editor, Information Processing ,83, pages 513-523. North-Holland, 1984.
• 36: J. C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millenial Perspectives in Computer Science. Palgrave, 2001.
• 37: Clyde Ruby , Gary T. Leavens, Safely creating correct subclasses without seeing superclass code, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.208-228, October 2000, Minneapolis, Minnesota, United States
• 38: Christian Skalka , Scott Smith, Static enforcement of security with types, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.34-45, September 2000
• 40: 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]
• 41: D. von Oheimb, T. Nipkow, and C. Pusch. muJava: Embedding a programming language in a theorem prover. In Proceedings of the International Summer School Marktoberdorf, 1999.
• 42: Dan S. Wallach , Andrew W. Appel , Edward W. Felten, SAFKASI: a security mechanism for language-based systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.4, p.341-378, Oct. 2000 [doi>10.1145/363516.363520]