Enforcement monitoring wrt. the safety-progress classification of properties: NOTE: ACM has found that the authors of this paper failed to cite a work they previously published with much identical content entitled Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties. Published in December 2008 in the Springer LNCS series for the ICISS 2008 conference DOI= http://dx.doi.org/10.1007/978-3-540-89862-7_3

ABSTRACT

Runtime enforcement is a powerful technique to ensure that a program will respect a given set of properties. We extend previous works on this topic in several directions. Firstly, we propose a generic notion of enforcement monitors based on a memory device and finite sets of control states and enforcement operations. Moreover, we specify their enforcement abilities wrt. the general safety-progress classification of properties. Furthermore, we propose a systematic technique to produce an enforcing monitor from the automaton recognizing a given safety, guarantee, or response property. Finally, we depict a prototype toolbox implementing the features proposed in this paper.

REFERENCES

• 1: Bowen Alpern , Fred B. Schneider, Defining Liveness, Cornell University, Ithaca, NY, 1984
• 2: AT&T Research. Graph Visualization Software. http://www.graphviz.org, 2007.
• 3: E. Chang, Z. Manna, and A. Pnueli. The safety-progress classification. Technical report, Stanford University, Dept. of Computer Science, 1992.
• 4: Edward Y. Chang , Zohar Manna , Amir Pnueli, Characterization of Temporal Property Classes, Proceedings of the 19th International Colloquium on Automata, Languages and Programming, p.474-486, July 13-17, 1992
• 5: Ú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]
• 6: Ulfar Erlingsson , Fred B. Schneider, The inlined reference monitor approach to security policy enforcement, Cornell University, Ithaca, NY, 2004
• 7: 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
• 8: Y. Falcone, J.-C. Fernandez, and L. Mounier. Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties. Technical Report TR-2008-7, Verimag Research Report, 2008.
• 9: P. W. L. Fong. Access control by tracking shallow execution history. sp, 00: 43, 2004.
• 10: 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]
• 11: G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. Lopes, J.-M. Loingtier, and J. Irwin. Aspect-oriented programming. pages 220--242. Springer-Verlag, 1997.
• 12: 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]
• 13: J. Ligatti, L. Bauer, and D. Walker. Composing Expressive Run-time Security Policies. ACM Transactions on Software Engineering and Methodology, Nov. 07.
• 14: Jay Ligatti , Lujo Bauer , David Walker, Run-Time Enforcement of Nonsafety Policies, ACM Transactions on Information and System Security (TISSEC), v.12 n.3, p.1-41, January 2009 [doi>10.1145/1455526.1455532]
• 15: J. Ligatti, L. Bauer, and D. Walker. Enforcing non-safety security policies with program monitors. In ESORICS, pages 355--373, 2005.
• 16: Nicholas Nethercote , Julian Seward, Valgrind: a framework for heavyweight dynamic binary instrumentation, ACM SIGPLAN Notices, v.42 n.6, June 2007
• 17: 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]
• 18: Robert S. Streett, Propositional Dynamic Logic of looping and converse, Proceedings of the thirteenth annual ACM symposium on Theory of computing, p.375-383, May 11-13, 1981, Milwaukee, Wisconsin, United States [doi>10.1145/800076.802492]
• 19: The Apache Jakarta Project. Byte Code Engineering Library. http://jakarta.apache.org/bcel/.
• 20: Mahesh Viswanathan , Sampath Kannan , Insup Lee, Foundations for the run-time analysis of software systems, University of Pennsylvania, Philadelphia, PA, 2000

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation; Reliability

General Terms:
Theory, Verification

Keywords:
monitor, property, runtime enforcement, safety-progress, synthesis