Quantitative Robustness for Vulnerability Assessment

Explore a 16-minute conference talk from PLDI 2024 that introduces a quantitative approach to robust reachability for vulnerability assessment in software. Learn about Quantitative Robust Symbolic Execution (QRSE), a novel technique that measures the difficulty of triggering bugs by considering the asymmetry between attacker-controlled and uncontrolled variables. Discover how this method improves upon traditional bug reachability analysis for security evaluation by distinguishing between mostly replicable bugs and unrealistic ones. Examine the application of functional E-MAJSAT, a variant of model counting, in the context of formal verification. Gain insights into the practical applications of this approach through security-oriented case studies, including an analysis of the real-world vulnerability CVE-2019-20839 from libvncserver.