  Many types of attacks on confidentiality stem from the nondeterministic
nature of the environment that computer programs operate in (e.g., schedulers
and asynchronous communication channels). In this paper, we focus on
verification of confidentiality in nondeterministic environments by reasoning
about asynchronous hyperproperties. First, 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 the
generalized 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 for different fragments of A-HLTL.
