Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

A Symbolic Execution Framework for JavaScript

Prateek Saxena, Devdatta Akhawe, Steve Hanna, Feng Mao, Stephen McCamant and Dawn Song

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2010-26
March 8, 2010

http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-26.pdf

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.


BibTeX citation:

@techreport{Saxena:EECS-2010-26,
    Author = {Saxena, Prateek and Akhawe, Devdatta and Hanna, Steve and Mao, Feng and McCamant, Stephen and Song, Dawn},
    Title = {A Symbolic Execution Framework for JavaScript},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2010},
    Month = {Mar},
    URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-26.html},
    Number = {UCB/EECS-2010-26},
    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.}
}

EndNote citation:

%0 Report
%A Saxena, Prateek
%A Akhawe, Devdatta
%A Hanna, Steve
%A Mao, Feng
%A McCamant, Stephen
%A Song, Dawn
%T A Symbolic Execution Framework for JavaScript
%I EECS Department, University of California, Berkeley
%D 2010
%8 March 8
%@ UCB/EECS-2010-26
%U http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-26.html
%F Saxena:EECS-2010-26