一句话：提出定量鲁棒可达性与定量鲁棒符号执行（QRSE），自动度量触发漏洞的难度。
多数软件分析技术只关注缺陷是否可达，但这对安全评估并不理想，因为没有考虑触发缺陷的难度。新近提出的鲁棒可达性（robust reachability）概念通过区分“可以独立于不可控输入被触发”与“不能”的缺陷来应对该问题，然而这种定性概念在实践中过强，无法区分大体可复现的缺陷与真正不现实的缺陷。本文提出更灵活的定量版鲁棒可达性，并设计相应的符号执行形式，以自动度量触发缺陷的难度。该定量鲁棒符号执行（QRSE）建立在一种模型计数（model counting）变体之上，能够刻画攻击者可控变量与不可控变量之间的不对称性。这类模型计数问题虽已在贝叶斯网络、知识表示与概率规划等 AI 领域得到研究，但在形式验证语境中的使用带来了新的挑战。作者通过面向安全的案例研究（包括 libvncserver 中真实漏洞 CVE-2019-20839）展示了所提方案的适用性。
Most software analysis techniques focus on bug reachability. However, this approach is not ideal for security evaluation as it does not take into account the difficulty of triggering said bugs. The recently introduced notion of robust reachability tackles this issue by distinguishing between bugs that can be reached independently from uncontrolled inputs, from those that cannot. Yet, this qualitative notion is too strong in practice as it cannot distinguish mostly replicable bugs from truly unrealistic ones. In this work we propose a more flexible quantitative version of robust reachability together with a dedicated form of symbolic execution, in order to automatically measure the difficulty of triggering bugs. This Quantitative Robust Symbolic Execution (QRSE) relies on a variant of model counting, which allows to account for the asymmetry between attacker-controlled and uncontrolled variables. While this specific model counting problem has been studied in AI research fields such as Bayesian networks, knowledge representation and probabilistic planning, its use within the context of formal verification presents new challenges. We show the applicability of our solutions through security-oriented case studies, including real-world vulnerabilities such as CVE-2019-20839 from libvncserver.
@article{GirolLB24,
title = {Quantitative Robustness for Vulnerability Assessment},
author = {Guillaume Girol and Guilhem Lacombe and Sébastien Bardin},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656407}
}