[{"_id":"20186","title":"Gray-box runtime enforcement of hyperproperties","date_published":"2025-09-01T00:00:00Z","volume":62,"PlanS_conform":"1","publisher":"Springer Nature","month":"09","date_updated":"2025-09-30T14:20:11Z","language":[{"iso":"eng"}],"OA_type":"hybrid","has_accepted_license":"1","license":"https://creativecommons.org/licenses/by/4.0/","status":"public","type":"journal_article","external_id":{"isi":["001546115300001"]},"author":[{"last_name":"Hsu","full_name":"Hsu, Tzu Han","first_name":"Tzu Han"},{"last_name":"Oliveira Da Costa","full_name":"Oliveira Da Costa, Ana A","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","first_name":"Ana A"},{"last_name":"Wintenberg","full_name":"Wintenberg, Andrew","first_name":"Andrew"},{"first_name":"Ezio","full_name":"Bartocci, Ezio","last_name":"Bartocci"},{"last_name":"Bonakdarpour","first_name":"Borzoo","full_name":"Bonakdarpour, Borzoo"}],"abstract":[{"lang":"eng","text":"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 hyperproperties– a powerful formalism for expressing and reasoning about a wide range of information-flow security policies. We study black- vs. gray- vs. white-box 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."}],"project":[{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy","grant_number":"F8502"}],"intvolume":"        62","acknowledgement":"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), National Science Foundation (NSF) CPS Award 1837680, NSF award ECCS-2144416 and NSF SaTC Award 2245114. Open access funding provided by Institute of Science and Technology (IST Austria).","day":"01","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","file_date_updated":"2025-09-02T05:53:47Z","issue":"3","date_created":"2025-08-17T22:01:36Z","isi":1,"article_number":"30","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"article_type":"original","publication_status":"published","publication":"Acta Informatica","quality_controlled":"1","citation":{"ama":"Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. Gray-box runtime enforcement of hyperproperties. <i>Acta Informatica</i>. 2025;62(3). doi:<a href=\"https://doi.org/10.1007/s00236-025-00502-1\">10.1007/s00236-025-00502-1</a>","short":"T.H. Hsu, A.A. Oliveira da Costa, A. Wintenberg, E. Bartocci, B. Bonakdarpour, Acta Informatica 62 (2025).","apa":"Hsu, T. H., Oliveira da Costa, A. A., Wintenberg, A., Bartocci, E., &#38; Bonakdarpour, B. (2025). Gray-box runtime enforcement of hyperproperties. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-025-00502-1\">https://doi.org/10.1007/s00236-025-00502-1</a>","mla":"Hsu, Tzu Han, et al. “Gray-Box Runtime Enforcement of Hyperproperties.” <i>Acta Informatica</i>, vol. 62, no. 3, 30, Springer Nature, 2025, doi:<a href=\"https://doi.org/10.1007/s00236-025-00502-1\">10.1007/s00236-025-00502-1</a>.","ieee":"T. H. Hsu, A. A. Oliveira da Costa, A. Wintenberg, E. Bartocci, and B. Bonakdarpour, “Gray-box runtime enforcement of hyperproperties,” <i>Acta Informatica</i>, vol. 62, no. 3. Springer Nature, 2025.","ista":"Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. 2025. Gray-box runtime enforcement of hyperproperties. Acta Informatica. 62(3), 30.","chicago":"Hsu, Tzu Han, Ana A Oliveira da Costa, Andrew Wintenberg, Ezio Bartocci, and Borzoo Bonakdarpour. “Gray-Box Runtime Enforcement of Hyperproperties.” <i>Acta Informatica</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s00236-025-00502-1\">https://doi.org/10.1007/s00236-025-00502-1</a>."},"corr_author":"1","year":"2025","article_processing_charge":"Yes (via OA deal)","doi":"10.1007/s00236-025-00502-1","file":[{"creator":"dernst","success":1,"file_size":6505049,"file_id":"20267","content_type":"application/pdf","checksum":"90a43350fd4a8c5cb5b1b0e1aea7970d","file_name":"2025_ActaInformatica_Hsu.pdf","date_created":"2025-09-02T05:53:47Z","access_level":"open_access","date_updated":"2025-09-02T05:53:47Z","relation":"main_file"}],"ddc":["000"],"scopus_import":"1","oa_version":"Published Version","oa":1,"department":[{"_id":"ToHe"}],"OA_place":"publisher","publication_identifier":{"issn":["0001-5903"],"eissn":["1432-0525"]}},{"conference":{"location":"Pilani, India","start_date":"2025-12-17","end_date":"2025-12-19","name":"FSTTCS: Conference on Foundations of Software Technology and Theoretical Computer Science"},"doi":"10.4230/LIPICS.FSTTCS.2025.20","year":"2025","page":"20:1-20:18","article_processing_charge":"No","oa_version":"Published Version","oa":1,"department":[{"_id":"ToHe"}],"OA_place":"publisher","file":[{"content_type":"application/pdf","file_size":933970,"file_id":"21213","success":1,"creator":"dernst","checksum":"8188ee5c7b14193d48eeb655e9bbdc47","access_level":"open_access","date_created":"2026-02-11T09:33:20Z","file_name":"2025_LIPIcS_Chalupa.pdf","relation":"main_file","date_updated":"2026-02-11T09:33:20Z"}],"ddc":["000"],"ec_funded":1,"scopus_import":"1","date_created":"2026-01-29T15:39:15Z","publication":"45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science","quality_controlled":"1","citation":{"chicago":"Chalupa, Marek, Thomas A Henzinger, and Ana A Oliveira da Costa. “Flavors of Quantifiers in Hyperlogics.” In <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, 360:20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. <a href=\"https://doi.org/10.4230/LIPICS.FSTTCS.2025.20\">https://doi.org/10.4230/LIPICS.FSTTCS.2025.20</a>.","ieee":"M. Chalupa, T. A. Henzinger, and A. A. Oliveira da Costa, “Flavors of quantifiers in hyperlogics,” in <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Pilani, India, 2025, vol. 360, p. 20:1-20:18.","ista":"Chalupa M, Henzinger TA, Oliveira da Costa AA. 2025. Flavors of quantifiers in hyperlogics. 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS: Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 360, 20:1-20:18.","mla":"Chalupa, Marek, et al. “Flavors of Quantifiers in Hyperlogics.” <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, vol. 360, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 20:1-20:18, doi:<a href=\"https://doi.org/10.4230/LIPICS.FSTTCS.2025.20\">10.4230/LIPICS.FSTTCS.2025.20</a>.","short":"M. Chalupa, T.A. Henzinger, A.A. Oliveira da Costa, in:, 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 20:1-20:18.","apa":"Chalupa, M., Henzinger, T. A., &#38; Oliveira da Costa, A. A. (2025). Flavors of quantifiers in hyperlogics. In <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i> (Vol. 360, p. 20:1-20:18). Pilani, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.FSTTCS.2025.20\">https://doi.org/10.4230/LIPICS.FSTTCS.2025.20</a>","ama":"Chalupa M, Henzinger TA, Oliveira da Costa AA. Flavors of quantifiers in hyperlogics. In: <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>. Vol 360. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025:20:1-20:18. doi:<a href=\"https://doi.org/10.4230/LIPICS.FSTTCS.2025.20\">10.4230/LIPICS.FSTTCS.2025.20</a>"},"corr_author":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"publication_status":"published","arxiv":1,"language":[{"iso":"eng"}],"has_accepted_license":"1","OA_type":"gold","status":"public","external_id":{"arxiv":["2510.12298"]},"type":"conference","author":[{"last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek","first_name":"Marek"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger"},{"full_name":"Oliveira da Costa, Ana A","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","first_name":"Ana A","last_name":"Oliveira da Costa"}],"date_updated":"2026-02-11T09:35:04Z","day":"09","file_date_updated":"2026-02-11T09:33:20Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"Hypertrace logic is a sorted first-order logic with separate sorts for time and execution traces. Its formulas specify hyperproperties, which are properties relating multiple traces. In this work, we extend hypertrace logic by introducing trace quantifiers that range over the set of all possible traces. In this extended logic, formulas can quantify over two kinds of trace variables: constrained trace variables, which range over a fixed set of traces defined by the model, and unconstrained trace variables, which can be assigned to any trace. In comparison, hyperlogics such as HyperLTL have only constrained trace quantifiers. We use hypertrace logic to study how different quantifier patterns affect the decidability of the satisfiability problem. We prove that hypertrace logic without constrained trace quantifiers is equivalent to monadic second-order logic of one successor (S1S), and therefore satisfiable, and that the trace-prefixed fragment (all trace quantifiers precede all time quantifiers) is equivalent to HyperQPTL. Moreover, we show that all hypertrace formulas where the only alternation between constrained trace quantifiers is from an existential to a universal quantifier are equisatisfiable to formulas without constraints on their trace variables and, therefore, decidable as well. Our framework allows us to study also time-prefixed hyperlogics, for which we provide new decidability and undecidability results.","lang":"eng"}],"intvolume":"       360","project":[{"name":"Interface Theory for Security and Privacy","grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"},{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"acknowledgement":"This work was supported in part by the Austrian Science Fund (FWF) SFB project SpyCoDe 10.55776/F85 and by the ERC Advanced Grant VAMOS 101020093.","volume":360,"date_published":"2025-12-09T00:00:00Z","_id":"21089","title":"Flavors of quantifiers in hyperlogics","alternative_title":["LIPIcs"],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","month":"12"},{"day":"13","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"We propose a monitoring approach for hyperproperties where the system’s observations range over infinite domains. The specifications are given as formulas of symbolic hypernode logic, an extension of earlier versions of hypernode logic that supports events with data. We demonstrate how to translate terms of symbolic hypernode logic into multi-tape symbolic transducers and we present a monitoring algorithm for universally quantified formulas that is based on this translation. We evaluate our approach against the previous approach for monitoring hypernode logic, and we also compare it to other monitors for hyperproperties."}],"intvolume":"     16087","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"},{"grant_number":"F8502","name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"}],"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 and in part by the FWF-2022-SFB F8502 (SPyCoDe).","language":[{"iso":"eng"}],"OA_type":"green","status":"public","type":"conference","external_id":{"arxiv":["2508.02301"]},"author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek","first_name":"Marek","last_name":"Chalupa"},{"orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Oliveira da Costa","first_name":"Ana A","full_name":"Oliveira da Costa, Ana A","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b"}],"date_updated":"2026-02-16T11:59:20Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2508.02301"}],"publisher":"Springer Nature","month":"09","date_published":"2025-09-13T00:00:00Z","volume":16087,"title":"Monitoring hypernode logic over infinite domains","_id":"21093","alternative_title":["LNCS"],"oa_version":"Preprint","oa":1,"department":[{"_id":"ToHe"}],"OA_place":"repository","publication_identifier":{"eissn":["1611-3349"],"eisbn":["9783032054357"],"issn":["0302-9743"]},"ec_funded":1,"conference":{"location":"Graz, Austria","start_date":"2025-09-15","name":"RV: Runtime Verification","end_date":"2025-09-19"},"doi":"10.1007/978-3-032-05435-7_23","year":"2025","page":"417-437","article_processing_charge":"No","publication":"25th International Conference on Runtime Verification","quality_controlled":"1","citation":{"chicago":"Chalupa, Marek, Thomas A Henzinger, and Ana A Oliveira da Costa. “Monitoring Hypernode Logic over Infinite Domains.” In <i>25th International Conference on Runtime Verification</i>, 16087:417–37. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">https://doi.org/10.1007/978-3-032-05435-7_23</a>.","ista":"Chalupa M, Henzinger TA, Oliveira da Costa AA. 2025. Monitoring hypernode logic over infinite domains. 25th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 16087, 417–437.","ieee":"M. Chalupa, T. A. Henzinger, and A. A. Oliveira da Costa, “Monitoring hypernode logic over infinite domains,” in <i>25th International Conference on Runtime Verification</i>, Graz, Austria, 2025, vol. 16087, pp. 417–437.","apa":"Chalupa, M., Henzinger, T. A., &#38; Oliveira da Costa, A. A. (2025). Monitoring hypernode logic over infinite domains. In <i>25th International Conference on Runtime Verification</i> (Vol. 16087, pp. 417–437). Graz, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">https://doi.org/10.1007/978-3-032-05435-7_23</a>","short":"M. Chalupa, T.A. Henzinger, A.A. Oliveira da Costa, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 417–437.","ama":"Chalupa M, Henzinger TA, Oliveira da Costa AA. Monitoring hypernode logic over infinite domains. In: <i>25th International Conference on Runtime Verification</i>. Vol 16087. Springer Nature; 2025:417-437. doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">10.1007/978-3-032-05435-7_23</a>","mla":"Chalupa, Marek, et al. “Monitoring Hypernode Logic over Infinite Domains.” <i>25th International Conference on Runtime Verification</i>, vol. 16087, Springer Nature, 2025, pp. 417–37, doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">10.1007/978-3-032-05435-7_23</a>."},"corr_author":"1","arxiv":1,"publication_status":"published","date_created":"2026-01-29T16:04:31Z"}]