Scalable Precise Computation of Shannon Entropy

TL;DR

This paper introduces PSE, a scalable and precise tool for computing Shannon entropy in quantitative information flow analysis, leveraging a novel knowledge compilation language and optimized model counting.

Contribution

The paper presents a new knowledge compilation language, exttt{ADDAND}, and optimization techniques that significantly improve the scalability and precision of Shannon entropy computation in QIF.

Findings

PSE solved 56 more benchmarks than EntropyEstimation.

PSE is at least 10 times more efficient on 98% of common benchmarks.

PSE demonstrates superior scalability and precision in entropy computation.

Abstract

Quantitative information flow analyses (QIF) are a class of techniques for measuring the amount of confidential information leaked by a program to its public outputs. Shannon entropy is an important method to quantify the amount of leakage in QIF. This paper focuses on the programs modeled in Boolean constraints and optimizes the two stages of the Shannon entropy computation to implement a scalable precise tool PSE. In the first stage, we design a knowledge compilation language called \ADDAND that combines Algebraic Decision Diagrams and conjunctive decomposition. \ADDAND avoids enumerating possible outputs of a program and supports tractable entropy computation. In the second stage, we optimize the model counting queries that are used to compute the probabilities of outputs. We compare PSE with the state-of-the-art probabilistic approximately correct tool EntropyEstimation, which was shown to significantly outperform the previous precise tools. The experimental results demonstrate that PSE solved 56 more benchmarks compared to EntropyEstimation in a total of 459. For 98\% of the benchmarks that both PSE and EntropyEstimation solved, PSE is at least $10\times$ as efficient as EntropyEstimation.