---
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. <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>
  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>
  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>.
  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.
  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>.
  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: hybrid
_id: '20866'
abstract:
- lang: eng
  text: In this work, we present hypernode automata as a specification formalism for
    hyperproperties of systems whose executions may be misaligned among themselves,
    such as concurrent systems. These automata consist of nodes labeled with hypernode
    logic formulas and transitions marked with synchronizing actions. Hypernode logic
    formulas establish relations between sequences of variable values among different
    system executions. This logic enables both synchronous and asynchronous analysis
    of traces. In its asynchronous view on execution traces, hypernode formulas establish
    relations on the order of value changes for each variable without correlating
    their timing. In both views, the analysis of different execution traces is synchronized
    through the transitions of hypernode automata. By combining logic’s declarative
    nature with automata’s procedural power, hypernode automata seamlessly integrate
    asynchronicity requirements at the node level with synchronicity between node
    transitions. We show that the model-checking problem for hypernode automata is
    decidable for specifications where each node specifies either a synchronous or
    an asynchronous requirement for the system’s executions, but not both.
acknowledgement: This work was supported in part by the Austrian Science Fund (FWF)
  SFB project SpyCoDe 10.55776/F85, by the FWF projects ZK-35 and W1255-N23, and by
  the ERC Advanced Grant VAMOS 101020093. Open access funding provided by Institute
  of Science and Technology (IST Austria).
article_number: '43'
article_processing_charge: Yes (via OA deal)
article_type: original
arxiv: 1
author:
- first_name: Ezio
  full_name: Bartocci, Ezio
  last_name: Bartocci
- 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: Dejan
  full_name: Nickovic, Dejan
  id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
  last_name: Nickovic
- first_name: Ana
  full_name: Oliveira da Costa, Ana
  id: f347ec37-6676-11ee-b395-a888cb7b4fb4
  last_name: Oliveira da Costa
  orcid: 0000-0002-8741-5799
citation:
  ama: Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode
    automata. <i>Acta Informatica</i>. 2025;62(4). doi:<a href="https://doi.org/10.1007/s00236-025-00509-8">10.1007/s00236-025-00509-8</a>
  apa: Bartocci, E., Chalupa, M., Henzinger, T. A., Nickovic, D., &#38; Oliveira da
    Costa, A. (2025). Hypernode automata. <i>Acta Informatica</i>. Springer Nature.
    <a href="https://doi.org/10.1007/s00236-025-00509-8">https://doi.org/10.1007/s00236-025-00509-8</a>
  chicago: Bartocci, Ezio, Marek Chalupa, Thomas A Henzinger, Dejan Nickovic, and
    Ana Oliveira da Costa. “Hypernode Automata.” <i>Acta Informatica</i>. Springer
    Nature, 2025. <a href="https://doi.org/10.1007/s00236-025-00509-8">https://doi.org/10.1007/s00236-025-00509-8</a>.
  ieee: E. Bartocci, M. Chalupa, T. A. Henzinger, D. Nickovic, and A. Oliveira da
    Costa, “Hypernode automata,” <i>Acta Informatica</i>, vol. 62, no. 4. Springer
    Nature, 2025.
  ista: Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025.
    Hypernode automata. Acta Informatica. 62(4), 43.
  mla: Bartocci, Ezio, et al. “Hypernode Automata.” <i>Acta Informatica</i>, vol.
    62, no. 4, 43, Springer Nature, 2025, doi:<a href="https://doi.org/10.1007/s00236-025-00509-8">10.1007/s00236-025-00509-8</a>.
  short: E. Bartocci, M. Chalupa, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa,
    Acta Informatica 62 (2025).
corr_author: '1'
date_created: 2025-12-29T12:07:12Z
date_published: 2025-12-09T00:00:00Z
date_updated: 2026-01-05T12:27:41Z
day: '09'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s00236-025-00509-8
ec_funded: 1
external_id:
  arxiv:
  - '2305.02836'
