---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '20186'
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.
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).
article_number: '30'
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Tzu Han
full_name: Hsu, Tzu Han
last_name: Hsu
- first_name: Ana A
full_name: Oliveira Da Costa, Ana A
id: 8b282559-50b0-11ef-861e-d6ace0d92e9b
last_name: Oliveira Da Costa
- first_name: Andrew
full_name: Wintenberg, Andrew
last_name: Wintenberg
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Borzoo
full_name: Bonakdarpour, Borzoo
last_name: Bonakdarpour
citation:
ama: Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. Gray-box
runtime enforcement of hyperproperties. Acta Informatica. 2025;62(3). doi:10.1007/s00236-025-00502-1
apa: Hsu, T. H., Oliveira da Costa, A. A., Wintenberg, A., Bartocci, E., & Bonakdarpour,
B. (2025). Gray-box runtime enforcement of hyperproperties. Acta Informatica.
Springer Nature. https://doi.org/10.1007/s00236-025-00502-1
chicago: Hsu, Tzu Han, Ana A Oliveira da Costa, Andrew Wintenberg, Ezio Bartocci,
and Borzoo Bonakdarpour. “Gray-Box Runtime Enforcement of Hyperproperties.” Acta
Informatica. Springer Nature, 2025. https://doi.org/10.1007/s00236-025-00502-1.
ieee: T. H. Hsu, A. A. Oliveira da Costa, A. Wintenberg, E. Bartocci, and B. Bonakdarpour,
“Gray-box runtime enforcement of hyperproperties,” Acta Informatica, 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.
mla: Hsu, Tzu Han, et al. “Gray-Box Runtime Enforcement of Hyperproperties.” Acta
Informatica, vol. 62, no. 3, 30, Springer Nature, 2025, doi:10.1007/s00236-025-00502-1.
short: T.H. Hsu, A.A. Oliveira da Costa, A. Wintenberg, E. Bartocci, B. Bonakdarpour,
Acta Informatica 62 (2025).
corr_author: '1'
date_created: 2025-08-17T22:01:36Z
date_published: 2025-09-01T00:00:00Z
date_updated: 2025-09-30T14:20:11Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s00236-025-00502-1
external_id:
isi:
- '001546115300001'
file:
- access_level: open_access
checksum: 90a43350fd4a8c5cb5b1b0e1aea7970d
content_type: application/pdf
creator: dernst
date_created: 2025-09-02T05:53:47Z
date_updated: 2025-09-02T05:53:47Z
file_id: '20267'
file_name: 2025_ActaInformatica_Hsu.pdf
file_size: 6505049
relation: main_file
success: 1
file_date_updated: 2025-09-02T05:53:47Z
has_accepted_license: '1'
intvolume: ' 62'
isi: 1
issue: '3'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
publication: Acta Informatica
publication_identifier:
eissn:
- 1432-0525
issn:
- 0001-5903
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Gray-box runtime enforcement of hyperproperties
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 62
year: '2025'
...
---
OA_place: publisher
OA_type: gold
_id: '21089'
abstract:
- lang: eng
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.'
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.
alternative_title:
- LIPIcs
article_processing_charge: No
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Ana A
full_name: Oliveira da Costa, Ana A
id: 8b282559-50b0-11ef-861e-d6ace0d92e9b
last_name: Oliveira da Costa
citation:
ama: 'Chalupa M, Henzinger TA, Oliveira da Costa AA. Flavors of quantifiers in hyperlogics.
In: 45th Annual Conference on Foundations of Software Technology and Theoretical
Computer Science. Vol 360. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2025:20:1-20:18. doi:10.4230/LIPICS.FSTTCS.2025.20'
apa: 'Chalupa, M., Henzinger, T. A., & Oliveira da Costa, A. A. (2025). Flavors
of quantifiers in hyperlogics. In 45th Annual Conference on Foundations of
Software Technology and Theoretical Computer Science (Vol. 360, p. 20:1-20:18).
Pilani, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.FSTTCS.2025.20'
chicago: Chalupa, Marek, Thomas A Henzinger, and Ana A Oliveira da Costa. “Flavors
of Quantifiers in Hyperlogics.” In 45th Annual Conference on Foundations of
Software Technology and Theoretical Computer Science, 360:20:1-20:18. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2025. https://doi.org/10.4230/LIPICS.FSTTCS.2025.20.
ieee: M. Chalupa, T. A. Henzinger, and A. A. Oliveira da Costa, “Flavors of quantifiers
in hyperlogics,” in 45th Annual Conference on Foundations of Software Technology
and Theoretical Computer Science, 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.” 45th Annual
Conference on Foundations of Software Technology and Theoretical Computer Science,
vol. 360, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 20:1-20:18,
doi:10.4230/LIPICS.FSTTCS.2025.20.
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.
conference:
end_date: 2025-12-19
location: Pilani, India
name: 'FSTTCS: Conference on Foundations of Software Technology and Theoretical
Computer Science'
start_date: 2025-12-17
corr_author: '1'
date_created: 2026-01-29T15:39:15Z
date_published: 2025-12-09T00:00:00Z
date_updated: 2026-02-11T09:35:04Z
day: '09'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPICS.FSTTCS.2025.20
ec_funded: 1
external_id:
arxiv:
- '2510.12298'
file:
- access_level: open_access
checksum: 8188ee5c7b14193d48eeb655e9bbdc47
content_type: application/pdf
creator: dernst
date_created: 2026-02-11T09:33:20Z
date_updated: 2026-02-11T09:33:20Z
file_id: '21213'
file_name: 2025_LIPIcS_Chalupa.pdf
file_size: 933970
relation: main_file
success: 1
file_date_updated: 2026-02-11T09:33:20Z
has_accepted_license: '1'
intvolume: ' 360'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: 20:1-20:18
project:
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 45th Annual Conference on Foundations of Software Technology and Theoretical
Computer Science
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Flavors of quantifiers in hyperlogics
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 360
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '21093'
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.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093 and
in part by the FWF-2022-SFB F8502 (SPyCoDe).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Ana A
full_name: Oliveira da Costa, Ana A
id: 8b282559-50b0-11ef-861e-d6ace0d92e9b
last_name: Oliveira da Costa
citation:
ama: 'Chalupa M, Henzinger TA, Oliveira da Costa AA. Monitoring hypernode logic
over infinite domains. In: 25th International Conference on Runtime Verification.
Vol 16087. Springer Nature; 2025:417-437. doi:10.1007/978-3-032-05435-7_23'
apa: 'Chalupa, M., Henzinger, T. A., & Oliveira da Costa, A. A. (2025). Monitoring
hypernode logic over infinite domains. In 25th International Conference on
Runtime Verification (Vol. 16087, pp. 417–437). Graz, Austria: Springer Nature.
https://doi.org/10.1007/978-3-032-05435-7_23'
chicago: Chalupa, Marek, Thomas A Henzinger, and Ana A Oliveira da Costa. “Monitoring
Hypernode Logic over Infinite Domains.” In 25th International Conference on
Runtime Verification, 16087:417–37. Springer Nature, 2025. https://doi.org/10.1007/978-3-032-05435-7_23.
ieee: M. Chalupa, T. A. Henzinger, and A. A. Oliveira da Costa, “Monitoring hypernode
logic over infinite domains,” in 25th International Conference on Runtime Verification,
Graz, Austria, 2025, vol. 16087, pp. 417–437.
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.'
mla: Chalupa, Marek, et al. “Monitoring Hypernode Logic over Infinite Domains.”
25th International Conference on Runtime Verification, vol. 16087, Springer
Nature, 2025, pp. 417–37, doi:10.1007/978-3-032-05435-7_23.
short: M. Chalupa, T.A. Henzinger, A.A. Oliveira da Costa, in:, 25th International
Conference on Runtime Verification, Springer Nature, 2025, pp. 417–437.
conference:
end_date: 2025-09-19
location: Graz, Austria
name: 'RV: Runtime Verification'
start_date: 2025-09-15
corr_author: '1'
date_created: 2026-01-29T16:04:31Z
date_published: 2025-09-13T00:00:00Z
date_updated: 2026-02-16T11:59:20Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-032-05435-7_23
ec_funded: 1
external_id:
arxiv:
- '2508.02301'
intvolume: ' 16087'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2508.02301
month: '09'
oa: 1
oa_version: Preprint
page: 417-437
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
publication: 25th International Conference on Runtime Verification
publication_identifier:
eisbn:
- '9783032054357'
eissn:
- 1611-3349
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Monitoring hypernode logic over infinite domains
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16087
year: '2025'
...