Automated analysis of security APIs

Attacks on security systems within the past decade have revealed that security Application Programming Interfaces (APIs) expose a large and real attack surface but remain to be a relatively unexplored problem. In 2000, Bond et al. discovered API- chaining and type-confusion attacks on hardware security modules used in large banking systems. While these first attacks were found through human inspection of the API specifications, we take the approach of modeling these APIs formally and using an automated-reasoning tool to discover attacks. In particular, we discuss the techniques we used to model the Trusted Platform Module (TPM) v1.2 API and how we used OTTER, a theorem-prover, and ALLOY, a model-finder, to find both API- chaining attacks and to manage API complexity. Using ALLOY, we also developed techniques to capture attacks that weaken, but not fully compromise, a system's security. Finally, we demonstrate a number of real and "near-miss" vulnerabilities that were discovered against the TPM.

Department dc:contributor.department

Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2005

Author dc:creator

• Lin, Amerson H

Advisor dc:contributor.advisor

• Ronald R. Rivest.

• Electrical Engineering and Computer Science.

Statement dc:rights

• M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/33295

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/33295