Bounded Model Checking for Asynchronous Hyperproperties

Abstract

Many types of attacks on confidentiality stem from the non-deterministic 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 ad- vance 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.