Probabilistic noninterference in a concurrent language
Conference
Volpano, D, Smith, G. (1998). Probabilistic noninterference in a concurrent language
. Proceedings of the Computer Security Foundations Workshop, 34-43. 10.1109/CSFW.1998.683153
Volpano, D, Smith, G. (1998). Probabilistic noninterference in a concurrent language
. Proceedings of the Computer Security Foundations Workshop, 34-43. 10.1109/CSFW.1998.683153
In [15], we 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. We describe how they can be eliminated without making the type system more restrictive. We 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 [10]1.
