A Probabilistic Justification of the Combining Calculus under the Uniform
Scheduler Assumption
Tina Kraußer, Heiko Mantel, and Henning Sudbrock
The combining calculus provides a framework for analyzing the information
flow of multi-threaded programs. The calculus incorporates so called
plug-in rules for integrating several previously existing analysis
techniques. By applying a plug-in rule to a subprogram, one decides
to analyze this subprogram with the given analysis technique, and not
with the rules of the combining calculus. The novelty of the combining
calculus was that one can analyze the information flow security of a
given program by using multiple analysis techniques in combination. It
was demonstrated that this flexibility leads to a more precise analysis,
allowing one to successfully verify the security of some programs
that cannot be verified with any of the existing analysis techniques
in isolation.
In MSK07, the soundness of the combining calculus is proved for a
possibilistic characterization of information flow security. This
characterization assumes a purely nondeterministic scheduling of
concurrent threads. In this report, we demonstrate that the combining
calculus is also sound for a probabilistic characterization of security
that assumes a uniform scheduler. This result further increases the
confidence in the combining calculus as a reliable and flexible tool
for formally analyzing the information flow security of multi-threaded
programs.