
For FullText PDF, please login, if you are a member of IEICE,
or go to Pay Per View on menu list, if you are a nonmember of IEICE.

Quantifying Dynamic Leakage  Complexity Analysis and Model Countingbased Calculation 
Bao Trung CHU Kenji HASHIMOTO Hiroyuki SEKI
Publication
IEICE TRANSACTIONS on Information and Systems
Vol.E102D
No.10
pp.19521965 Publication Date: 2019/10/01 Publicized: 2019/07/11 Online ISSN: 17451361
DOI: 10.1587/transinf.2019EDP7132 Type of Manuscript: PAPER Category: Software System Keyword: quantitative information flow, hybrid monitor, dynamic leakage,
Full Text: FreePDF(456.4KB)
Summary:
A program is noninterferent if it leaks no secret information to an observable output. However, noninterference is too strict in many practical cases and quantitative information flow (QIF) has been proposed and studied in depth. Originally, QIF is defined as the average of leakage amount of secret information over all executions of a program. However, a vulnerable program that has executions leaking the whole secret but has the small average leakage could be considered as secure. This counterintuition raises a need for a new definition of information leakage of a particular run, i.e., dynamic leakage. As discussed in [5], entropybased definitions do not work well for quantifying information leakage dynamically; Beliefbased definition on the other hand is appropriate for deterministic programs, however, it is not appropriate for probabilistic ones. In this paper, we propose new simple notions of dynamic leakage based on entropy which are compatible with existing QIF definitions for deterministic programs, and yet reasonable for probabilistic programs in the sense of [5]. We also investigated the complexity of computing the proposed dynamic leakage for three classes of Boolean programs. We also implemented a tool for QIF calculation using model counting tools for Boolean formulae. Experimental results on popular benchmarks of QIF research show the flexibility of our framework. Finally, we discuss the improvement of performance and scalability of the proposed method as well as an extension to more general cases.

