Aspect-oriented in-lined reference monitors

ABSTRACT

An Aspect-Oriented, declarative, security policy specification language is presented, for enforcement by In-lined Reference Monitors. The semantics of the language establishes a formal connection between Aspect-Oriented Programming and In-lined Reference Monitoring wherein policy specifications denote Aspect-Oriented security automata---security automata whose edge labels are encoded as pointcut expressions. The prototype language implementation enforces these security policies by automatically rewriting Java bytecode programs so as to detect and prevent policy violations at runtime.

REFERENCES

• 1: Irem Aktug and Katsiaryna Naliuka. ConSpec: A formal language for policy specification. In Proc. of the 1st International Workshop on Run Time Enforcement for Mobile and Distributed Systems (REM'07), volume 197--1 of Lecture Notes in Theoretical Computer Science, pages 45---58, Dresden, Germany, September 2007.
• 2: Irem Aktug, Mads Dam, and Dilian Gurov. Provably correct runtime monitoring. In Proc. of the 15th International Symposium on Formal Methods (FM'08), Turku, Finland, May 2008. To appear.
• 3: Alexander Barvinok and James E. Pommersheim. An algorithmic theory of lattice points in polyhedra. New Perspectives in Algebraic Combinatorics, 38:91--147, 1999.
• 4: Lujo Bauer , Jay Ligatti , David Walker, Composing security policies with polymer, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 5: Feng Chen and Grigore Roşu. Java--MOP: A Monitoring Oriented Programming environment for Java. In Proc. of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 546--550, Edinburgh, Scotland, United Kingdom, April 2005.
• 6: Daniel S. Dantas , David Walker, Harmless advice, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.383-396, January 11-13, 2006, Charleston, South Carolina, USA
• 7: Daniel S. Dantas , David Walker , Geoffrey Washburn , Stephanie Weirich, AspectML: A polymorphic aspect-oriented functional programming language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.3, p.1-60, May 2008 [doi>10.1145/1353445.1353448]
• 8: Robert DeLine and Manuel Fähndrich. Typestates for objects. In Proc. of the 18th European Conference on Object--Oriented Programming (ECOOP), pages 465--490, Oslo, Norway, June 2004.
• 9: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 10: Ulfar Erlingsson , Fred B. Schneider, The inlined reference monitor approach to security policy enforcement, Cornell University, Ithaca, NY, 2004
• 11: Úlfar Erlingsson , Fred B. Schneider, SASI enforcement of security policies: a retrospective, Proceedings of the 1999 workshop on New security paradigms, p.87-95, September 22-24, 1999, Caledon Hills, Ontario, Canada [doi>10.1145/335169.335201]
• 12: David Evans and Andrew Twynman. Flexible policy--directed code safety. In Proc. of the 20th IEEE Symposium on Security and Privacy, pages 32--45, Oakland, California, May 1999.
• 13: Matthew Flatt , Shriram Krishnamurthi , Matthias Felleisen, Classes and mixins, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268961]
• 14: Apache Software Foundation. Byte code engineering library, 2006. http://jakarta.apache.org/bcel/.
• 15: Kevin Hamlen , Greg Morrisett, Security policy enforcement by automated program-rewriting, Cornell University, Ithaca, NY, 2006
• 16: Kevin W. Hamlen , Greg Morrisett , Fred B. Schneider, Computability classes for enforcement mechanisms, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.1, p.175-205, January 2006 [doi>10.1145/1111596.1111601]
• 17: Kevin W. Hamlen , Greg Morrisett , Fred B. Schneider, Certified In-lined Reference Monitoring on .NET, Proceedings of the 2006 workshop on Programming languages and analysis for security, June 10-10, 2006, Ottawa, Ontario, Canada [doi>10.1145/1134744.1134748]
• 18: Gregor Kiczales, John Lamping, Anurag Medhdhekar, Chris Maeda, Cristina Lopes, Jean--Marc Loingtier, and John Irwin. Aspect--Oriented Programming. In Proc. of the 11th European Conference on Object--Oriented Programming (ECOOP), volume 1241, pages 220--242, Jyvaskyla, Finland, June 1997.
• 19: Gregor Kiczales , Erik Hilsdale , Jim Hugunin , Mik Kersten , Jeffrey Palm , William G. Griswold, An Overview of AspectJ, Proceedings of the 15th European Conference on Object-Oriented Programming, p.327-353, June 18-22, 2001
• 20: Moonzoo Kim , Mahesh Viswanathan , Sampath Kannan , Insup Lee , Oleg Sokolsky, Java-MaC: A Run-Time Assurance Approach for Java Programs, Formal Methods in System Design, v.24 n.2, p.129-155, March 2004 [doi>10.1023/B:FORM.0000017719.43755.7c]
• 21: Gary T. Leavens , Albert L. Baker, Enhancing the Pre- and Postcondition Technique for More Expressive Specifications, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume II, p.1087-1106, September 20-24, 1999
• 22: Jarred Ligatti, Lujo Bauer, and David Walker. Edit automata: Enforcement mechanisms for run--time security policies. International Journal of Information Security, 4(1---2):2--16, February 2005.
• 23: Jay Ligatti, Lujo Bauer, and David Walker. Enforcing nonsafety security policies with program monitors. In Proc. of the 10th European Symposium on Research in Computer Security (ESORICS), pages 355--373, Milan, Italy, September 2005.
• 24: George C. Necula , Peter Lee, The design and implementation of a certifying compiler, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.333-344, June 17-19, 1998, Montreal, Quebec, Canada
• 25: Peri Tarr , Harold Ossher, Hyper/J: multi-dimensional separation of concerns for Java, Proceedings of the 23rd International Conference on Software Engineering, p.729-730, May 12-19, 2001, Toronto, Ontario, Canada
• 26: Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000 [doi>10.1145/353323.353382]
• 27: Viren Shah and Frank Hill. An aspect--oriented security framework. In Proc. of the DARPA Information Survivability Conference and Exposition, volume 2, pages 143--145, April 2003.
• 28: John Viega, J.T. Bloch, and Pravir Chandra. Applying aspectoriented programming to security. Cutter IT Journal, 14(2), February 2001.
• 29: David Walker , Steve Zdancewic , Jay Ligatti, A theory of aspects, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.127-139, August 25-29, 2003, Uppsala, Sweden
• 30: Mitchell Wand , Gregor Kiczales , Christopher Dutchyn, A semantics for advice and dynamic join points in aspect-oriented programming, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.5, p.890-910, September 2004 [doi>10.1145/1018203.1018208]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Access controls

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics

General Terms:
Languages, Security

Keywords:
aspect-oriented programming, in-lined reference monitors, object-oriented programming, runtime verification, security automata