Technical Report: Probabilistic Noninterference Based on Program Dependence Graphs

We present a new algorithm for checking probabilistic noninterference in concurrent programs. The algorithm uses the Low-Security Observational Determinism criterion. It is based on program dependence graphs for concurrent programs, and is thus very precise: it is flow-sensitive, context-sensitive, object-sensitive, and optionally time-sensitive. The algorithm has been implemented for full Java bytecode with unlimited threads, and avoids restrictions or soundness leaks of previous approaches. A soundness proof is provided. Precision and scalability have been experimentally validated.