Execution monitoring enforcement for limited-memory systems

ABSTRACT

Recently, attention has been given to formally characterize security policies that are enforceable by different kinds of security mechanisms. Since execution monitoring (EM) is a ubiquitous technique for enforcing security policies, this class of enforcement mechanisms has attracted the attention of the majority of authors characterizing security enforcement. A very important research problem is the characterization of security policies that are enforceable by execution monitors constrained by memory limitations. This paper contributes to give more precise answers to this research problem. To represent execution monitors constrained by memory limitations, we introduce a new class of automata that we call Bounded History Automata. Characterizing memory limitations gives rise to a precise taxonomy of security policies enforceable under such constraints.

This work is in the same line as the research work advanced by Schneider [31], Ligatti et. al [1, 21] and Fong [12] on security enforcement. Our main contribution consists in (1) instantiating Fong's abstraction idea to deal with memory-limitations, (2) defining Bounded History Automata by applying our abstraction to both security automata and edit automata [1], and (3) Reasoning about the enforcement power of bounded history automata by investigating the enforcement of locally testable properties; a well studied class of languages that are recognizable by investigating "local" information. Our approach gives rise to a realistic evaluation of the enforcement power of execution monitoring. This evaluation is based on bounding the memory size used by the monitor to save execution history, and identifying the security policies enforceable under such constraint.

REFERENCES

• 1: L. Bauer, J. Ligatti, and D. Walker. More enforceable security policies. In Foundations of Computer Security, pages 95--104, Copenhagen, Denmark, 25--26 July 2002. DIKU Technical Report.
• 2: L. Bauer, J. Ligatti, and D. Walker. Edit automata: Enforcement mechanisms for run-time security policies. Tech. Rep TR-681-03, Princeton University, May, 2003.
• 3: Lujo Bauer , Jay Ligatti , David Walker, Composing security policies with polymer, ACM SIGPLAN Notices, v.40 n.6, June 2005
• 4: D. Beauquier , J.-E. Pin, Languages and scanners, Theoretical Computer Science, v.84 n.1, p.3-21, July 22, 1991 [doi>10.1016/0304-3975(91)90258-4]
• 5: Jean Berstel , Jean-Eric Pin, Local languages and the Berry-Sethi algorithm, Theoretical Computer Science, v.155 n.2, p.439-446, March 11, 1996 [doi>10.1016/0304-3975(95)00104-2]
• 6: K. Biba. Integrity considerations for secure computer systems. Technical Report 76372, US Air Force Electronic Systems Division, 1977.
• 7: W. E. Boebert and R. Y. Kain. A practical alternative to hierarchical integrity policies. In In Proceedings of the 8th National Computer Security Conference, page 1827, October 1985.
• 8: D. F. C. Brewer and M. J. Nash. The chinese wall security policy. In IEEE Symposium on Security and Privacy, pages 206--214, May 1989.
• 9: Pascal Caron, Families of locally testable languages, Theoretical Computer Science, v.242 n.1-2, p.361-376, July 6, 2000 [doi>10.1016/S0304-3975(98)00332-6]
• 10: 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
• 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: P. L. Fong. Access control by tracking shallow execution history. In In Proceedings of the 2004 IEEE Symposium on Security and Privacy. Berkeley, California, May 2004.
• 13: Cédric Fournet , Andrew D. Gordon, Stack inspection: theory and variants, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.307-318, January 16-18, 2002, Portland, Oregon
• 14: Virgil D. Gligor, A note on denial-of-service in operating systems, IEEE Transactions on Software Engineering, v.10 n.3, p.320-324, May 1984 [doi>10.1109/TSE.1984.5010241]
• 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: 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, 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]
• 18: M. Kim, S. Kannan, I. Lee, S. Sokolsky, and M. Viswanathan. Computational analysis of run-time monitoring. In K. Havelund and G. Roşu, editors, Runtime Verification, volume 70 of Electronic Notes in Theoretical Computer Science, pages 81--95. Elsevier Science, July 26 2002.
• 19: 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]
• 20: J. Levy, H. Saidi, and T. E. Uribe. Combining monitors for runtime system verification. In K. Havelund and G. Rosu, editors, Electronic Notes in Theoretical Computer Science, volume 70. Elsevier, 2002.
• 21: J. Ligatti, L. Bauer, and D. Walker. Edit automata: Enforcement mechanisms for run-time security policies. International Journal of Information Security, 4(1--2):2--16, Feb. 2005. (Published online 26 Oct 2004.).
• 22: J. Ligatti, L. Bauer, and D. Walker. Enforcing non-safety security policies with program monitors. Technical Report TR-720-05, Princeton University, Jan. 2005.
• 23: A. Magnaghi and H. Tanaka. An efficient algorithm for order evaluation of strict locally testable languages.
• 24: 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]
• 25: D. Perrin and J. E. Pin. Infinite Words. Automata, Semigroups, Logic and Games, volume 141 of Pure and Applied Mathematics. Elsevier, 1004.
• 26: D. Perrin and J. Pin. Semigroups and automata on infinite words, 1995.
• 27: J.-E. Pin. Logic, semigroups and automata on words., 1994.
• 28: J. E. Pin. Finite semigroups and recognizable languages: an introduction. In J. Fountain, editor, NATO Advanced Study Institute Semigroups, Formal Languages and Groups, pages 1--32. Kluwer academic publishers, 1995.
• 29: A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5--19, Jan. 2003.
• 30: F. B. Schneider, G. Morrisett, and R. Harper. A language-based approach to security. Lecture Notes in Computer Science, 2000.
• 31: 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]
• 32: Sam M. Kim , Robert McNaughton , Robert McCloskey, A Polynomial time Algorithm for the Local Testability Problem of Deterministic Finite Automata, IEEE Transactions on Computers, v.40 n.10, p.1087-1093, October 1991 [doi>10.1109/12.93741]
• 33: Sam M. Kim , Robert McNaughton, Computing the Order of a Locally Testable Automaton, SIAM Journal on Computing, v.23 n.6, p.1193-1215, Dec. 1994 [doi>10.1137/S0097539791216987]
• 34: A. Taivalsaari. JSR 139 J2ME Connected Limited Device Configuration 1.1, March 2003.
• 35: A. N. Trahtman, An Algorithm to Verify Local Threshold Testability of Deterministic Finite Automata, Revised Papers from the 4th International Workshop on Automata Implementation, p.164-173, July 17-19, 1999
• 36: Mahesh Viswanathan , Sampath Kannan , Insup Lee, Foundations for the run-time analysis of software systems, University of Pennsylvania, Philadelphia, PA, 2000
• 37: P. A. T. W. D. Young and W. E. Boebert. A verified labler for the secure ada target. In In Proceedings of the 9th National Computer Security Conference, page 5561, September 1986.

INDEX TERMS

Keywords:
bounded history automata, edit automata, enforcement mechanisms, execution monitoring, locally-testable properties, security policies