Anindya Banerjee
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.
- 1.M. Abadi, A. Banerjee, N. Heintze, and J. G. Riecke. A core calculus of dependency. In POPL, 1999.]] Google Scholar
Digital Library
- 2.A. Banerjee and D. A. Naumann. A static analysis for instance-based confinement in Java. In preparation.]]Google Scholar
- 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.]]Google Scholar
- 4.J. Boyland. Alias burying: Unique variables without destructive reads. Software Practice and Experience, 31(6), 2001.]] Google ScholarDigital Library
- 5.J. Boyland, J. Noble, and W. Retert. Capabilities for sharing: A generalisation of uniqueness and read-only. In ECOOP, 2001.]] Google ScholarDigital Library
- 6.A. Cavalcanti and D. A. Naumann. Forward simulation for data refinement of classes. Submitted, 2001.]]Google Scholar
- 7.D. G. Clarke, J. Noble, and J. M. Potter. Simple ownership types for object containment. In ECOOP 2001.]] Google ScholarDigital Library
- 8.W.-P. de Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, 1998.]]Google ScholarDigital Library
- 9.D. Detlefs and K. R. M. Leino and G. Nelson. Wrestling with rep exposure. Research Report 156, COMPAQ Systems Research Center, July 1998.]]Google Scholar
- 10.K. K. Dhara and G. T. Leavens. Forcing behavioral subtyping through specification inheritance. In ICSE, Berlin, 1996.]] Google ScholarDigital Library
- 11.L. Gong. Inside Java 2 Platform Security. Addison-Wesley, 1999.]] Google ScholarDigital Library
- 12.A. D. Gordon and A. M. Pitts, editors. Higher Order Operational Techniques in Semantics. Cambridge University Press, 1998.]] Google ScholarDigital Library
- 13.D. Grossman, G. Morrisett, and S. Zdancewic. Syntactic type abstraction. ACM Trans. Prog. Lang. Syst., 22(6), 2000.]] Google ScholarDigital Library
- 14.M. Huisman and B. Jacobs. Java program verification via a Hoare logic with abrupt termination. In FASE, 2000.]] Google ScholarDigital Library
- 15.A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java: a minimal core calculus for Java and GJ. In OOPSLA, 1999.]] Google ScholarDigital Library
- 16.S. Ishtiaq and P. W. O'Hearn. BI as an assertion language for mutable data structures. In POPL, 2001.]] Google ScholarDigital Library
- 17.D. Lea. Concurrent Programming in Java. Addison-Wesley, second edition, 2000.]] Google ScholarDigital Library
- 18.K. R. M. Leino and G. Nelson. Data abstraction and information hiding. Research Report 160, COMPAQ Systems Research Center, Nov. 2000. To appear in ACM Trans. Prog. Lang. Syst.]] Google ScholarDigital Library
- 19.B. H. Liskov and J. M. Wing. A behavioral notion of subtyping. ACM Trans. Prog. Lang. Syst., 16(6), 1994.]] Google ScholarDigital Library
- 20.N. Lynch and F. Vaandrager. Forward and backward simulations part I. Inf. Comput., 121(2), 1995.]] Google ScholarDigital Library
- 21.A. R. Meyer and K. Sieber. Towards fully abstract semantics for local variables: Preliminary report. In POPL, 1988.]] Google ScholarDigital Library
- 22.J. C. Mitchell. Representation independence and data abstraction. In POPL, 1986.]] Google ScholarDigital Library
- 23.J. C. Mitchell. On the equivalence of data representations. In V. Lifschitz, editor, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, 1991.]] Google ScholarDigital Library
- 24.J. C. Mitchell. Foundations for Programming Languages. MIT Press, 1996.]] Google ScholarDigital Library
- 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.]]Google Scholar
- 26.P. M. uller and A. Poetzsch-Heffter. Modular specification and verification techniques for object-oriented software components. In G. T. Leavens and M. Sitaraman, editors, Foundations of Component-Based Systems. Cambridge University Press, 2000.]] Google ScholarDigital Library
- 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.]]Google Scholar
- 28.D. A. Naumann. Soundness of data refinement for a higher order imperative language. Theoretical Comput. Sci., 2001. To appear.]] Google ScholarDigital Library
- 29.P. W. OHearn and R. D. Tennent. Parametricity and local variables. J. ACM, 42(3), 1995.]] Google ScholarDigital Library
- 30.P. W. OHearn and R. D. Tennent. Algol-like Languages (Two volumes). Birkh. auser, Boston, 1997.]] Google ScholarDigital Library
- 31.G. Plotkin. Lambda definability and logical relations. Technical Report SAI-RM-4, University of Edinburgh, School of Artificial Intelligence, 1973.]]Google Scholar
- 32.U. S. Reddy. Objects and classes in Algol-like languages. In FOOL, 1998.]]Google Scholar
- 33.J. C. Reynolds. Towards a theory of type structure. In Colloques sur la Programmation, LNCS 19, pages 408-425, 1974.]] Google ScholarDigital Library
- 34.J. C. Reynolds. The essence of Algol. In J. W. de Bakker and J. C. van Vliet, editors, Algorithmic Languages. North-Holland, 1981.]]Google Scholar
- 35.J. C. Reynolds. Types, abstraction, and parametric polymorphism. In R. Mason, editor, Information Processing ,83, pages 513-523. North-Holland, 1984.]]Google Scholar
- 36.J. C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millenial Perspectives in Computer Science. Palgrave, 2001.]]Google Scholar
- 37.C. Ruby and G. T. Leavens. Safely creating correct subclasses without seeing superclass code. In OOPSLA, 2000.]] Google ScholarDigital Library
- 38.C. Skalka and S. Smith. Static enforcement of security with types. In ICFP, 2000.]] Google ScholarDigital Library
- 40.J. Vitek and B. Bokowski. Confined types in java. Software Practice and Experience, 31(6), 2001.]] Google ScholarDigital Library
- 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.]]Google Scholar
- 42.D. Wallach, A. Appel, and E. Felten. SAFKASI: a security mechanism for language-based systems. ACM Trans. Software Eng. Method., 9(4), 2000.]] Google ScholarDigital Library
- Representation independence, confinement and access control [extended abstract]
Recommendations
Representation independence, confinement and access control [extended 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 ...
Configuring role-based access control to enforce mandatory and discretionary access control policies
Access control models have traditionally included mandatory access control (or lattice-based access control) and discretionary access control. Subsequently, role-based access control has been introduced, along with claims that its mechanisms are general ...
Concrete- and abstract-based access control
Access control models allow expressing access control rules (also called policies) stating that certain subjects (or users) have or do not have the right (or privilege) to access certain objects in order to execute certain actions under certain ...
Comments