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.

翻译：定量信息流分析是一类用于测量程序通过其公开输出泄露的机密信息量的技术。香农熵是量化QIF中泄露量的重要方法。本文聚焦于布尔约束建模的程序，并优化香农熵计算的两个阶段以实现可扩展的精确工具PSE。在第一阶段，我们设计了一种名为\ADDAND的知识编译语言，它结合了代数决策图与合取分解。\ADDAND避免了枚举程序的可能输出，并支持可处理的熵计算。在第二阶段，我们优化了用于计算输出概率的模型计数查询。我们将PSE与最先进的概率近似正确工具EntropyEstimation进行比较，后者已被证明显著优于以往的精确工具。实验结果表明，在总计459个基准测试中，PSE比EntropyEstimation多解决了56个。对于PSE和EntropyEstimation均解决的98%基准测试，PSE的效率至少是EntropyEstimation的$10\times$。