Bounded Model Checking for Asynchronous Hyperproperties

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 logi... View More