Sound Abstract Nonexploitability Analysis

Runtime errors that can be triggered by an attacker are sensibly more dangerous than others, as they not only result in program failure, but can also be exploited and lead to security breaches such as Denial-of-Service attacks or remote code execution. Proving the absence of exploitable runtime errors is challenging, as it involves combining classic techniques for safety with novel security analyses. While numerous approaches to statically detect runtime errors have been proposed, they lack the ability to classify program failures as potentially exploitable or not. In this paper, we bridge the gap between traditional safety properties and security hyperproperties by putting forward a novel definition of nonexploitability, which we leverage to propose a sound static analysis by abstract interpretation to prove the absence of exploitable runtime errors. While false alarms can occur, if our analysis determines that a program is nonexploitable, then there is a strong mathematical guarantee that it is impossible for an attacker to trigger a runtime error. Furthermore, our analysis reduces the noise generated from false positives by classifying each warning as security-critical or not. We implemented the first nonexploitability analyzer for a subset of C, and we evaluated it on a set of $77$ real-world programs taken from the GNU Coreutils package that are long up to $4,188$ lines of code. Our analysis was able to prove that more than 70% of the runtime errors previously reported ($3,498$ over $4,715$) cannot be triggered by an attacker.