A Symbolic Execution Framework for JavaScript
Top Cited Papers
- 1 January 2010
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 513-528
- https://doi.org/10.1109/sp.2010.38
Abstract
As AJAX applications gain popularity, client-side JavaScript code is becoming increasingly complex. However, few automated vulnerability analysis tools for JavaScript exist. In this paper, we describe the first system for exploring the execution space of JavaScript code using symbolic execution. To handle JavaScript code's complex use of string operations, we design a new language of string constraints and implement a solver for it. We build an automatic end-to-end tool, Kudzu, and apply it to the problem of finding client-side code injection vulnerabilities. In experiments on 18 live web applications, Kudzu automatically discovers 2 previously unknown vulnerabilities and 9 more that were previously found only with a manually-constructed test suite.Keywords
This publication has 16 references indexed in Scilit:
- A decision procedure for subset constraints over regular languagesPublished by Association for Computing Machinery (ACM) ,2009
- Extracting Models of Security-Sensitive Operations using String-Enhanced White-Box Exploration on BinariesPublished by Defense Technical Information Center (DTIC) ,2009
- Path Feasibility Analysis for String-Manipulating ProgramsLecture Notes in Computer Science, 2009
- Finding bugs in dynamic web applicationsPublished by Association for Computing Machinery (ACM) ,2008
- Crawling AJAX by Inferring User Interface State ChangesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2008
- A Decision Procedure for Bit-Vectors and ArraysPublished by Springer Science and Business Media LLC ,2007
- The expressibility of languages and relations by word equationsLecture Notes in Computer Science, 1997
- Periodic sets of integersTheoretical Computer Science, 1994
- Definability in the Existential Theory of Concatenation and Undecidable Extensions of this TheoryMathematical Logic Quarterly, 1988
- Equations between regular terms and an application to process logicPublished by Association for Computing Machinery (ACM) ,1981