{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:49:06Z","timestamp":1770752946467,"version":"3.50.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000183","name":"Army Research Office","doi-asserted-by":"publisher","award":["DAAD19-02-1-0389"],"award-info":[{"award-number":["DAAD19-02-1-0389"]}],"id":[{"id":"10.13039\/100000183","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CNS-0716216"],"award-info":[{"award-number":["CNS-0716216"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CNS-0716343"],"award-info":[{"award-number":["CNS-0716343"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CNS-0742736"],"award-info":[{"award-number":["CNS-0742736"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Inf. Syst. Secur."],"published-print":{"date-parts":[[2009,1]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>","DOI":"10.1145\/1455526.1455532","type":"journal-article","created":{"date-parts":[[2009,2,4]],"date-time":"2009-02-04T13:01:58Z","timestamp":1233752518000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":134,"title":["Run-Time Enforcement of Nonsafety Policies"],"prefix":"10.1145","volume":"12","author":[{"given":"Jay","family":"Ligatti","sequence":"first","affiliation":[{"name":"University of South Florida"}]},{"given":"Lujo","family":"Bauer","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}]},{"given":"David","family":"Walker","sequence":"additional","affiliation":[{"name":"Princeton University"}]}],"member":"320","published-online":{"date-parts":[[2009,1]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 10th Annual Network and Distributed System Symposium (NDSS\u201903)","author":"Abadi M.","unstructured":"<scp> Abadi , M. and Fournet , C . <\/scp> 2003. Access control based on execution history . In Proceedings of the 10th Annual Network and Distributed System Symposium (NDSS\u201903) . <scp>Abadi, M. and Fournet, C.<\/scp> 2003. Access control based on execution history. In Proceedings of the 10th Annual Network and Distributed System Symposium (NDSS\u201903)."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151649"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_19"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01782772"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the Annual Symposium on Foundations of Computer Security (FOCS\u201902)","author":"Bauer L.","unstructured":"<scp> Bauer , L. , Ligatti , J. , and Walker , D . <\/scp> 2002. More enforceable security policies . In Proceedings of the Annual Symposium on Foundations of Computer Security (FOCS\u201902) . Copenhagen, Denmark. <scp>Bauer, L., Ligatti, J., and Walker, D.<\/scp> 2002. More enforceable security policies. In Proceedings of the Annual Symposium on Foundations of Computer Security (FOCS\u201902). Copenhagen, Denmark."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the Software Security---Theories and Systems. Mext-NSF-JSPS International Symposium, (ISSS\u201902)","volume":"2609","author":"Bauer L.","unstructured":"<scp> Bauer , L. , Ligatti , J. , and Walker , D . <\/scp> 2003. Types and effects for non-interfering program monitors . In Proceedings of the Software Security---Theories and Systems. Mext-NSF-JSPS International Symposium, (ISSS\u201902) . Tokyo, Japan, Revised Papers, M. Okada, B. Pierce, A. Scedrov, H. Tokuda, and A. Yonezawa, Eds. Lecture Notes in Computer Science , vol. 2609 . Springer. <scp>Bauer, L., Ligatti, J., and Walker, D.<\/scp> 2003. Types and effects for non-interfering program monitors. In Proceedings of the Software Security---Theories and Systems. Mext-NSF-JSPS International Symposium, (ISSS\u201902). Tokyo, Japan, Revised Papers, M. Okada, B. Pierce, A. Scedrov, H. Tokuda, and A. Yonezawa, Eds. Lecture Notes in Computer Science, vol. 2609. Springer."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065047"},{"key":"e_1_2_1_9_1","volume-title":"<\/scp>","author":"Bauer L.","year":"2005","unstructured":"<scp> Bauer , L. , Ligatti , J. , and Walker , D . <\/scp> 2005 b. Polymer : A language for composing run-time security policies. http:\/\/www.cs.princeton.edu\/sip\/projects\/polymer\/. <scp>Bauer, L., Ligatti, J., and Walker, D.<\/scp> 2005b. Polymer: A language for composing run-time security policies. http:\/\/www.cs.princeton.edu\/sip\/projects\/polymer\/."},{"key":"e_1_2_1_10_1","volume-title":"Integrity considerations for secure computer systems. Tech. rep. ESD-TR-76-372","author":"Biba K. J.","unstructured":"<scp> Biba , K. J. <\/scp> 1975. Integrity considerations for secure computer systems. Tech. rep. ESD-TR-76-372 , MITRE Corporation . <scp>Biba, K. J.<\/scp> 1975. Integrity considerations for secure computer systems. Tech. rep. ESD-TR-76-372, MITRE Corporation."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/504909.504910"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy (SP\u201989)","author":"Brewer D. F. C.","unstructured":"<scp> Brewer , D. F. C. and Nash , M. J . <\/scp> 1989. The Chinese Wall security policy . In Proceedings of the IEEE Symposium on Security and Privacy (SP\u201989) . 206--214. <scp>Brewer, D. F. C. and Nash, M. J.<\/scp> 1989. The Chinese Wall security policy. In Proceedings of the IEEE Symposium on Security and Privacy (SP\u201989). 206--214."},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 1960 International Congress on Logic, Methodology, and Philosophy of Science (CLMPS\u201960)","author":"B\u00fcchi J. R.","year":"1962","unstructured":"<scp> B\u00fcchi , J. R. <\/scp> 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\u201960) . 1--11. <scp>B\u00fcchi, J. R.<\/scp> 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\u201960). 1--11."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/646962.712108"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/288090.288102"},{"key":"e_1_2_1_16_1","volume-title":"<\/scp>","author":"Elmasri R.","year":"1994","unstructured":"<scp> Elmasri , R. and Navathe , S. B . <\/scp> 1994 . Fundamentals of Database Systems. The Benjamin\/ Cummings Publishing Company , Inc. <scp>Elmasri, R. and Navathe, S. B.<\/scp> 1994. Fundamentals of Database Systems. The Benjamin\/ Cummings Publishing Company, Inc."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/335169.335201"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/882494.884407"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy (SP\u201999)","author":"Evans D.","unstructured":"<scp> Evans , D. and Twyman , A . <\/scp> 1999. Flexible policy-directed code safety . In Proceedings of the IEEE Symposium on Security and Privacy (SP\u201999) . <scp>Evans, D. and Twyman, A.<\/scp> 1999. Flexible policy-directed code safety. In Proceedings of the IEEE Symposium on Security and Privacy (SP\u201999)."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.2004.1301314"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111596.1111601"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134744.1134748"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065944.1065952"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2944225.2944368"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/277631.277644"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the 2nd International Workshop on Runtime Verification (RV\u201902)","author":"Kim M.","unstructured":"<scp> Kim , M. , Kannan , S. , Lee , I. , Sokolsky , O. , and Viswantathan , M . <\/scp> 2002. Computational analysis of run-time monitoring---fundamentals of Java-MaC . In Proceedings of the 2nd International Workshop on Runtime Verification (RV\u201902) . <scp>Kim, M., Kannan, S., Lee, I., Sokolsky, O., and Viswantathan, M.<\/scp> 2002. Computational analysis of run-time monitoring---fundamentals of Java-MaC. In Proceedings of the 2nd International Workshop on Runtime Verification (RV\u201902)."},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 11th Euromicro Conference on Real-Time Systems (ECRTS\u201999)","author":"Kim M.","unstructured":"<scp> Kim , M. , Viswanathan , M. , Ben-Abdallah , H. , Kannan , S. , Lee , I. , and Sokolsky , O . <\/scp> 1999. Formally specified monitoring of temporal properties . In Proceedings of the 11th Euromicro Conference on Real-Time Systems (ECRTS\u201999) . <scp>Kim, M., Viswanathan, M., Ben-Abdallah, H., Kannan, S., Lee, I., and Sokolsky, O.<\/scp> 1999. Formally specified monitoring of temporal properties. In Proceedings of the 11th Euromicro Conference on Real-Time Systems (ECRTS\u201999)."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.177366"},{"key":"e_1_2_1_34_1","volume-title":"<\/scp>","author":"Ligatti J.","year":"2003","unstructured":"<scp> Ligatti , J. , Bauer , L. , and Walker , D . <\/scp> 2003 . Edit automata: Enforcement mechanisms for run-time security policies. Tech. rep. TR-681-03, Princeton University . <scp>Ligatti, J., Bauer, L., and Walker, D.<\/scp> 2003. Edit automata: Enforcement mechanisms for run-time security policies. Tech. rep. TR-681-03, Princeton University."},{"key":"e_1_2_1_35_1","first-page":"1","article-title":"Edit automata: Enforcement mechanisms for run-time security policies","volume":"4","author":"Ligatti J.","year":"2005","unstructured":"<scp> Ligatti , J. , Bauer , L. , and Walker , D. <\/scp> 2005 a. Edit automata: Enforcement mechanisms for run-time security policies . Int. J. Inform. Secur. 4 , 1 -- 2 , 2--16. <scp>Ligatti, J., Bauer, L., and Walker, D.<\/scp> 2005a. Edit automata: Enforcement mechanisms for run-time security policies. Int. J. Inform. Secur. 4, 1--2, 2--16.","journal-title":"Int. J. Inform. Secur."},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the 10th European Symposium on Research in Computer Security (ESORICS\u201905)","author":"Ligatti J.","unstructured":"<scp> Ligatti , J. , Bauer , L. , and Walker , D . <\/scp> 2005b. Enforcing non-safety security policies with program monitors . In Proceedings of the 10th European Symposium on Research in Computer Security (ESORICS\u201905) . <scp>Ligatti, J., Bauer, L., and Walker, D.<\/scp> 2005b. Enforcing non-safety security policies with program monitors. In Proceedings of the 10th European Symposium on Research in Computer Security (ESORICS\u201905)."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41852"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/829514.830531"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.003"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.08.029"},{"key":"e_1_2_1_41_1","volume-title":"<\/scp>","author":"Martinelli F.","year":"2007","unstructured":"<scp> Martinelli , F. and Mori , P . <\/scp> 2007 . Enhancing Java security with history based access control. In Foundations of Security Analysis and Design . <scp>Martinelli, F. and Mori, P.<\/scp> 2007. Enhancing Java security with history based access control. In Foundations of Security Analysis and Design."},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the 4th International Workshop on Formal Aspects in Security and Trust (FAST\u201906)","author":"Matteucci I.","year":"2006","unstructured":"<scp> Matteucci , I. <\/scp> 2006 . A tool for the synthesis of programmable controllers . In Proceedings of the 4th International Workshop on Formal Aspects in Security and Trust (FAST\u201906) . <scp>Matteucci, I.<\/scp> 2006. A tool for the synthesis of programmable controllers. In Proceedings of the 4th International Workshop on Formal Aspects in Security and Trust (FAST\u201906)."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.03.025"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.481534"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08921-7_57"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/800215.806565"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/820747.821306"},{"key":"e_1_2_1_48_1","volume-title":"Decomposing properties into safety and liveness using predicate logic. Tech. rep. TR 87-874","author":"Schneider F. B.","unstructured":"<scp> Schneider , F. B. <\/scp> 1987. Decomposing properties into safety and liveness using predicate logic. Tech. rep. TR 87-874 , Cornell University . <scp>Schneider, F. B.<\/scp> 1987. Decomposing properties into safety and liveness using predicate logic. Tech. rep. TR 87-874, Cornell University."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/353323.353382"},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the 26th International Conference on Software Engineering (ICSE\u201904)","author":"Sen K.","unstructured":"<scp> Sen , K. , Vardhan , A. , Agha , G. , and Rosu , G . <\/scp> 2004. Efficient decentralized monitoring of safety in distributed systems . In Proceedings of the 26th International Conference on Software Engineering (ICSE\u201904) . 418--427. <scp>Sen, K., Vardhan, A., Agha, G., and Rosu, G.<\/scp> 2004. Efficient decentralized monitoring of safety in distributed systems. In Proceedings of the 26th International Conference on Software Engineering (ICSE\u201904). 418--427."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/224964.224987"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/168619.168635"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325728"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190252"}],"container-title":["ACM Transactions on Information and System Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1455526.1455532","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1455526.1455532","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:18Z","timestamp":1750287258000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1455526.1455532"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1]]},"references-count":50,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,1]]}},"alternative-id":["10.1145\/1455526.1455532"],"URL":"https:\/\/doi.org\/10.1145\/1455526.1455532","relation":{},"ISSN":["1094-9224","1557-7406"],"issn-type":[{"value":"1094-9224","type":"print"},{"value":"1557-7406","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,1]]},"assertion":[{"value":"2007-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}