arXiv:2502.01160v1 宣告类型: 新 摘要: 量化信息流分析（QIF）是一类用于测量程序泄露给其公共输出的机密信息量的技术。香农熵是一种重要的方法，用于量化QIF中的泄露量。本文关注的是用布尔约束模型化的程序，并优化了香农熵计算的两个阶段，以实现一个可扩展的精确工具PSE。在第一阶段，我们设计了一种称为\ADDAND的知识编译语言，该语言结合了代数决策图和合取分解。\ADDAND避免枚举程序的可能输出，并支持可处理的熵计算。在第二阶段，我们优化了用于计算输出概率的模型计数查询。我们将PSE与现有的最先进很可能近似工具EntropyEstimation进行了比较，EntropyEstimation被证明在现有的精确工具中表现显著更优。实验结果表明，在总共441个基准测试中，PSE比EntropyEstimation多解决了55个基准测试。对于PSE和EntropyEstimation都能解决的98%的基准测试，PSE至少比EntropyEstimation快10倍。