Probabilistic noninterference for multi-threaded programs
- 7 November 2002
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 1109, 200-214
- https://doi.org/10.1109/csfw.2000.856937
Abstract
We present a probability-sensitive confidentiality specification -- a form of probabilistic noninterference -- for a small multi-threaded programming language with dynamic thread creation. Probabilistic covert channels arise from a scheduler, which is probabilistic. Since scheduling policy is typically outside the language specification for multi-threaded languages, we describe how to generalize the security condition in order to define robust security with respect to a wide class of schedulers, not excluding the possibility of deterministic (e.g., round-robin) schedulers and program-controlled thread priorities. The formulation is based on an adaptation of Larsen and Skou's notion of probabilistic bisimulation. We show how the security condition satisfies compositionality properties, which facilitate straightforward proofs of correctness for, e.g., security type systems. We illustrate this by defining a security type system, which improves on previous multi-threaded systems, and by proving it correct with respect to our stronger scheduler-independent security condition.Keywords
This publication has 16 references indexed in Scilit:
- Probabilistic noninterference in a concurrent languagePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Domain equations for probabilistic processesMathematical Structures in Computer Science, 2000
- Transforming out timing leaksPublished by Association for Computing Machinery (ACM) ,2000
- Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other SystemsPublished by Springer Nature ,1996
- A Classification of Security Properties for Process Algebras1Journal of Computer Security, 1995
- Bisimulation through probabilistic testingInformation and Computation, 1991
- Security Policies and Security ModelsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1982
- An Axiomatic Approach to Information Flow in ProgramsACM Transactions on Programming Languages and Systems, 1980
- Certification of programs for secure information flowCommunications of the ACM, 1977
- A lattice model of secure information flowCommunications of the ACM, 1976