一句话：提出可靠（sound）的符号定量信息流分析，在路径探索不全与模型计数不精确时仍能给出信息泄露的上界与下界。
信息泄露是现代软件系统中的重要问题，近年来常以 Shannon 熵等信息论概念量化程序的信息泄露。已有方法将符号执行与模型计数约束求解器结合来量化泄露，但存在两类不可靠来源：符号执行可能无法探索所有执行路径；模型计数求解器也可能无法给出精确计数。本文提出一种可靠的符号定量信息流分析，在程序行为未被完全探索、以及模型计数求解器只能给出模型计数上界与下界的情况下，仍能为信息泄露计算可靠边界。作者将该方法实现为 KLEE 的扩展，用于对 C 程序计算可靠的信息泄露边界。
Information leaks are a significant problem in modern software systems. In recent years, information theoretic concepts, such as Shannon entropy, have been applied to quantifying information leaks in programs. One recent approach is to use symbolic execution together with model counting constraints solvers in order to quantify information leakage. There are at least two reasons for unsoundness in quantifying information leakage using this approach: 1) Symbolic execution may not be able to explore all execution paths, 2) Model counting constraints solvers may not be able to provide an exact count. We present a sound symbolic quantitative information flow analysis that bounds the information leakage both for the cases where the program behavior is not fully explored and the model counting constraint solver is unable to provide a precise model count but provides an upper and a lower bound. We implemented our approach as an extension to KLEE for computing sound bounds for information leakage in C programs.
@article{paperbot2003,
title = {Obtaining Information Leakage Bounds via Approximate Model Counting},
author = {Seemanta Saha and Surendra Ghentiyala and Shihua Lu and Lucas Bang and Tevfik Bultan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591281}
}