Abstract
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.
Supported by the Studienstiftung des deutschen Volkes and the Division of Informatics.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
S. Abramsky. A note on reactive refinement, 1999. Manuscript.
Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, and Moshe Vardi. Alternating refinement relations. In CONCUR’98, volume 1466 of Lecture Notes in Computer Science, pages 163–178. Springer Verlag, 1998.
M. Abadi and Leslie Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems 15, 1:73–132, January 1993.
M. Abadi and P. Rogaway. Reconciling two views of cryptography (invited lecture). In TCS 2000, August 2000.
dAKN+00._L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, and R. Segala. Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation. In TACAS’2000, Lecture Notes in Computer Science, January 2000.
J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panagaden. Metrics for labeled markov systems. In CONCUR, 1999.
Bruno Dutertre and Victoria Stavridou. A model of noninterference for integrating mixed-criticality software components. In DCCA-7, Seventh IFIP International Working Conference on Dependable Computing for Critical Applications, San Jose, CA, January 1999.
B. Dutertre. State of the art in secure noninterference, 1999. Manuscript.
R. Focardi and R. Gorrieri. A classification of security properties for process algebra. J. Computer Security, 3(1):5–33, 1994.
R. Focardi and R. Gorrieri. The compositional security checker: A tool for the verification of information flow security properties. IEEE Transaction of Software Engineering, 23(9), September 1997.
R. Focardi. Comparing two information flow security properties. In Proceeding of the 9th IEEE Computer Security Foundation Workshop, pages 116–122, June 1996.
J. Goguen and J. Meseguer. Security policies and security models. In Proceedings of the 1982 Symposium on Security and Privacy, pages 11–20. IEEE Computer Society, 1982.
J. W. Gray. Toward A Mathematical Foundation for Information Flow Security. Journal of Computer Security, 3–4(1):255–294, 1992.
B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, Department of Computer Systems, Uppsala University, 1987. Tech. Rep. DoCS 87/09.
J. Jürjens. Verification of probabilistic secure information flow, 2000. submitted.
Gavin Lowe. Defining information flow. Technical report, Department of Mathematics and Computer Science Technical Report 1999/3, University of Leicester, 1999.
J. McLean. Security Models and Information Flow. In Proceedings of the IEEE Symposium on Research in Security and Privacy, pages 180–187, Oakland, CA, May 1990.
J. McLean. Security models. In John Marciniak, editor, Encyclopedia of Software Engineering. Wiley & Sons, Inc., 1994.
John D. McLean. A general theory of composition for a class of ”possibilistic” properties. IEEE Transactions on Software Engineering, 22(1):53–67, January 1996.
A. Roscoe and M. Goldsmith. What is intransitive noninterference? In Proceedings of the Computer Security Foundations Workshop of the IEEE Computer Society (CSFW), 1999.
A.W. Roscoe. CSP and determinism in security modelling. In Proceedings of the 1995 IEEE Symposium on Security and Privacy, 1995.
P. Ryan and S. Schneider. Process algebra and non-interference. In Proceedings of the 12 th Computer Security Foundations Workshop of the IEEE Computer Society (CSFW 12), 1999.
A. Roscoe, J. Woodcock, and L. Wulf. Non-interference through determinism. In ESORICS, 1994.
C. Shannon. Channels with side information at the transmitter. IBM Journal of Research and Development, 2:289–293, 1958.
J. T. Wittbold and D. M. Johnson. Information Flow in Nondeterministic Systems. In Proceedings of the IEEE Symposium on Research in Security and Privacy, pages 144–161, Oakland, CA, May 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jürjens, J. (2000). Secure Information Flow for Concurrent Processes. In: Palamidessi, C. (eds) CONCUR 2000 — Concurrency Theory. CONCUR 2000. Lecture Notes in Computer Science, vol 1877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44618-4_29
Download citation
DOI: https://doi.org/10.1007/3-540-44618-4_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67897-7
Online ISBN: 978-3-540-44618-7
eBook Packages: Springer Book Archive