Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification

Confidentiality is an important concern in today's information society: electronic payment and personal data should be protected appropriately. This holds in particular for multi-threaded applications, which are generally seen the future of high-performance computing. Multi-threading poses new challenges to data protection, in particular, data races may be exploited in security attacks. Also, the role of the scheduler is seminal in the multi-threaded context. This paper proposes a new notion of confidentiality for probabilistic and non-probabilistic multi-threaded programs, formalized as scheduler-specific probabilistic observational determinism (SSPOD), together with verification methods. Essentially, SSPOD ensures that no information about the private data can be derived either from the public data, or from the probabilities of the public data being changed. Moreover, SSPOD explicitly depends on a given (class of) schedulers. Formally, this is expressed by using two conditions: (i) each publicly visible variable individually behaves deterministically with probability $1$, and (ii) for every trace considering all publicly visible variables, there always exists a matching trace with equal probability. We verify these conditions by a clever combination of new and existing algorithms over probabilistic Kripke structures.