Probabilistic noninterference in a concurrent language
- 27 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 7, 34-43
- https://doi.org/10.1109/csfw.1998.683153
Abstract
The authors previously give a type system that guarantees that well-typed multi-threaded programs are possibilistically noninterfering. If thread scheduling is probabilistic, however, then well-typed programs may have probabilistic timing channels. They describe how they can be eliminated without making the type system more restrictive. They show that well-typed concurrent programs are probabilistically noninterfering if every total command with a high guard executes atomically. The proof uses the concept of a probabilistic state of a computation, following the work of Kozen (1981).Keywords
This publication has 14 references indexed in Scilit:
- Protection against covert storage and timing channelsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Eliminating covert flows with minimum typingsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Secure information flow in a multi-threaded imperative languagePublished by Association for Computing Machinery (ACM) ,1998
- The Compositional Security Checker: a tool for the verification of information flow security propertiesIEEE Transactions on Software Engineering, 1997
- A sound type system for secure flow analysisJournal of Computer Security, 1996
- A Classification of Security Properties for Process Algebras1Journal of Computer Security, 1995
- Security models and information flowPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1990
- Probabilistic interferencePublished by Institute of Electrical and Electronics Engineers (IEEE) ,1990
- Information flow in nondeterministic systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1990
- Semantics of probabilistic programsJournal of Computer and System Sciences, 1981