Affiliations: [a] Computer Science Department, Naval Postgraduate School, Monterey, CA 93943, USA. E-mail: volpano@cs.nps.navy.mil | [b] School of Computer Science, Florida International University, Miami, FL 33199, USA. E-mail: smithg@cs.fiu.edu
Note: [1] This is an expanded version of a paper that appeared in the Proceedings of the 11th IEEE Computer Security Foundations Workshop, Rockport, MA, June 1998, pp. 34–43.
Abstract: 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).2This material is based upon activities supported by DARPA and by the National Science Foundation under Agreement Nos. CCR-9612176 and CCR-9612345.
