A Symbolic Execution Framework for Java']JavaScript

被引:192
|
作者
Saxena, Prateek [1 ]
Akhawe, Devdatta [1 ]
Hanna, Steve [1 ]
Mao, Feng [1 ]
McCamant, Stephen [1 ]
Song, Dawn [1 ]
机构
[1] Univ Calif Berkeley, Dept EECS, Div Comp Sci, Berkeley, CA 94720 USA
关键词
web security; symbolic execution; string decision procedures;
D O I
10.1109/SP.2010.38
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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.
引用
下载
收藏
页码:513 / 528
页数:16
相关论文
共 50 条
  • [1] Symbolic Execution for Java']JavaScript
    Santos, Jose Fragoso
    Maksimovic, Petar
    Grohens, Theotime
    Dolby, Julian
    Gardner, Philippa
    PPDP'18: PROCEEDINGS OF THE 20TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, 2018,
  • [2] JaVerT 2.0: Compositional Symbolic Execution for Java']JavaScript
    Santos, Jose Fragoso
    Maksimovic, Petar
    Sampaio, Gabriela
    Gardner, Philippa
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (POPL):
  • [3] Constraint Programming for Dynamic Symbolic Execution of Java']JavaScript
    Amadini, Roberto
    Andrlon, Mak
    Gange, Graeme
    Schachte, Peter
    Sondergaard, Harald
    Stuckey, Peter J.
    INTEGRATION OF CONSTRAINT PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND OPERATIONS RESEARCH, CPAIOR 2019, 2019, 11494 : 1 - 19
  • [4] ExpoSE: Practical Symbolic Execution of Standalone Java']JavaScript
    Loring, Blake
    Mitchell, Duncan
    Kinder, Johannes
    SPIN'17: PROCEEDINGS OF THE 24TH ACM SIGSOFT INTERNATIONAL SPIN SYMPOSIUM ON MODEL CHECKING OF SOFTWARE, 2017, : 196 - 199
  • [5] Sound Regular Expression Semantics for Dynamic Symbolic Execution of Java']JavaScript
    Loring, Blake
    Mitchell, Duncan
    Kinder, Johannes
    PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19), 2019, : 425 - 438
  • [6] Symbolic PathFinder: Symbolic execution of Java bytecode
    NASA Ames Research Center, Moffett Field, CA 94035, United States
    ASE - Proc. IEEE/ACM Int. Conf. Autom. Softw. Eng., (179-180):
  • [7] A Comparative Evaluation of Java']JavaScript Execution Behavior
    Martinsen, Jan Kasper
    Grahn, Hakan
    Isberg, Anders
    WEB ENGINEERING, ICWE 2011, 2011, 6757 : 399 - 402
  • [8] One solution for execution of Java']JavaScript in Java']Java EE application servers
    Vidakovic, Milan
    Cosic, Stefan
    Cosic, Ognjen
    Kastelan, Ivan
    Velikic, Gordana
    2018 ZOOMING INNOVATION IN CONSUMER TECHNOLOGIES CONFERENCE (ZINC), 2018, : 177 - 180
  • [9] Putting in All the Stops: Execution Control for Java']JavaScript
    Baxter, Samuel
    Nigam, Rachit
    Politz, Joe Gibbs
    Krishnamurthi, Shriram
    Guha, Arjun
    PROCEEDINGS OF THE 39TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, PLDI 2018, 2018, : 30 - 45
  • [10] Parallel Java']JavaScript Execution in Web Navigation Sequences
    Losada, Jose
    Raposo, Juan
    Pan, Alberto
    Montoto, Paula
    Alvarez, Manuel
    2015 IEEE/WIC/ACM INTERNATIONAL CONFERENCE ON WEB INTELLIGENCE AND INTELLIGENT AGENT TECHNOLOGY (WI-IAT), VOL 1, 2015, : 284 - 291