A Symbolic Execution Framework for Java']JavaScript

被引:197
|
作者
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
来源
2010 IEEE SYMPOSIUM ON SECURITY AND PRIVACY | 2010年
关键词
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 条
  • [31] The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more
    Martin Hentschel
    Richard Bubel
    Reiner Hähnle
    International Journal on Software Tools for Technology Transfer, 2019, 21 : 485 - 513
  • [32] The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more
    Hentschel, Martin
    Bubel, Richard
    Haehnle, Reiner
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2019, 21 (05) : 485 - 513
  • [33] Symbolic Execution for Randomized Programs
    Susag, Zachary
    Lahiri, Sumit
    Hsu, Justin
    Roy, Subhajit
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2022, 6 (OOPSLA):
  • [34] Dependence Guided Symbolic Execution
    Wang, Haijun
    Liu, Ting
    Guan, Xiaohong
    Shen, Chao
    Zheng, Qinghua
    Yang, Zijiang
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2017, 43 (03) : 252 - 271
  • [35] Specification Extraction by Symbolic Execution
    Pichler, Josef
    2013 20TH WORKING CONFERENCE ON REVERSE ENGINEERING (WCRE), 2013, : 462 - 466
  • [36] Symbolic Execution of Virtual Devices
    Cong, Kai
    Xie, Fei
    Lei, Li
    2013 13TH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE (QSIC), 2013, : 1 - 10
  • [37] SymJEx: Symbolic Execution on the GraalVM
    Kloibhofer, Sebastian
    Pointhuber, Thomas
    Heisinger, Maximilian
    Moessenboeck, Hanspeter
    Stadler, Lukas
    Leopoldseder, David
    MPLR '20: PROCEEDINGS OF THE 17TH INTERNATIONAL CONFERENCE ON MANAGED PROGRAMMING LANGUAGES AND RUNTIMES, 2020, : 63 - 72
  • [38] Symbolic Execution Debugger (SED)
    Hentschel, Martin
    Bubel, Richard
    Haehnle, Reiner
    RUNTIME VERIFICATION, RV 2014, 2014, 8734 : 255 - 262
  • [39] Denotational Semantics for Symbolic Execution
    Voogd, Erik
    Klovstad, Asmund Aqissiaq Arild
    Johnsen, Einar Broch
    THEORETICAL ASPECTS OF COMPUTING, ICTAC 2023, 2023, 14446 : 370 - 387
  • [40] Directed Incremental Symbolic Execution
    Person, Suzette
    Yang, Guowei
    Rungta, Neha
    Khurshid, Sarfraz
    ACM SIGPLAN NOTICES, 2011, 46 (06) : 504 - 515