{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T05:57:53Z","timestamp":1785304673941,"version":"3.55.0"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986819","type":"print"},{"value":"9783031986826","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Runtime enforcers receive events from a system and output commands ensuring the system\u2019s policy compliance. Proactive enforcers extend traditional (reactive) enforcers by emitting commands at any time, rather only as a response to system actions. However, proactive enforcers have so far lacked support for many useful policy features. This, along with the existing tools\u2019 poor performance, hinders their adoption. We present a performance-optimized, proactive enforcement algorithm for a rich policy language: metric first-order temporal logic with function applications, aggregations, and  bindings. We have implemented this algorithm in\n                    <jats:sc>EnfGuard<\/jats:sc>\n                    , the first proactive enforcer tool that supports the above constructs. We evaluated our tool using a novel set of six benchmarks containing both real-world and synthetic policies and logs, demonstrating that it enforces realistic policies out-of-the-box and achieves the necessary performance to be used in real-time systems.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-98682-6_19","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:15:14Z","timestamp":1753154114000},"page":"370-392","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Scaling Up Proactive Enforcement"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Hublet","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Leonardo","family":"Lima","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sr\u0111an","family":"Krsti\u0107","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dmitriy","family":"Traytel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Aceto, L., Cassar, I., Francalanza, A., Ingolfsdottir, A.: Bidirectional runtime enforcement of first-order branching-time properties. Logical Methods in Computer Science 19 (2023)","DOI":"10.46298\/lmcs-19(1:14)2023"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Aceto, L., Cassar, I., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: On first-order runtime enforcement of branching-time properties. Acta Informatica pp. 1\u201367 (2023)","DOI":"10.46298\/lmcs-19(1:14)2023"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"681","DOI":"10.1007\/978-3-030-29959-0_33","volume-title":"Computer Security \u2013 ESORICS 2019","author":"E Arfelt","year":"2019","unstructured":"Arfelt, E., Basin, D., Debois, S.: Monitoring the GDPR. In: Sako, K., Schneider, S.A., Ryan, P.Y.A. (eds.) 24th European Symposium on Research in Computer Security (ESORICS). LNCS, vol. 11735, pp. 681\u2013699. Springer (2019)"},{"issue":"3","key":"19_CR4","doi-asserted-by":"publisher","first-page":"247","DOI":"10.3233\/JCS-210078","volume":"32","author":"D Basin","year":"2024","unstructured":"Basin, D., Debois, S., Hildebrandt, T.: Proactive enforcement of provisions and obligations. J. Comput. Secur. 32(3), 247\u2013289 (2024)","journal-title":"J. Comput. Secur."},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Basin, D., Dietiker, D.S., Krsti\u0107, S., Pignolet, Y.A., Raszyk, M., Schneider, J., Ter-Gabrielyan, A.: Monitoring the internet computer. In: International Symposium on Formal Methods. pp. 383\u2013402. Springer (2023)","DOI":"10.1007\/978-3-031-27481-7_22"},{"issue":"10","key":"19_CR6","doi-asserted-by":"publisher","first-page":"1403","DOI":"10.1109\/TSE.2013.18","volume":"39","author":"D Basin","year":"2013","unstructured":"Basin, D., Harvan, M., Klaedtke, F., Zalinescu, E.: Monitoring data usage in distributed systems. IEEE Transactions on Software Engineering 39(10), 1403\u20131426 (2013)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"19_CR7","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/s10703-015-0222-7","volume":"46","author":"D Basin","year":"2015","unstructured":"Basin, D., Klaedtke, F., Marinovic, S., Z\u0103linescu, E.: Monitoring of temporal first-order properties with aggregations. Formal methods in system design 46, 262\u2013285 (2015)","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"19_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2699444","volume":"62","author":"D Basin","year":"2015","unstructured":"Basin, D., Klaedtke, F., M\u00fcller, S., Z\u0103linescu, E.: Monitoring metric first-order temporal properties. Journal of the ACM (JACM) 62(2), 1\u201345 (2015)","journal-title":"Journal of the ACM (JACM)"},{"key":"19_CR9","unstructured":"Bauer, L., Ligatti, J., Walker, D.: More enforceable security policies. In: Workshop on Foundations of Computer Security (FCS). Citeseer (2002)"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K., Lime, D.: UPPAAL-Tiga: Time for playing games! In: Damm, W., Hermanns, H. (eds.) International Conference Computer Aided Verification (CAV). LNCS, vol.\u00a04590, pp. 121\u2013125. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_14"},{"issue":"2","key":"19_CR11","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1145\/210197.210200","volume":"20","author":"J Chomicki","year":"1995","unstructured":"Chomicki, J.: Efficient checking of temporal integrity constraints using bounded history encoding. ACM Transactions on Database Systems (TODS) 20(2), 149\u2013186 (1995)","journal-title":"ACM Transactions on Database Systems (TODS)"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Unbeast: Symbolic bounded synthesis. In: Abdulla, P.A., Leino, K.R.M. (eds.) International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a06605, pp. 272\u2013275. Springer (2011)","DOI":"10.1007\/978-3-642-19835-9_25"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Erlingsson, \u00da., Schneider, F.: SASI enforcement of security policies: a retrospective. In: Kienzle, D., Zurko, M.E., Greenwald, S., Serbau, C. (eds.) Workshop on New Security Paradigms. pp. 87\u201395. ACM (1999)","DOI":"10.1145\/335169.335201"},{"key":"19_CR14","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.scico.2016.02.008","volume":"123","author":"Y Falcone","year":"2016","unstructured":"Falcone, Y., J\u00e9ron, T., Marchand, H., Pinisetty, S.: Runtime enforcement of regular timed properties by suppressing and delaying events. Science of Computer Programming 123, 2\u201341 (2016)","journal-title":"Science of Computer Programming"},{"issue":"2","key":"19_CR15","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/s10009-021-00609-z","volume":"23","author":"Y Falcone","year":"2021","unstructured":"Falcone, Y., Krsti\u0107, S., Reger, G., Traytel, D.: A taxonomy for classifying runtime verification tools. Int. J. Softw. Tools Technol. Transf. 23(2), 255\u2013284 (2021)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Falcone, Y., Pinisetty, S.: On the runtime enforcement of timed properties. In: Finkbeiner, B., Mariani, L. (eds.) 19th International Conference on Runtime Verification, (RV). LNCS, vol. 11757, pp. 48\u201369. Springer (2019)","DOI":"10.1007\/978-3-030-32079-9_4"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Fredrikson, M., Joiner, R., Jha, S., Reps, T.W., Porras, P.A., Sa\u00efdi, H., Yegneswaran, V.: Efficient runtime policy enforcement using counterexample-guided abstraction refinement. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 548\u2013563. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_39"},{"issue":"4","key":"19_CR18","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1214\/aoms\/1177729885","volume":"21","author":"FE Grubbs","year":"1950","unstructured":"Grubbs, F.E.: Sample criteria for testing outlying observations. Ann. Math. Statist. 21(4), 27\u201358 (1950)","journal-title":"Ann. Math. Statist."},{"issue":"2","key":"19_CR19","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1109\/TSC.2011.10","volume":"5","author":"S Hall\u00e9","year":"2012","unstructured":"Hall\u00e9, S., Villemaire, R.: Runtime enforcement of web service message contracts with data. IEEE Trans. Serv. Comput. 5(2), 192\u2013206 (2012)","journal-title":"IEEE Trans. Serv. Comput."},{"issue":"4","key":"19_CR20","doi-asserted-by":"publisher","first-page":"880","DOI":"10.1145\/502090.502100","volume":"48","author":"L Hella","year":"2001","unstructured":"Hella, L., Libkin, L., Nurmonen, J., Wong, L.: Logics with aggregate operators. J. ACM 48(4), 880\u2013907 (2001). https:\/\/doi.org\/10.1145\/502090.502100","journal-title":"J. ACM"},{"issue":"5\u20137","key":"19_CR21","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.jlap.2013.05.005","volume":"82","author":"T Hildebrandt","year":"2013","unstructured":"Hildebrandt, T., Mukkamala, R.R., Slaats, T., Zanitti, F.: Contracts for cross-organizational workflows as timed dynamic condition response graphs. The Journal of Logic and Algebraic Programming 82(5-7), 164\u2013185 (2013)","journal-title":"The Journal of Logic and Algebraic Programming"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Hofmann, T., Schupp, S.: TACoS: A tool for MTL controller synthesis. In: Calinescu, R., Pasareanu, C.S. (eds.) International Conference on Software Engineering and Formal Methods (SEFM). LNCS, vol. 13085, pp. 372\u2013379. Springer (2021)","DOI":"10.1007\/978-3-030-92124-8_21"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Hublet, F., Basin, D., Krsti\u0107, S.: Real-time policy enforcement with metric first-order temporal logic. In: European Symposium on Research in Computer Security. pp. 211\u2013232. Springer (2022)","DOI":"10.1007\/978-3-031-17146-8_11"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Hublet, F., Lima, L., Basin, D., Krsti\u0107, S., Traytel, D.: Proactive real-time first-order enforcement. In: International Conference on Computer Aided Verification. pp. 156\u2013181. Springer (2024)","DOI":"10.1007\/978-3-031-65630-9_8"},{"key":"19_CR25","doi-asserted-by":"publisher","unstructured":"Hublet, F., Lima, L., Basin, D., Krsti\u0107, S., Traytel, D.: Scaling-up proactive enforcement: Technical report (2025), https:\/\/doi.org\/10.5281\/zenodo.15501642","DOI":"10.5281\/zenodo.15501642"},{"key":"19_CR26","unstructured":"Hublet, Fran\u00e7ois and Lima, Leonardo and Basin, David and Krsti\u0107, Sr\u0111an and Traytel, Dmitriy: EnfGuard (2025), https:\/\/github.com\/runtime-enforcement\/enfguard"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: International Conference Formal Methods in Computer-Aided Design (FMCAD). pp. 117\u2013124. IEEE (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"19_CR28","unstructured":"Kiukkonen, N., Blom, J., Dousse, O., Gatica-Perez, D., Laurila, J.: Towards rich mobile phone datasets: Lausanne data collection campaign. Proc. ICPS, Berlin 68(7) (2010)"},{"key":"19_CR29","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001). https:\/\/doi.org\/10.1023\/A:1011254632723, https:\/\/doi.org\/10.1023\/A:1011254632723","DOI":"10.1023\/A:1011254632723"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"Li, G., Jensen, P., Larsen, K., Legay, A., Poulsen, D.: Practical controller synthesis for MTL$$ _{0},{\\infty}$$. In: Erdogmus, H., Havelund, K. (eds.) ACM SIGSOFT International SPIN Symposium on Model Checking of Software. pp. 102\u2013111. ACM (2017)","DOI":"10.1145\/3092282.3092303"},{"key":"19_CR31","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/s10207-004-0046-8","volume":"4","author":"J Ligatti","year":"2005","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Edit automata: Enforcement mechanisms for run-time security policies. International Journal of Information Security 4, 2\u201316 (2005)","journal-title":"International Journal of Information Security"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Lima, L., Huerta\u00a0y Munive, J.J., Traytel, D.: Explainable online monitoring of metric first-order temporal logic. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 288\u2013307. Springer (2024)","DOI":"10.1007\/978-3-031-57246-3_16"},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"Minato, S.i.: Binary decision diagrams and applications for VLSI CAD, vol.\u00a0342. Springer Science & Business Media (1995)","DOI":"10.1007\/978-1-4613-1303-8"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Ngo, M., Massacci, F., Milushev, D., Piessens, F.: Runtime enforcement of security policies on black box reactive programs. In: Rajamani, S.K., Walker, D. (eds.) 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). pp. 43\u201354. ACM (2015)","DOI":"10.1145\/2676726.2676978"},{"key":"19_CR35","doi-asserted-by":"crossref","unstructured":"Peter, H., Ehlers, R., Mattm\u00fcller, R.: Synthia: Verification and synthesis for timed automata. In: Gopalakrishnan, G., Qadeer, S. (eds.) International Conference on Computer Aided Verification (CAV). LNCS,vol.\u00a06806, pp. 649\u2013655. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_52"},{"key":"19_CR36","doi-asserted-by":"crossref","unstructured":"Pinisetty, S., Falcone, Y., J\u00e9ron, T., Marchand, H.: TiPEX: A tool chain for timed property enforcement during execution. In: International Conference on Runtime Verification (RV). pp. 306\u2013320. Springer (2015)","DOI":"10.1007\/978-3-319-23820-3_22"},{"issue":"3","key":"19_CR37","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/s10703-014-0215-y","volume":"45","author":"S Pinisetty","year":"2014","unstructured":"Pinisetty, S., Falcone, Y., J\u00e9ron, T., Marchand, H., Rollet, A., Nguena\u00a0Timo, O.: Runtime enforcement of timed properties revisited. Formal Methods Syst. Des. 45, 381\u2013422 (2014)","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"19_CR38","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/s10703-017-0271-1","volume":"51","author":"S Pinisetty","year":"2017","unstructured":"Pinisetty, S., Preoteasa, V., Tripakis, S., J\u00e9ron, T., Falcone, Y., Marchand, H.: Predictive runtime enforcement. Formal Methods Syst. Des. 51(1), 154\u2013199 (2017)","journal-title":"Formal Methods in System Design"},{"key":"19_CR39","doi-asserted-by":"crossref","unstructured":"Raszyk, M., Basin, D., Krsti\u0107, S., Traytel, D.: Efficient evaluation of arbitrary relational calculus queries. Logical Methods in Computer Science 19 (2023)","DOI":"10.46298\/lmcs-19(4:38)2023"},{"key":"19_CR40","doi-asserted-by":"crossref","unstructured":"Renard, M., Rollet, A., Falcone, Y.: GREP: games for the runtime enforcement of properties. In: Yevtushenko, N., Cavalli, A., Yenig\u00fcn, H. (eds.) International Conference on Testing Software and Systems (ICTSS). LNCS, vol. 10533, pp. 259\u2013275. Springer (2017)","DOI":"10.1007\/978-3-319-67549-7_16"},{"issue":"1","key":"19_CR41","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F Schneider","year":"2000","unstructured":"Schneider, F.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30\u201350 (2000)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"19_CR42","unstructured":"The DFINITY Team: The Internet Computer for geeks. Cryptology ePrint Archive, Paper 2022\/087 (2022), https:\/\/eprint.iacr.org\/2022\/087"},{"key":"19_CR43","doi-asserted-by":"crossref","unstructured":"Zhu, S., Tabajara, L., Li, J., Pu, G., Vardi, M.: A symbolic approach to safety LTL synthesis. In: Strichman, O., Tzoref-Brill, R. (eds.) International Haifa Verification Conference (HVC). LNCS, vol. 10629, pp. 147\u2013162. Springer (2017)","DOI":"10.1007\/978-3-319-70389-3_10"},{"key":"19_CR44","doi-asserted-by":"crossref","unstructured":"Zingg, S., Krsti\u0107, S., Raszyk, M., Schneider, J., Traytel, D.: Verified first-order monitoring with recursive rules. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 236\u2013253. Springer (2022)","DOI":"10.1007\/978-3-030-99527-0_13"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98682-6_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T10:31:21Z","timestamp":1783506681000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98682-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986819","9783031986826"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98682-6_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}