Quantifying Information Flow in Programs Using Program Logics
The authors have explained a precise quantitative information flow analysis can be built on top of a direct formalization of indistinguishability in Dynamic Logic. They have used three publicly available tools for this: the KeY system v1.6, the Z3 SMT solver v2.10, and the Barvinok tool v0.35. According to the running times reported in, the KeY-based analysis was several times faster than model checking. Furthermore, the use of a deductive verification foundation and improved model counting technology allowed one to extend analysis scope. The technique they presented is, to their knowledge, the only termination-sensitive quantitative analysis, as well as the only precise analysis for programs with unbounded loops or a large number of possible outputs.