Probabilistic Noninterference Based on Program Dependence Graphs
Dennis Giffhorn, Gregor Snelting · Repository KITopen (Karlsruhe Institute of Technology) · 2012
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 flowsensitive, 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.