  Quantitative information flow (QIF) is traditionally defined as the expected
value of information leakage over all feasible program runs and it fails to
identify vulnerable programs where only limited number of runs leak large
amount of information. As discussed in Bielova (2016), a good notion for
dynamic leakage and an efficient way of computing the leakage are needed. To
address this problem, the authors have already proposed two notions for dynamic
leakage and a method of quantifying dynamic leakage based on model counting.
Inspired by the work of Kawamoto et. al. (2017), this paper proposes two
efficient methods for computing dynamic leakage, a compositional method along
with the sequential structure of a program and a parallel computation based on
the value domain decomposition. For the former, we also investigate both exact
and approximated calculations. From the perspective of implementation, we
utilize binary decision diagrams (BDDs) and deterministic decomposable negation
normal forms (d-DNNFs) to represent Boolean formulas in model counting.
Finally, we show experimental results on several examples.
