Secure Information Flow for Concurrent Processes

Information flow security is that aspect of computer security concerned with how confidential information is allowed to flow through a computer system. This is especially subtle when considering processes that are executed concurrently. We consider the notion of Probabilistic Noninterference (PNI) proposed in the literature to ensure secure information flow in concurrent processes. In the setting of a model of probabilistic dataflow, we provide a number of important results towards simplified verification that suggest relevance in the interaction of probabilistic processes outside this particular framework:PNI is shown to be compositional by casting it into a rely-guarantee framework, where the proof yields a more general Inductive Compositionality Principle. We deliver a considerably simplified criterion equivalent to PNI by “factoring out” the probabilistic behaviour of the environment. We show that the simpler nonprobabilistic notion of Nondeducibility-on-Strategies proposed in the literature is an instantiation of PNI, allowing us to extend our results to it.