Konferenzartikel: Upper Bound Computation of Information Leakages for Unbounded Recursion

Confidentiality is an important security goal that is ensured by the absence of information flow between secrets and observable outputs. Quantitative information flow (QIF) analyses quantify the amount of knowledge an attacker can gain on the secrets by observing the outputs. This paper presents a novel approach for calculating an upper bound for the leakage of confidential information in a program regarding min-entropy. The approach uses a data flow analysis that represents dependencies between program variables as a bit dependency graph. The bit dependency graph is interpreted as a flow network and used to compute an upper bound for the leakage using a maximum flow computation. We introduce two novelties to improve the precision and soundness: We strengthen the precision of the data flow representation by using the path conditions. We add sound support of unbounded loops and recursion by using summary graphs, an extension of a common technique from compiler engineering. Our approach computes a valid upper bound of the leakage for all programs regardless of the number of loop iterations and recursion depth. We evaluate our tool against a state-of-the-art analysis on 13 example programs.