A Symbolic Execution Framework for JavaScript
Authors:
- Prateek SaxenaPSPrateek Saxena
- Devdatta AkhaweDADevdatta Akhawe
- Steve HannaSHSteve Hanna
- Feng MaoFMFeng Mao
- Stephen McCamantSMStephen McCamant
- Dawn SongDSDawn Song
Top Cited Papers
- 1 January 2010
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10816011,p. 513-528
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 languages2009
- Extracting Models of Security-Sensitive Operations using String-Enhanced White-Box Exploration on Binaries2009
- Path Feasibility Analysis for String-Manipulating ProgramsLecture Notes in Computer Science, 2009
- Finding bugs in dynamic web applications2008
- Crawling AJAX by Inferring User Interface State Changes2008
- A Decision Procedure for Bit-Vectors and Arrays2007
- 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 logic1981