{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T02:07:13Z","timestamp":1758593233509,"version":"3.44.0"},"reference-count":66,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,8,9]],"date-time":"2025-08-09T00:00:00Z","timestamp":1754697600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,8,9]],"date-time":"2025-08-09T00:00:00Z","timestamp":1754697600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100014988","name":"Institute of Science and Technology","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100014988","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Enforcement of information-flow policies has been extensively studied by language-based approaches over the past few decades. In this paper, we propose an alternative, novel, general, and effective approach using enforcement of <jats:italic>hyperproperties<\/jats:italic>\u2013 a powerful formalism for expressing and reasoning about a wide range of information-flow security policies. We study <jats:italic>black-<\/jats:italic> vs. <jats:italic>gray-<\/jats:italic> vs. <jats:italic>white-box<\/jats:italic> enforcement of hyperproperties expressed by nondeterministic finite-word hyperautomata (NFH), where the enforcer has null, some, or complete information about the implementation of the system under scrutiny. Given an NFH, in order to generate a runtime enforcer, we reduce the problem to controller synthesis for hyperproperties and subsequently to the satisfiability problem for quantified Boolean formulas (QBFs). The resulting enforcers are transferable with low-overhead. We conduct a rich set of case studies, including information-flow control for JavaScript code, as well as synthesizing obfuscators for control plants.<\/jats:p>","DOI":"10.1007\/s00236-025-00502-1","type":"journal-article","created":{"date-parts":[[2025,8,9]],"date-time":"2025-08-09T07:22:02Z","timestamp":1754724122000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Gray-box runtime enforcement of hyperproperties"],"prefix":"10.1007","volume":"62","author":[{"given":"Tzu-Han","family":"Hsu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ana","family":"Oliveira da Costa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Wintenberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Borzoo","family":"Bonakdarpour","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,9]]},"reference":[{"key":"502_CR1","doi-asserted-by":"crossref","unstructured":"Algehed, M., Flanagan, C.: Transparent IFC enforcement: Possibility and (in)efficiency results. In: 2020 IEEE 33rd Computer Security Foundations Symposium (CSF), pp. 65\u201378 (2020). doi:10.1109\/CSF49147.2020.00013","DOI":"10.1109\/CSF49147.2020.00013"},{"key":"502_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Cern\u00fd, P., Zdancewic, S.: Preserving secrecy under refinement. In: Proceedings of the 33rd Automata, Languages and Programming, International Colloquium (ICALP), pp. 107\u2013118 (2006)","DOI":"10.1007\/11787006_10"},{"key":"502_CR3","doi-asserted-by":"crossref","unstructured":"Askarov, A., Hunt, S., Sabelfeld, A., Sands, D.: Termination-insensitive noninterference leaks more than just a bit. In: Proceedings of 13th European Symposium on Research in Computer Security Computer Security (ESORICS), pp. 333\u2013348 (2008)","DOI":"10.1007\/978-3-540-88313-5_22"},{"key":"502_CR4","doi-asserted-by":"crossref","unstructured":"Askarov, A., Sabelfeld, A.: Gradual release: Unifying declassification, encryption and key release policies. In: 2007 IEEE Symposium on Security and Privacy (SP\u201907), pp. 207\u2013221 (2007). IEEE","DOI":"10.1109\/SP.2007.22"},{"key":"502_CR5","doi-asserted-by":"crossref","unstructured":"Askarov, A., Sabelfeld, A.: Tight enforcement of information-release policies for dynamic languages. In: 2009 22nd IEEE Computer Security Foundations Symposium, pp. 43\u201359 (2009)","DOI":"10.1109\/CSF.2009.22"},{"key":"502_CR6","doi-asserted-by":"crossref","unstructured":"Askarov, A., Chong, S., Mantel, H.: Hybrid monitors for concurrent noninterference. In: 2015 IEEE 28th Computer Security Foundations Symposium, pp. 137\u2013151 (2015)","DOI":"10.1109\/CSF.2015.17"},{"key":"502_CR7","doi-asserted-by":"publisher","unstructured":"Austin, T.H., Flanagan, C.: Multiple facets for dynamic information flow. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 165\u2013178 (2012). https:\/\/doi.org\/10.1145\/2103656.2103677","DOI":"10.1145\/2103656.2103677"},{"key":"502_CR8","doi-asserted-by":"crossref","unstructured":"Austin, T.H., Flanagan, C.: Efficient purely-dynamic information flow analysis. In: ACM Transactions on Programming Languages and Systems, pp. 113\u2013124 (2009)","DOI":"10.1145\/1554339.1554353"},{"key":"502_CR9","doi-asserted-by":"publisher","unstructured":"Backes, M., Kopf, B., Rybalchenko, A.: Automatic discovery and quantification of information leaks. In: Proceedings of the 2009 30th IEEE Symposium on Security and Privacy, pp. 141\u2013153. IEEE Computer Society, USA (2009). https:\/\/doi.org\/10.1109\/SP.2009.18","DOI":"10.1109\/SP.2009.18"},{"key":"502_CR10","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-45193-8_8","volume-title":"Principles and Practice of Constraint Programming - CP 2003","author":"O Bailleux","year":"2003","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient cnf encoding of boolean cardinality constraints. In: Rossi, F. (ed.) Principles and Practice of Constraint Programming - CP 2003, pp. 108\u2013122. Springer, Berlin, Heidelberg (2003)"},{"key":"502_CR11","unstructured":"Bauer, L., Ligatti, J., Walker, D.: More enforceable security policies. In: Proceedings of the Workshop on Foundations of Computer Security (FCS\u201902), Copenhagen, Denmark (2002)"},{"key":"502_CR12","doi-asserted-by":"publisher","unstructured":"Bindschaedler, V., Shokri, R., Gunter, C.A.: Plausible deniability for privacy-preserving data synthesis 10(5), 481\u2013492 https:\/\/doi.org\/10.14778\/3055540.3055542","DOI":"10.14778\/3055540.3055542"},{"key":"502_CR13","doi-asserted-by":"publisher","unstructured":"Bielova, N., Rezk, T.: Spot the difference: Secure multi-execution and multiple facets. In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) 21st European Symposium on Research in Computer Security (ESORICS), pp. 501\u2013519 (2016). https:\/\/doi.org\/10.1007\/978-3-319-45744-4_25","DOI":"10.1007\/978-3-319-45744-4_25"},{"key":"502_CR14","doi-asserted-by":"publisher","unstructured":"Bhuiyan, M.H.M., Parthasarathy, A.S., Vasilakis, N., Pradel, M., Staicu, C.-A.: Secbench.js: An executable security benchmark suite for server-side javascript. In: 2023 IEEE\/ACM 45th International Conference on Software Engineering (ICSE), pp. 1059\u20131070 (2023). https:\/\/doi.org\/10.1109\/ICSE48619.2023.00096","DOI":"10.1109\/ICSE48619.2023.00096"},{"key":"502_CR15","doi-asserted-by":"crossref","unstructured":"Bonakdarpour, B., Sheinvald, S.: Finite-word hyperlanguages. In: Proceedings of the 15th International Conference on Language and Automata Theory and Applications (LATA), pp. 173\u2013186 (2021)","DOI":"10.1007\/978-3-030-68195-1_17"},{"key":"502_CR16","doi-asserted-by":"crossref","unstructured":"Bonakdarpour, B., Finkbeiner, B.: Controller synthesis for hyperproperties. In: Proceedings of the 33rd IEEE Computer Security Foundations Symposium (CSF), pp. 366\u2013379 (2020)","DOI":"10.1109\/CSF49147.2020.00033"},{"key":"502_CR17","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.jlamp.2016.08.006","volume":"87","author":"M Bugliesi","year":"2017","unstructured":"Bugliesi, M., Calzavara, S., Focardi, R.: Formal methods for web security. Journal of Logical and Algebraic Methods in Programming 87, 110\u2013126 (2017)","journal-title":"Journal of Logical and Algebraic Methods in Programming"},{"issue":"6","key":"502_CR18","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. Journal of Computer Security 18(6), 1157\u20131210 (2010)","journal-title":"Journal of Computer Security"},{"key":"502_CR19","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Proceedings of the 3rd Conference on Principles of Security and Trust POST, pp. 265\u2013284 (2014)","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"502_CR20","doi-asserted-by":"crossref","unstructured":"Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J., Schillo, Y.: Runtime enforcement of hyperproperties. In: Proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 283\u2013299 (2021)","DOI":"10.1007\/978-3-030-88885-5_19"},{"key":"502_CR21","doi-asserted-by":"crossref","unstructured":"De\u00a0Groef, W., Devriese, D., Nikiforakis, N., Piessens, F.: Flowfox: A web browser with flexible and precise information flow control. In: Proceedings of the 2012 ACM Conference on Computer and Communications Security. CCS \u201912 (2012)","DOI":"10.1145\/2382196.2382275"},{"key":"502_CR22","doi-asserted-by":"crossref","unstructured":"D, D., Piessens, F.: Noninterference through secure multi-execution. In: Proceedings of the 31st IEEE Symposium on Security and Privacy, S &P, pp. 109\u2013124 (2010)","DOI":"10.1109\/SP.2010.15"},{"key":"502_CR23","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11499107_32","volume-title":"Theory and Applications of Satisfiability Testing","author":"N Dershowitz","year":"2005","unstructured":"Dershowitz, N., Hanna, Z., Katz, J.: Bounded model checking with QBF. In: Bacchus, F., Walsh, T. (eds.) Theory and Applications of Satisfiability Testing, pp. 408\u2013414. Springer, Berlin, Heidelberg (2005)"},{"issue":"3","key":"502_CR24","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/s10703-011-0114-4","volume":"38","author":"Y Falcone","year":"2011","unstructured":"Falcone, Y., Mounier, L., Fernandez, J.-C., Richier, J.-U.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods in System Design 38(3), 223\u2013262 (2011)","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"502_CR25","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/s10009-011-0196-8","volume":"14","author":"Y Falcone","year":"2012","unstructured":"Falcone, Y., Fernandez, J., Mounier, L.: What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Transfer (STTT) 14(3), 349\u2013382 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transfer (STTT)"},{"key":"502_CR26","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: 20th Annual IEEE Symposium on Logic in Computer Science (LICS\u2019 05), pp. 321\u2013330 (2005). https:\/\/doi.org\/10.1109\/LICS.2005.53","DOI":"10.1109\/LICS.2005.53"},{"key":"502_CR27","doi-asserted-by":"crossref","unstructured":"Guernic, G.L.: Automaton-based confidentiality monitoring of concurrent programs. In: 20th IEEE Computer Security Foundations Symposium (CSF\u201907), pp. 218\u2013232 (2007)","DOI":"10.1109\/CSF.2007.10"},{"key":"502_CR28","doi-asserted-by":"crossref","unstructured":"Hedin, D., Birgisson, A., Bello, L., Sabelfeld, A.: Jsflow: Tracking information flow in javascript and its apis. In: Proceedings of the 29th Annual ACM Symposium on Applied Computing. SAC \u201914 (2014)","DOI":"10.1145\/2554850.2554909"},{"key":"502_CR29","doi-asserted-by":"crossref","unstructured":"Hedin, D., Bello, L., Sabelfeld, A.: Value-sensitive hybrid information flow control for a javascript-like language. In: 2015 IEEE 28th Computer Security Foundations Symposium, pp. 351\u2013365 (2015)","DOI":"10.1109\/CSF.2015.31"},{"key":"502_CR30","doi-asserted-by":"crossref","unstructured":"Hsu, T.-H., S\u00e1nchez, C., Bonakdarpour, B.: Bounded model checking for hyperproperties. In: Proceedings of the 27th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS) (2021). To appear","DOI":"10.1007\/978-3-030-72016-2_6"},{"key":"502_CR31","doi-asserted-by":"crossref","unstructured":"Jang, D., Jhala, R., Lerner, S., Shacham, H.: An empirical study of privacy-violating information flows in javascript web applications. In: Proceedings of the 17th ACM Conference on Computer and Communications Security, pp. 270\u2013283 (2010)","DOI":"10.1145\/1866307.1866339"},{"issue":"1","key":"502_CR32","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.cosrev.2012.01.001","volume":"6","author":"R Khoury","year":"2012","unstructured":"Khoury, R., Tawbi, N.: Which security policies are enforceable by runtime monitors? A survey. Computer Science Review 6(1), 27\u201345 (2012). https:\/\/doi.org\/10.1016\/j.cosrev.2012.01.001","journal-title":"Computer Science Review"},{"issue":"2","key":"502_CR33","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/s10703-017-0276-9","volume":"51","author":"B K\u00f6nighofer","year":"2017","unstructured":"K\u00f6nighofer, B., Alshiekh, M., Bloem, R., Humphrey, L.R., K\u00f6nighofer, R., Topcu, U., Wang, C.: Shield synthesis. Formal Methods in System Design 51(2), 332\u2013361 (2017)","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"502_CR34","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. Int. J. Inf. Secur. 4(1), 2\u201316 (2005)","journal-title":"Int. J. Inf. Secur."},{"key":"502_CR35","unstructured":"Linus, R.: Social Media Fingerprint. https:\/\/robinlinus.github.io\/socialmedia-leak\/ (2023 (accessed August 3, 2023))"},{"key":"502_CR36","doi-asserted-by":"crossref","unstructured":"Loring, B., Mitchell, D., Kinder, J.: Expose: practical symbolic execution of standalone javascript. In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, pp. 196\u2013199 (2017)","DOI":"10.1145\/3092282.3092295"},{"key":"502_CR37","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.entcs.2006.08.029","volume":"179","author":"F Martinell","year":"2007","unstructured":"Martinell, F., Matteucci, I.: Through modeling to synthesis of security automata. Proceedings of the Second International Workshop on Security and Trust Management (STM 2006) 179, 31\u201346 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2006.08.029","journal-title":"Proceedings of the Second International Workshop on Security and Trust Management (STM 2006)"},{"key":"502_CR38","doi-asserted-by":"crossref","unstructured":"McCall, M., Bichhawat, A., Jia, L.: Compositional information flow monitoring for reactive programs. In: 2022 IEEE 7th European Symposium on Security and Privacy (EuroS &P), pp. 467\u2013486 (2022)","DOI":"10.1109\/EuroSP53844.2022.00036"},{"key":"502_CR39","doi-asserted-by":"crossref","unstructured":"McCullough, D.: Noninterference and the composability of security properties. In: Proceedings of the 1988 IEEE Symposium on Security and Privacy, pp. 177\u2013186 (1988)","DOI":"10.1109\/SECPRI.1988.8110"},{"key":"502_CR40","doi-asserted-by":"crossref","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proc. IEEE Symposium on Security and Privacy, pp. 79\u201393 (1994)","DOI":"10.1109\/RISP.1994.296590"},{"key":"502_CR41","doi-asserted-by":"crossref","unstructured":"Moore, S., Chong, S.: Static analysis for efficient hybrid information-flow control. In: 2011 IEEE 24th Computer Security Foundations Symposium, pp. 146\u2013160 (2011)","DOI":"10.1109\/CSF.2011.17"},{"key":"502_CR42","doi-asserted-by":"publisher","unstructured":"Ngo, M., Bielova, N., Flanagan, C., Rezk, T., Russo, A., Schmitz, T.: A better facet of dynamic information flow control. In: Companion Proceedings of The Web Conference 2018, pp. 731\u2013739 (2018). https:\/\/doi.org\/10.1145\/3184558.3185979","DOI":"10.1145\/3184558.3185979"},{"key":"502_CR43","doi-asserted-by":"publisher","unstructured":"Ngo, M., Massacci, F., Milushev, D., Piessens, F.: Runtime enforcement of security policies on black box reactive programs. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 43\u201354. Association for Computing Machinery (2015). https:\/\/doi.org\/10.1145\/2676726.2676978","DOI":"10.1145\/2676726.2676978"},{"key":"502_CR44","unstructured":"O\u2019Halloran, C.: A calculus of information flow. Proceedings of the European Symposium on Research in Computer Security (1990)"},{"issue":"1","key":"502_CR45","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 in System Design 51(1), 154\u2013199 (2017)","journal-title":"Formal Methods in System Design"},{"key":"502_CR46","doi-asserted-by":"crossref","unstructured":"Russo, A., Sabelfeld, A.: Dynamic vs. static flow-sensitive security analysis. In: 2010 23rd IEEE Computer Security Foundations Symposium, pp. 186\u2013199 (2010)","DOI":"10.1109\/CSF.2010.20"},{"issue":"1","key":"502_CR47","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2006","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5\u201319 (2006)","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"502_CR48","doi-asserted-by":"publisher","unstructured":"Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: 18th IEEE Computer Security Foundations Workshop (CSFW\u201905), pp. 255\u2013269 (2005). https:\/\/doi.org\/10.1109\/CSFW.2005.15","DOI":"10.1109\/CSFW.2005.15"},{"key":"502_CR49","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Russo, A.: From dynamic to static and back: Riding the roller coaster of information-flow control research. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) Perspectives of Systems Informatics (2010)","DOI":"10.1007\/978-3-642-11486-1_30"},{"key":"502_CR50","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-030-53288-8_11","volume-title":"Computer Aided Verification","author":"S Sahai","year":"2020","unstructured":"Sahai, S., Subramanyan, P., Sinha, R., Lahiri, S.K., Wang, C.: Verification of quantitative hyperproperties using trace enumeration relations. In: Computer Aided Verification, pp. 201\u2013224. Springer, Cham (2020)"},{"key":"502_CR51","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Transactions on Information and System Security 3, 30\u201350 (2000)","journal-title":"ACM Transactions on Information and System Security"},{"key":"502_CR52","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Myers, A.C.: A model for delimited information release. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) Software Security - Theories and Systems, pp. 174\u2013191. Springer (2004)","DOI":"10.1007\/978-3-540-37621-7_9"},{"key":"502_CR53","doi-asserted-by":"crossref","unstructured":"Sen, K., Kalasapur, S., Brutch, T., Gibbs, S.: Jalangi: A selective record-replay and dynamic analysis framework for javascript. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, pp. 488\u2013498 (2013)","DOI":"10.1145\/2491411.2491447"},{"key":"502_CR54","doi-asserted-by":"crossref","unstructured":"Shroff, P., Smith, S., Thober, M.: Dynamic dependency monitoring to secure information flow. In: 20th IEEE Computer Security Foundations Symposium (CSF\u201907), pp. 203\u2013217 (2007)","DOI":"10.1109\/CSF.2007.20"},{"key":"502_CR55","doi-asserted-by":"crossref","unstructured":"Staicu, C.-A., Schoepe, D., Balliu, M., Pradel, M., Sabelfeld, A.: An empirical study of information flows in real-world javascript. In: Proceedings of the 14th ACM SIGSAC Workshop on Programming Languages and Analysis for Security, pp. 45\u201359 (2019)","DOI":"10.1145\/3338504.3357339"},{"key":"502_CR56","doi-asserted-by":"crossref","unstructured":"Stefan, D., Russo, A., Mitchell, J.C., Mazi\u00e8res, D.: Flexible dynamic information flow control in haskell. In: Proceedings of the 4th ACM Symposium on Haskell. Haskell \u201911 (2011)","DOI":"10.1145\/2034675.2034688"},{"key":"502_CR57","doi-asserted-by":"publisher","unstructured":"Tong, Y., Ma, Z., Li, Z., Seatzu, C., Giua, A.: Supervisory enforcement of current-state opacity with uncomparable observations. In: 2016 13th International Workshop on Discrete Event Systems (WODES), pp. 313\u2013318 (2016). https:\/\/doi.org\/10.1109\/WODES.2016.7497865","DOI":"10.1109\/WODES.2016.7497865"},{"issue":"1","key":"502_CR58","doi-asserted-by":"publisher","first-page":"155","DOI":"10.3233\/SAT190121","volume":"11","author":"L Tentrup","year":"2019","unstructured":"Tentrup, L.: CAQE and QuAbS: Abstraction based QBF solvers. Journal of Satisfiability Boolean Modeling and Computation 11(1), 155\u2013210 (2019)","journal-title":"Journal of Satisfiability Boolean Modeling and Computation"},{"key":"502_CR59","doi-asserted-by":"crossref","unstructured":"Vanhoef, M., De\u00a0Groef, W., Devriese, D., Piessens, F., Rezk, T.: Stateful declassification policies for event-driven programs. In: 2014 IEEE 27th Computer Security Foundations Symposium, pp. 293\u2013307 (2014). IEEE","DOI":"10.1109\/CSF.2014.28"},{"issue":"2","key":"502_CR60","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","volume":"68","author":"JP Warners","year":"1998","unstructured":"Warners, J.P.: A linear-time transformation of linear inequalities into conjunctive normal form. Inf. Process. Lett. 68(2), 63\u201369 (1998). https:\/\/doi.org\/10.1016\/S0020-0190(98)00144-6","journal-title":"Inf. Process. Lett."},{"key":"502_CR61","doi-asserted-by":"publisher","unstructured":"Wintenberg, A., Blischke, M., Lafortune, S., Ozay, N.: A dynamic obfuscation framework for security and utility. In: 2022 ACM\/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS), pp. 236\u2013246 (2022). https:\/\/doi.org\/10.1109\/ICCPS54341.2022.00028","DOI":"10.1109\/ICCPS54341.2022.00028"},{"issue":"1","key":"502_CR62","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10817-017-9420-x","volume":"60","author":"Y-C Wu","year":"2017","unstructured":"Wu, Y.-C., Raman, V., Rawlings, B.C., Lafortune, S., Seshia, S.A.: Synthesis of obfuscation policies to ensure privacy and utility. J. Autom. Reason. 60(1), 107\u2013131 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9420-x","journal-title":"J. Autom. Reason."},{"key":"502_CR63","doi-asserted-by":"crossref","unstructured":"Wu, M., Zeng, H., Wang, C., Yu, H.: Safety guard: Runtime enforcement for safety-critical cyber-physical systems. In: Proceedings of the Design Automation Conference, pp. 84\u20131846 (2017)","DOI":"10.1145\/3061639.3072957"},{"key":"502_CR64","doi-asserted-by":"publisher","unstructured":"Zakinthinos, A., Lee, E.S.: A general theory of security properties. In: Proceedings. 1997 IEEE Symposium on Security and Privacy, pp. 94\u2013102 (1997). https:\/\/doi.org\/10.1109\/SECPRI.1997.601322","DOI":"10.1109\/SECPRI.1997.601322"},{"key":"502_CR65","doi-asserted-by":"publisher","unstructured":"Zanarini, D., Jaskelioff, M., Russo, A.: Precise enforcement of confidentiality for reactive systems. In: 2013 IEEE 26th Computer Security Foundations Symposium, pp. 18\u201332 (2013). https:\/\/doi.org\/10.1109\/CSF.2013.9","DOI":"10.1109\/CSF.2013.9"},{"key":"502_CR66","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW), pp. 29\u201343 (2003)","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00502-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-025-00502-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00502-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,22]],"date-time":"2025-09-22T06:26:17Z","timestamp":1758522377000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-025-00502-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,9]]},"references-count":66,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["502"],"URL":"https:\/\/doi.org\/10.1007\/s00236-025-00502-1","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2025,8,9]]},"assertion":[{"value":"4 December 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 July 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 August 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"This project was funded in part by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502, Vienna Science and Technology Fund (WWTF) [10.47379\/ICT19018] (ProbInG) and WWTF project ICT22-023 (TAIGER), NSF CPS Award 1837680, NSF award ECCS-2144416 and NSF SaTC Award 2245114.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"30"}}