Automatic discovery of API-level exploits
Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, and Randal E. Bryant.
In 27th International Conference on Software Engineering (ICSE).
St. Louis, Missouri, May 2005.
We argue that finding vulnerabilities in software components is different from finding exploits against them. Exploits that compromise security often use several low-level details of the component, such as layouts of stack frames. Existing software analysis tools, while effective at identifying vulnerabilities, fail to model low-level details, and are hence unsuitable for exploit-finding.
We study the issues involved in exploit-finding by considering application programming interface (API) level exploits. A software component is vulnerable to an API-level exploit if its security can be compromised by invoking a sequence of API operations allowed by the component. We develop a formal framework that allows us to model low-level details of API operations, and develop an automatic technique based upon bounded, infinite-state model checking to discover API-level exploits.
We present two instantiations of this framework. We show that format-string exploits can be modeled as API-level exploits, and demonstrate our technique by finding exploits against vulnerabilities in widely-used software. We also use the framework to model a cryptographic-key management API (the IBM CCA) and demonstrate a tool that identifies a previously known exploit
Paper:
[pdf]
[ps]
Slides:
[ppt]
[html]
Source code:
[html]
An earlier version of this paper is available as a technical report:
