Confidentiality for multithreaded programs via bisimulation

Bisimulation has been a popular foundation for characterizing the confidentiality properties of concurrent programs. However, because a variety of bisimulation definitions are available in the literature, it is often difficult to pin down the "right" definition for modeling a particular attacker. Focusing on timing- and probability-sensitive confidentiality for shared-memory multithreaded programs, we clarify the relation between different kinds of bisimulation by proving inclusion results. As a consequence, we derive the relationship between scheduler-specific, scheduler-independent, and strong confidentiality definitions. A key result justifying strong confidentiality is that it is the most accurate (largest) compositional indistinguishability-based confidentiality property that implies scheduler-independent confidentiality.