Nov 15, 2011: Minh Tri Ngo: Confidentiality for Multi-Threaded Programs under Probabilistic Schedulers

November 15, 2011Confidentiality for Multi-Threaded Programs under Probabilistic Schedulers
Room: Zi 5126Minh Tri Ngo

A common way to ensure confidentiality for multi-threaded programs is to require that the executions are deterministic in the public variables. In recent work, we have characterized this property as scheduler-specific observational determinism. In contrast to earlier work, this property explicitly considers a (possibilistic) scheduler and the executions that are enabled by this scheduler.

This paper extends this definition of observational determinism to consider also probabilistic schedulers. This leads to an extra condition in the formal definition, ensuring that no information about private data can be derived from the probabilities of a publicly visible variable being changed. We compare our definition with earlier confidentiality properties considering probabilities, and argue that it expresses confidentiality better.

Finally, we show how our definition can be verified algorithmically. We develop two algorithms: the first algorithm verifies stuttering equivalence of all public program traces, the second algorithm checks for stuttering equivalence between probabilistic languages. Since these problems are important concepts, the algorithms are also of interest in a broad context.