Probabilistic noninterference in a concurrent language
Article
Volpano, D, Smith, G. (1999). Probabilistic noninterference in a concurrent language
. Journal of Computer Security, 7(2), 231-253. 10.3233/JCS-1999-72-305
Volpano, D, Smith, G. (1999). Probabilistic noninterference in a concurrent language
. Journal of Computer Security, 7(2), 231-253. 10.3233/JCS-1999-72-305
In previous work (Smith and Volpano, Proceedings 25th Symposium on Principles of Programming Languages, San Diego, CA, 1998, pp. 355-364), 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 guard containing high variables executes atomically. The proof uses the notion of a probabilistic state of a computation from Kozen's work in the denotational semantics of probabilistic programs (Kozen, Journal of Computer and System Sciences 22 (1981), 328-350).