file:
- access_level: open_access
  checksum: 06ed45a1218ad8464818803ae2968aaf
  content_type: application/pdf
  creator: dernst
  date_created: 2026-01-05T12:26:43Z
  date_updated: 2026-01-05T12:26:43Z
  file_id: '20944'
  file_name: 2025_ActaInformatica_Bartocci.pdf
  file_size: 7117003
  relation: main_file
  success: 1
file_date_updated: 2026-01-05T12:26:43Z
has_accepted_license: '1'
intvolume: '        62'
issue: '4'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
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: Acta Informatica
publication_identifier:
  eissn:
  - 1432-0525
  issn:
  - 0001-5903
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
  record:
  - id: '14405'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Hypernode automata
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 62
year: '2025'
...
---
_id: '10602'
abstract:
- lang: eng
  text: Transforming ω-automata into parity automata is traditionally done using appearance
    records. We present an efficient variant of this idea, tailored to Rabin automata,
    and several optimizations applicable to all appearance records. We compare the
    methods experimentally and show that our method produces significantly smaller
    automata than previous approaches.
acknowledgement: This work is partially funded by the German Research Foundation (DFG)
  projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification
  (No. 383882557), and the Alexander von Humboldt Foundation with funds from the German
  Federal Ministry of Education and Research. It is an extended version of [21], including
  all proofs together with further explanations and examples. Moreover, we provide
  a new, more efficient construction based on (total) preorders, unifying previous
  optimizations. Experiments are performed with a new, performant implementation,
  comparing our approach to the current state of the art.
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
- first_name: Tobias
  full_name: Meggendorfer, Tobias
  id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
  last_name: Meggendorfer
  orcid: 0000-0002-1712-2165
- first_name: Clara
  full_name: Waldmann, Clara
  last_name: Waldmann
- first_name: Maximilian
  full_name: Weininger, Maximilian
  last_name: Weininger
citation:
  ama: Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record
    with preorders. <i>Acta Informatica</i>. 2022;59:585-618. doi:<a href="https://doi.org/10.1007/s00236-021-00412-y">10.1007/s00236-021-00412-y</a>
  apa: Kretinsky, J., Meggendorfer, T., Waldmann, C., &#38; Weininger, M. (2022).
    Index appearance record with preorders. <i>Acta Informatica</i>. Springer Nature.
    <a href="https://doi.org/10.1007/s00236-021-00412-y">https://doi.org/10.1007/s00236-021-00412-y</a>
  chicago: Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger.
    “Index Appearance Record with Preorders.” <i>Acta Informatica</i>. Springer Nature,
    2022. <a href="https://doi.org/10.1007/s00236-021-00412-y">https://doi.org/10.1007/s00236-021-00412-y</a>.
  ieee: J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance
    record with preorders,” <i>Acta Informatica</i>, vol. 59. Springer Nature, pp.
    585–618, 2022.
  ista: Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance
    record with preorders. Acta Informatica. 59, 585–618.
  mla: Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” <i>Acta Informatica</i>,
    vol. 59, Springer Nature, 2022, pp. 585–618, doi:<a href="https://doi.org/10.1007/s00236-021-00412-y">10.1007/s00236-021-00412-y</a>.
  short: J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica
    59 (2022) 585–618.
corr_author: '1'
date_created: 2022-01-06T12:37:27Z
date_published: 2022-10-01T00:00:00Z
date_updated: 2025-04-15T06:53:08Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/s00236-021-00412-y
external_id:
  isi:
  - '000735765500001'
file:
- access_level: open_access
  checksum: bf1c195b6aaf59e8530cf9e3a9d731f7
  content_type: application/pdf
  creator: cchlebak
  date_created: 2022-01-07T07:50:31Z
  date_updated: 2022-01-07T07:50:31Z
  file_id: '10603'
  file_name: 2021_ActaInfor_Křetínský.pdf
  file_size: 1066082
  relation: main_file
  success: 1
file_date_updated: 2022-01-07T07:50:31Z
has_accepted_license: '1'
intvolume: '        59'
isi: 1
keyword:
- computer networks and communications
- information systems
- software
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 585-618
project:
- _id: B67AFEDC-15C9-11EA-A837-991A96BB2854
  name: IST Austria Open Access Fund
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: Index appearance record with preorders
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 59
year: '2022'
...