other · CISPA Helmholtz Center · 2023

Bounded Model Checking for Asynchronous Hyperproperties

Hsu, Tzu-Han, Bonakdarpour, Borzoo, Finkbeiner, Bernd, Sánchez, César

Cited by 0Open access

Abstract

Many types of attacks on confidentiality stem from the nondeterministic nature of the environment that computer programs operate in. We focus on verification of confidentiality in nondeterministic environments by reasoning about asynchronous hyperproperties. We generalize the temporal logic A-HLTL to allow nested trajectory quantification, where a trajectory determines how different execution traces may advance and stutter. We propose a bounded model checking algorithm for A-HLTL based on QBF-solving for a fragment of A-HLTL and evaluate it by various case studies on concurrent programs, scheduling attacks, compiler optimization, speculative execution, and cache timing attacks. We also rigorously analyze the complexity of model checking A-HLTL.

Cite this paper

APA 7

Hsu, T.-H., Bonakdarpour, B., Finkbeiner, B., & Sánchez, C. (2023). Bounded Model Checking for Asynchronous Hyperproperties. CISPA Helmholtz Center. https://doi.org/10.60882/cispa.25471216

MLA 9

Hsu, Tzu-Han, et al. “Bounded Model Checking for Asynchronous Hyperproperties.” CISPA Helmholtz Center, 2023, https://doi.org/10.60882/cispa.25471216.

Chicago

Hsu, Tzu-Han, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez. 2023. “Bounded Model Checking for Asynchronous Hyperproperties.” CISPA Helmholtz Center. https://doi.org/10.60882/cispa.25471216.

Harvard

Hsu, T.-H. et al. (2023) ‘Bounded Model Checking for Asynchronous Hyperproperties’, CISPA Helmholtz Center. Available at: https://doi.org/10.60882/cispa.25471216.

BibTeX

@misc{hsu2023bounded,
  title = {{Bounded Model Checking for Asynchronous Hyperproperties}},
  author = {Hsu, Tzu-Han and Bonakdarpour, Borzoo and Finkbeiner, Bernd and Sánchez, César},
  journal = {CISPA Helmholtz Center},
  year = {2023},
  doi = {10.60882/cispa.25471216}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.