Certified In-lined Reference Monitoring on .NET

ABSTRACT

MOBILE is an extension of the .NET Common Intermediate Language that supports certified In-Lined Reference Monitoring. Mobile programs have the useful property that if they are well-typed with respect to a declared security policy, then they are guaranteed not to violate that security policy when executed. Thus, when an In-Lined Reference Monitor (IRM) is expressed in Mobile, it can be certified by a simple type-checker to eliminate the need to trust the producer of the IRM.Security policies in Mobile are declarative, can involve unbounded collections of objects allocated at runtime, and can regard infinite-length histories of security events exhibited by those objects. The prototype Mobile implementation enforces properties expressed by finite-state security automata - one automaton for each security-relevant object - and can type-check Mobile programs in the presence of exceptions, finalizers, concurrency, and non-termination. Executing Mobile programs requires no change to existing .NET virtual machine implementations, since Mobile programs consist of normal managed CIL code with extra typing annotations stored in .NET attributes.

REFERENCES

• 1: 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
• 2: Andrew Bernard , Peter Lee, Engineering formal security policies for proof-carrying code, 2004
• 3: Andrew Bernard , Peter Lee, Temporal Logic for Proof-Carrying Code, Proceedings of the 18th International Conference on Automated Deduction, p.31-46, July 27-30, 2002
• 4: Feng Chen and Grigore Rosu. Java-MOP: A monitoring oriented programming environment for Java. In Proceedings of the Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 546--550, Edinburgh, U.K., April 2005.
• 5: Dave Clarke , Sophia Drossopoulou, Ownership, encapsulation and the disjointness of type and effect, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 6: 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
• 7: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 8: Robert DeLine and Manuel Fähndrich. The Fugue protocol checker: Is your software baroque? Technical Report MSR-TR-2004-07, Microsoft Research, Redmond, Washington, January 2004.
• 9: Robert DeLine and Manuel Fähndrich. Typestates for objects. In 18th European Conference on Object-Oriented Programming, pages 465--490, Oslo, Norway, June 2004.
• 10: ECMA. ECMA-335: Common Language Infrastructure (CLI). ECMA (European Association for Standardizing Information and Communication Systems), Geneva, Switzerland, second edition, December 2002.
• 11: Ulfar Erlingsson , Fred B. Schneider, IRM Enforcement of Java Stack Inspection, Proceedings of the 2000 IEEE Symposium on Security and Privacy, p.246, May 14-17, 2000
• 12: Ú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]
• 13: David Evans and Andrew Twynman. Flexible policy-directed code safety. In IEEE Symposium on Security and Privacy, pages 32--45, Oakland, California, May 1999.
• 14: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 15: Li Gong. Java™ 2 platform security architecture, version 1.2. Whitepaper. ©1997-2002 Sun Microsystems, Inc.
• 16: Andrew D. Gordon , Don Syme, Typing a multi-language intermediate code, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.248-260, January 2001, London, United Kingdom
• 17: Kevin W. Hamlen, Greg Morrisett, and Fred B. Schneider. Certified in-lined reference monitoring on .NET. Technical Report TR-2005-2003, Cornell University, Ithaca, New York, November 2005.
• 18: 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]
• 19: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 20: Andrew Kennedy , Don Syme, Design and implementation of generics for the .NET Common language runtime, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.1-12, June 2001, Snowbird, Utah, United States
• 21: 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]
• 22: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 23: Greg Morrisett, Amal Ahmed, and Matthew Fluet. L³: A linear language with locations. In 7th International Conference on Typed Lambda Calculi and Applications (TLCA), pages 293--307, Nara, Japan, April 2005.
• 24: Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25--35, Atlanta, Georgia, May 1999.
• 25: 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
• 26: Peter W. O'Hearn , John C. Reynolds , Hongseok Yang, Local Reasoning about Programs that Alter Data Structures, Proceedings of the 15th International Workshop on Computer Science Logic, p.1-19, September 10-13, 2001
• 27: Michael F. Ringenburg , Dan Grossman, Types for describing coordinated data structures, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.25-36, January 10-10, 2005, Long Beach, California, USA [doi>10.1145/1040294.1040297]
• 28: 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]
• 29: Christian Skalka and Scott F. Smith. History effects and verification. In Asian Programming Languages Symposium (APLAS), pages 107--128, November 2004.
• 30: Frederick Smith , David Walker , J. Gregory Morrisett, Alias Types, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.366-381, April 02, 2000
• 31: Don Syme. ILX: Extending the .NET Common IL for functional language interoperability. In Nick Benton and Andrew Kennedy, editors, First International Workshop on Multi-Language Infrastructure and Interoperability, volume 59.1, Florence, Italy, September 2001.
• 32: David Walker, A type system for expressive security policies, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.254-267, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325728]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.2 Automatic Programming

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
  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.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)

General Terms:
Security

Keywords:
execution monitoring, in-lined reference monitoring, program rewriting, reference monitors, security automata