提出可扩展的精确香农熵计算工具PSE，提升程序信息泄露分析效率。
Scalable Precise Computation of Shannon Entropy
- 设计新型知识编译语言ADDAND，避免枚举输出并支持高效熵计算
- 在459个基准中比现有工具多解决56个，98%的相同任务快10倍以上
- 适合需要精确分析程序信息泄露的密码学与安全研究者
定量信息流分析（QIF）是一类用于衡量程序向公开输出泄露机密信息量的技术。香农熵是QIF中量化泄漏量的重要方法。本文聚焦于以布尔约束建模的程序，优化香农熵计算的两个阶段，实现可扩展的精确工具PSE。第一阶段设计了一种名为ADDAND的知识编译语言，结合代数决策图与合取分解，避免枚举程序可能的输出，并支持可处理的熵计算。第二阶段优化了用于计算输出概率的模型计数查询。将PSE与最先进的概率近似正确工具EntropyEstimation对比，后者已被证明显著优于之前的精确工具。实验结果表明，在总共459个基准中，PSE比EntropyEstimation多解决了56个；对于两者均能解决的98%基准，PSE效率至少高出10倍。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。