Run-Time Enforcement of Nonsafety Policies

ABSTRACT

A common mechanism for ensuring that software behaves securely is to monitor programs at run time and check that they dynamically adhere to constraints specified by a security policy. Whenever a program monitor detects that untrusted software is attempting to execute a dangerous action, it takes remedial steps to ensure that only safe code actually gets executed.

This article improves our understanding of the space of policies enforceable by monitoring the run-time behaviors of programs. We begin by building a formal framework for analyzing policy enforcement: we precisely define policies, monitors, and enforcement. This framework allows us to prove that monitors enforce an interesting set of policies that we call the infinite renewal properties. We show how to construct a program monitor that provably enforces any reasonable infinite renewal property. We also show that the set of infinite renewal properties includes some nonsafety policies, that is, that monitors can enforce some nonsafety (including some purely liveness) policies. Finally, we demonstrate concrete examples of nonsafety policies enforceable by practical run-time monitors.

REFERENCES

• 1: Abadi, M. and Fournet, C. 2003. Access control based on execution history. In Proceedings of the 10th Annual Network and Distributed System Symposium (NDSS’03).
• 2: Martín Abadi , Leslie Lamport, Composing specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.73-132, Jan. 1993 [doi>10.1145/151646.151649]
• 3: Irem Aktug , Mads Dam , Dilian Gurov, Provably Correct Runtime Monitoring, Proceedings of the 15th international symposium on Formal Methods, May 26-30, 2008, Turku, Finland [doi>10.1007/978-3-540-68237-0_19]
• 4: Alpern, B. and Schneider, F. B. 1985. Defining liveness. Inform. Process. Lett. 21, 4, 181--185.
• 5: Alpern, B. and Schneider, F. B. 1987. Recognizing safety and liveness. Distrib. Comput. 2, 117--126.
• 6: Bauer, L., Ligatti, J., and Walker, D. 2002. More enforceable security policies. In Proceedings of the Annual Symposium on Foundations of Computer Security (FOCS’02). Copenhagen, Denmark.
• 7: Bauer, L., Ligatti, J., and Walker, D. 2003. Types and effects for non-interfering program monitors. In Proceedings of the Software Security---Theories and Systems. Mext-NSF-JSPS International Symposium, (ISSS’02). Tokyo, Japan, Revised Papers, M. Okada, B. Pierce, A. Scedrov, H. Tokuda, and A. Yonezawa, Eds. Lecture Notes in Computer Science, vol. 2609. Springer.
• 8: 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
• 9: Bauer, L., Ligatti, J., and Walker, D. 2005b. Polymer: A language for composing run-time security policies. http://www.cs.princeton.edu/sip/projects/polymer/.
• 10: Biba, K. J. 1975. Integrity considerations for secure computer systems. Tech. rep. ESD-TR-76-372, MITRE Corporation.
• 11: Piero Bonatti , Sabrina De Capitani di Vimercati , Pierangela Samarati, An algebra for composing access control policies, ACM Transactions on Information and System Security (TISSEC), v.5 n.1, p.1-35, February 2002 [doi>10.1145/504909.504910]
• 12: Brewer, D. F. C. and Nash, M. J. 1989. The Chinese Wall security policy. In Proceedings of the IEEE Symposium on Security and Privacy (SP’89). 206--214.
• 13: Büchi, J. R. 1962. On a decision method in restricted second order arithmetic. In Proceedings of the 1960 International Congress on Logic, Methodology, and Philosophy of Science (CLMPS’60). 1--11.
• 14: Nicodemos Damianou , Naranker Dulay , Emil Lupu , Morris Sloman, The Ponder Policy Specification Language, Proceedings of the International Workshop on Policies for Distributed Systems and Networks, p.18-38, January 29-31, 2001
• 15: Guy Edjlali , Anurag Acharya , Vipin Chaudhary, History-based access control for mobile code, Proceedings of the 5th ACM conference on Computer and communications security, p.38-48, November 02-05, 1998, San Francisco, California, United States [doi>10.1145/288090.288102]
• 16: Ramez Elmasri , Shamkant B. Navathe, Fundamentals of database systems, Benjamin-Cummings Publishing Co., Inc., Redwood City, CA, 1989
• 17: Ulfar Erlingsson , Fred B. Schneider, The inlined reference monitor approach to security policy enforcement, Cornell University, Ithaca, NY, 2004
• 18: Ú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]
• 19: 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
• 20: David E. Evans , John V. Guttag, Policy-directed code safety, Massachusetts Institute of Technology, 2000
• 21: Evans, D. and Twyman, A. 1999. Flexible policy-directed code safety. In Proceedings of the IEEE Symposium on Security and Privacy (SP’99).
• 22: Fong, P. W. L. 2004. Access control by tracking shallow execution history. In Proceedings of the IEEE Symposium on Security and Privacy (SP’04).
• 23: Kevin Hamlen , Greg Morrisett, Security policy enforcement by automated program-rewriting, Cornell University, Ithaca, NY, 2006
• 24: 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]
• 25: 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]
• 26: Tim Harris , Simon Marlow , Simon Peyton-Jones , Maurice Herlihy, Composable memory transactions, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065952]
• 27: Klaus Havelund , Grigore Roşu, Efficient monitoring of safety properties, International Journal on Software Tools for Technology Transfer (STTT), v.6 n.2, p.158-173, August 2004 [doi>10.1007/s10009-003-0117-6]
• 28: Clinton Jeffery , Wenyi Zhou , Kevin Templer , Michael Brazell, A lightweight architecture for program execution monitoring, Proceedings of the 1998 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.67-74, June 16-16, 1998, Montreal, Quebec, Canada
• 29: Kim, M., Kannan, S., Lee, I., Sokolsky, O., and Viswantathan, M. 2002. Computational analysis of run-time monitoring---fundamentals of Java-MaC. In Proceedings of the 2nd International Workshop on Runtime Verification (RV’02).
• 30: Kim, M., Viswanathan, M., Ben-Abdallah, H., Kannan, S., Lee, I., and Sokolsky, O. 1999. Formally specified monitoring of temporal properties. In Proceedings of the 11th Euromicro Conference on Real-Time Systems (ECRTS’99).
• 31: L. Lamport, Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering, v.3 n.2, p.125-143, March 1977 [doi>10.1109/TSE.1977.229904]
• 32: Yingsha Liao , Donald Cohen, A Specificational Approach to High Level Program Monitoring and Measuring, IEEE Transactions on Software Engineering, v.18 n.11, p.969-978, November 1992 [doi>10.1109/32.177366]
• 33: Jarred Adam Ligatti , David P. Walker, Policy enforcement via program monitoring, Princeton University, Princeton, NJ, 2006
• 34: Ligatti, J., Bauer, L., and Walker, D. 2003. Edit automata: Enforcement mechanisms for run-time security policies. Tech. rep. TR-681-03, Princeton University.
• 35: Ligatti, J., Bauer, L., and Walker, D. 2005a. Edit automata: Enforcement mechanisms for run-time security policies. Int. J. Inform. Secur. 4, 1--2, 2--16.
• 36: Ligatti, J., Bauer, L., and Walker, D. 2005b. Enforcing non-safety security policies with program monitors. In Proceedings of the 10th European Symposium on Research in Computer Security (ESORICS’05).
• 37: Nancy A. Lynch , Mark R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.137-151, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41852]
• 38: Heiko Mantel, On the Composition of Secure Systems, Proceedings of the 2002 IEEE Symposium on Security and Privacy, p.88, May 12-15, 2002
• 39: Fabio Martinelli , Ilaria Matteucci, An Approach for the Specification, Verification and Synthesis of Secure Systems, Electronic Notes in Theoretical Computer Science (ENTCS), 168, p.29-43, February, 2007 [doi>10.1016/j.entcs.2006.12.003]
• 40: Fabio Martinell , Ilaria Matteucci, Through Modeling to Synthesis of Security Automata, Electronic Notes in Theoretical Computer Science (ENTCS), 179, p.31-46, July, 2007 [doi>10.1016/j.entcs.2006.08.029]
• 41: Martinelli, F. and Mori, P. 2007. Enhancing Java security with history based access control. In Foundations of Security Analysis and Design.
• 42: Matteucci, I. 2006. A tool for the synthesis of programmable controllers. In Proceedings of the 4th International Workshop on Formal Aspects in Security and Trust (FAST’06).
• 43: Ilaria Matteucci, Automated Synthesis of Enforcing Mechanisms for Security Properties in a Timed Setting, Electronic Notes in Theoretical Computer Science (ENTCS), 186, p.101-120, July, 2007 [doi>10.1016/j.entcs.2007.03.025]
• 44: John McLean, A General Theory of Composition for a Class of "Possibilistic" Properties, IEEE Transactions on Software Engineering, v.22 n.1, p.53-67, January 1996 [doi>10.1109/32.481534]
• 45: Milner, R. 1978. Synthesis of communicating behaviour. In Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 64. 71--83.
• 46: William H. Paxton, A client-based transaction system to maintain data integrity, Proceedings of the seventh ACM symposium on Operating systems principles, p.18-23, December 10-12, 1979, Pacific Grove, California, United States [doi>10.1145/800215.806565]
• 47: W. Robinson, Monitoring Software Requirements Using Instrumented Code, Proceedings of the 35th Annual Hawaii International Conference on System Sciences (HICSS'02)-Volume 9, p.276.2, January 07-10, 2002
• 48: Fred B. Schneider, Decomposing Properties into Safety and Liveness, Cornell University, Ithaca, NY, 1987
• 49: 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]
• 50: Koushik Sen , Abhay Vardhan , Gul Agha , Grigore Rosu, Efficient Decentralized Monitoring of Safety in Distributed Systems, Proceedings of the 26th International Conference on Software Engineering, p.418-427, May 23-28, 2004
• 51: Nir Shavit , Dan Touitou, Software transactional memory, Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing, p.204-213, August 20-23, 1995, Ottowa, Ontario, Canada [doi>10.1145/224964.224987]
• 52: Mahesh Viswanathan , Sampath Kannan , Insup Lee, Foundations for the run-time analysis of software systems, University of Pennsylvania, Philadelphia, PA, 2000
• 53: Robert Wahbe , Steven Lucco , Thomas E. Anderson , Susan L. Graham, Efficient software-based fault isolation, Proceedings of the fourteenth ACM symposium on Operating systems principles, p.203-216, December 05-08, 1993, Asheville, North Carolina, United States
• 54: 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]
• 55: Dachuan Yu , Ajay Chander , Nayeem Islam , Igor Serikov, JavaScript instrumentation for browser security, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.0 General
          Subjects: Protection mechanisms

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation; Formal methods
      D.2.5 Testing and Debugging
          Subjects: Monitors

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Interactive and reactive computation

General Terms:
Security, Theory

Keywords:
Security policies, liveness, monitoring, policy enforcement, safety, security automata