{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T11:36:29Z","timestamp":1770896189029,"version":"3.50.1"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,6,1]],"date-time":"2013-06-01T00:00:00Z","timestamp":1370044800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006785","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":[[2013,6]]},"abstract":"<jats:p>We revisit Schneider\u2019s work on policy enforcement by execution monitoring. We overcome limitations of Schneider\u2019s setting by distinguishing between system actions that are controllable by an enforcement mechanism and those actions that are only observable, that is, the enforcement mechanism sees them but cannot prevent their execution. For this refined setting, we give necessary and sufficient conditions on when a security policy is enforceable. To state these conditions, we generalize the standard notion of safety properties. Our classification of system actions also allows one, for example, to reason about the enforceability of policies that involve timing constraints. Furthermore, for different specification languages, we investigate the decision problem of whether a given policy is enforceable. We provide complexity results and show how to synthesize an enforcement mechanism from an enforceable policy.<\/jats:p>","DOI":"10.1145\/2487222.2487225","type":"journal-article","created":{"date-parts":[[2013,6,18]],"date-time":"2013-06-18T12:36:08Z","timestamp":1371558968000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":46,"title":["Enforceable Security Policies Revisited"],"prefix":"10.1145","volume":"16","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[{"name":"ETH Zurich"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vincent","family":"Jug\u00e9","sequence":"additional","affiliation":[{"name":"MINES ParisTech"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felix","family":"Klaedtke","sequence":"additional","affiliation":[{"name":"ETH Zurich"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eugen","family":"Z\u0103linescu","sequence":"additional","affiliation":[{"name":"ETH Zurich"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/648143.749966"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/174644.174651"},{"key":"e_1_2_1_4_1","unstructured":"American National Standards Institute Inc. 2004. Role Based Access Control. American National Standards Institute Inc. Washington DC.  American National Standards Institute Inc. 2004. Role Based Access Control . American National Standards Institute Inc. Washington DC."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1229285.1229299"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 28th Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics Series","volume":"2","author":"Basin D.","unstructured":"Basin , D. , Klaedtke , F. , M\u00fcller , S. , and Pfitzmann , B . 2008. Runtime monitoring of metric first-order temporal properties . In Proceedings of the 28th Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics Series , vol. 2 , Schloss Dagstuhl - Leibniz Center for Informatics, 49--60. Basin, D., Klaedtke, F., M\u00fcller, S., and Pfitzmann, B. 2008. Runtime monitoring of metric first-order temporal properties. In Proceedings of the 28th Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics Series, vol. 2, Schloss Dagstuhl - Leibniz Center for Informatics, 49--60."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1809842.1809849"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2011.14"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_17"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_20"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97297"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2010.11.004"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/646246.684871"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592761.1592781"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1891823.1891830"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-010-0118-3"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.54.13"},{"key":"e_1_2_1_19_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 15th International Conference on Computer Aided Verification","author":"Eisner C.","unstructured":"Eisner , C. , Fisman , D. , Havlicek , J. , Lustig , Y. , McIsaac , A. , and Van Campenhout , D. 2003. Reasoning with temporal logic on truncated paths . In Proceedings of the 15th International Conference on Computer Aided Verification . Lecture Notes in Computer Science , vol. 2725 , Springer , 27--39. Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., and Van Campenhout, D. 2003. Reasoning with temporal logic on truncated paths. In Proceedings of the 15th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 2725, Springer, 27--39."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/335169.335201"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 246--255","author":"Erlingsson","unstructured":"Erlingsson , \u00da. and Schneider, F. B . 2000. IRM enforcement of Java stack inspection . In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 246--255 . Erlingsson, \u00da. and Schneider, F. B. 2000. IRM enforcement of Java stack inspection. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 246--255."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0114-4"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.2004.1301314"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046726"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2011.10"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111596.1111601"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/645880.672085"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the 16th IEEE International Conference on Automated Software Engineering. IEEE Computer Society, 135--143","author":"Havelund K.","unstructured":"Havelund , K. and Ro\u015fu , G . 2001. Monitoring programs using rewriting . In Proceedings of the 16th IEEE International Conference on Automated Software Engineering. IEEE Computer Society, 135--143 . Havelund, K. and Ro\u015fu, G. 2001. Monitoring programs using rewriting. In Proceedings of the 16th IEEE International Conference on Automated Software Engineering. IEEE Computer Society, 135--143."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(92)90005-G"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"e_1_2_1_32_1","unstructured":"Hopcroft J. E. and Ullman J. D. 1979. Introduction to Automata Theory Languages and Computation. Addison-Wesley Longman Boston MA.   Hopcroft J. E. and Ullman J. D. 1979. Introduction to Automata Theory Languages and Computation. Addison-Wesley Longman Boston MA."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(75)80050-X"},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the 11th Euromicro Conference on Real-Time Systems. IEEE Computer Society, 114--122","author":"Kim M.","unstructured":"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. IEEE Computer Society, 114--122 . 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. IEEE Computer Society, 114--122."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the 15th European Symposium on Research in Computer Security. Lecture Notes in Computer Science","volume":"6345","author":"Ligatti J.","unstructured":"Ligatti , J. and Reddy , S . 2010. A theory of runtime enforcement, with results . In Proceedings of the 15th European Symposium on Research in Computer Security. Lecture Notes in Computer Science , vol. 6345 . Springer, 87--100. Ligatti, J. and Reddy, S. 2010. A theory of runtime enforcement, with results. In Proceedings of the 15th European Symposium on Research in Computer Security. Lecture Notes in Computer Science, vol. 6345. Springer, 87--100."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0053-9"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455526.1455532"},{"key":"e_1_2_1_40_1","volume-title":"Counter-Free Automata. Research Monograph Series","volume":"65","author":"McNaughton R.","unstructured":"McNaughton , R. and Papert , S . 1971 . Counter-Free Automata. Research Monograph Series , vol. 65 , The MIT Press, Cambridge, MA. McNaughton, R. and Papert, S. 1971. Counter-Free Automata. Research Monograph Series, vol. 65, The MIT Press, Cambridge, MA."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/3640"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1151030.1151053"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.32.0114"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1137\/0325013"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/353323.353382"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.07.009"},{"key":"e_1_2_1_49_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 8th Banff Higher Order Workshop on Logics for Concurrency: Structure Versus Automata","author":"Vardi M. Y.","unstructured":"Vardi , M. Y. 1995. An automata-theoretic approach to linear temporal logic . In Proceedings of the 8th Banff Higher Order Workshop on Logics for Concurrency: Structure Versus Automata . Lecture Notes in Computer Science , vol. 1043 , Springer , 238--266. Vardi, M. Y. 1995. An automata-theoretic approach to linear temporal logic. In Proceedings of the 8th Banff Higher Order Workshop on Logics for Concurrency: Structure Versus Automata. Lecture Notes in Computer Science, vol. 1043, Springer, 238--266."},{"key":"e_1_2_1_50_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation","author":"Vardi M. Y.","unstructured":"Vardi , M. Y. 2007. Automata-theoretic model checking revisited . In Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation . Lecture Notes in Computer Science , vol. 4349 , Springer , 137--150. Vardi, M. Y. 2007. Automata-theoretic model checking revisited. In Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 4349, Springer, 137--150."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"}],"container-title":["ACM Transactions on Information and System Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2487222.2487225","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2487222.2487225","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:48:39Z","timestamp":1750236519000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2487222.2487225"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6]]},"references-count":50,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,6]]}},"alternative-id":["10.1145\/2487222.2487225"],"URL":"https:\/\/doi.org\/10.1145\/2487222.2487225","relation":{},"ISSN":["1094-9224","1557-7406"],"issn-type":[{"value":"1094-9224","type":"print"},{"value":"1557-7406","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,6]]},"assertion":[{"value":"2012-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-06-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}