CISPA
Browse

Bounded Model Checking for Asynchronous Hyperproperties

Download (693.42 kB)
conference contribution
posted on 2024-03-25, 12:54 authored by Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd FinkbeinerBernd Finkbeiner, César Sánchez
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.

History

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Tools and Algorithms for Construction and Analysis of Systems (TACAS)

Journal

CoRR

Volume

13993

Page Range

29-46

Publisher

Springer Nature

Open Access Type

  • Hybrid

BibTeX

@inproceedings{Hsu:Bonakdarpour:Finkbeiner:Sánchez:2023, title = "Bounded Model Checking for Asynchronous Hyperproperties", author = "Hsu, Tzu-Han" AND "Bonakdarpour, Borzoo" AND "Finkbeiner, Bernd" AND "Sánchez, César", year = 2023, month = 4, journal = "CoRR", pages = "29--46", publisher = "Springer Nature", issn = "1611-3349", doi = "10.1007/978-3-031-30823-9_2" }