Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

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 present a framework to model low-level details of APIs, and develop an automatic technique based on 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.

REFERENCES

• 1: Rajeev Alur , Pavol Černý , P. Madhusudan , Wonhong Nam, Synthesis of interface specifications for Java classes, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.98-109, January 12-14, 2005, Long Beach, California, USA
• 2: Glenn Ammons , Rastislav Bodík , James R. Larus, Mining specifications, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.4-16, January 16-18, 2002, Portland, Oregon
• 3: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 4: Dirk Beyer , Adam J. Chlipala , Rupak Majumdar, Generating Tests from Counterexamples, Proceedings of the 26th International Conference on Software Engineering, p.326-335, May 23-28, 2004
• 5: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 6: M. Bond. A chosen key difference attack on control vectors. Manuscript, November 2000. http://www.cl.cam.ac.uk/ mkb23/research/CVDif.pdf.
• 7: Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 8: Randal E. Bryant , Shuvendu K. Lahiri , Sanjit A. Seshia, Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Proceedings of the 14th International Conference on Computer Aided Verification, p.78-92, July 27-31, 2002
• 9: Tevfik Bultan , Richard Gerber , William Pugh, Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.4, p.747-789, July 1999 [doi>10.1145/325478.325480]
• 10: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 11: E. M. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Proc. 10th TACAS, 2004.
• 12: C. Cowan, M. Barringer, S. Beattie, G. Kroah-Hartman, M. Frantzen, and J. Lokier. FormatGuard: Automatic protection from printf format-string vulnerabilities. In Proc. 10th Security Symp. USENIX, 2001.
• 13: Luca de Alfaro , Thomas A. Henzinger, Interface automata, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 14: Leonardo M. de Moura , Harald Rueß , Maria Sorea, Lazy Theorem Proving for Bounded Model Checking over Infinite Domains, Proceedings of the 18th International Conference on Automated Deduction, p.438-455, July 27-30, 2002
• 15: D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198--208, 1983.
• 16: D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proc. 4th OSDI. ACM/USENIX, 2000.
• 17: D. F. Ferraiolo and D. R. Kuhn. Role based access control. In 15th National Computer Security Conference, October 1992.
• 18: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
• 19: V. Ganapathy, S. A. Seshia, S. Jha, T. W. Reps, and R. E. Bryant. Automatic discovery of API-level vulnerabilities. Technical Report 1512, CS Dept., Univ. of Wisconsin, 2004. http://www.cs.wisc.edu/wisa/papers/tr1512/tr1512.pdf.
• 20: Michael A. Harrison , Walter L. Ruzzo , Jeffrey D. Ullman, Protection in operating systems, Communications of the ACM, v.19 n.8, p.461-471, Aug. 1976 [doi>10.1145/360303.360333]
• 21: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 22: Greg Hoglund , Gary McGraw, Exploiting Software: How to Break Code, Pearson Higher Education, 2004
• 23: Daniel Jackson, Automating first-order relational logic, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.130-139, November 06-10, 2000, San Diego, California, United States
• 24: D. B. Johnson , G. M. Dolan , M. J. Kelly , A. V. Le , S. M. Matyas, Common cryptographic architecture cryptographic application programming interface, IBM Systems Journal, v.30 n.2, p.130-150, 1991
• 25: Rajeev Joshi , Greg Nelson , Keith Randall, Denali: a goal-directed superoptimizer, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 26: Henry Massalin, Superoptimizer: a look at the smallest program, Proceedings of the second international conference on Architectual support for programming languages and operating systems, p.122-126, October 1987, Palo Alto, California, United States
• 27: S. M. Matyas , A. V. Le , D. G. Abraham, A key-management scheme based on control vectors, IBM Systems Journal, v.30 n.2, p.175-191, 1991
• 28: C. Meadows. The NRL Protocol Analyzer: An overview. Journal of Logic Programming, 26(2):113--131, 1996.
• 29: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 30: T. Newsham. Format string attacks. www.securityfocus.com/guest/3342.
• 31: SecurityFocus. Qualcomm qpopper vulnerability. www.securityfocus.com/advisories/2271.
• 32: Sanjit A. Seshia , Randal E. Bryant, Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), p.100-109, July 13-17, 2004
• 33: U. Shankar, K. Talwar, J. S. Foster, and D. Wagner. Automated detection of format-string vulnerabilities using type qualifiers. In Proc. 10th Security Symp. USENIX, 2001.
• 34: Siege SAT solver. http://www.cs.sfu.ca/loryan/personal.
• 35: Aaron Stump , Clark W. Barrett , David L. Dill, CVC: A Cooperating Validity Checker, Proceedings of the 14th International Conference on Computer Aided Verification, p.500-504, July 27-31, 2002
• 36: Kevin Sullivan , Jinlin Yang , David Coppit , Sarfraz Khurshid , Daniel Jackson, Software assurance by bounded exhaustive testing, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 37: A. Thuemmel. Analysis of format string bugs. Manuscript, 2001. http://downloads.securityfocus.com/library/format-bug-analysis.pdf.
• 38: David Wagner , Drew Dean, Intrusion Detection via Static Analysis, Proceedings of the 2001 IEEE Symposium on Security and Privacy, p.156, May 14-16, 2001
• 39: D. Wagner, J. S. Foster, E. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In Proc. NDSS. ISOC, 2000.
• 40: Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.351-363, January 12-14, 2005, Long Beach, California, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Algorithms, Security, Verification

Keywords:
API-level exploit, bounded model checking