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 Composition-ality 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. © Springer-Verlag Berlin Heidelberg 2000.
CITATION STYLE
Jürjens, J. (2000). Secure information flow for concurrent processes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1877 LNCS, pp. 395–409). Springer Verlag. https://doi.org/10.1007/3-540-44618-4_29
Mendeley helps you to discover research relevant for your work.