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 条
  • [41] Deconstructing Dynamic Symbolic Execution
    Ball, Thomas
    Daniel, Jakub
    DEPENDABLE SOFTWARE SYSTEMS ENGINEERING, 2015, 40 : 26 - 41
  • [42] Symbolic execution of programs with strings
    Redelinghuys, Gideon
    Visser, Willem
    Geldenhuys, Jaco
    PROCEEDINGS OF THE SOUTH AFRICAN INSTITUTE FOR COMPUTER SCIENTISTS AND INFORMATION TECHNOLOGISTS CONFERENCE, 2012, : 139 - 148
  • [43] Directed Incremental Symbolic Execution
    Person, Suzette
    Yang, Guowei
    Rungta, Neha
    Khurshid, Sarfraz
    PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, 2011, : 504 - 515
  • [44] Directed Incremental Symbolic Execution
    Yang, Guowei
    Person, Suzette
    Rungta, Neha
    Khurshid, Sarfraz
    ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2014, 24 (01)
  • [45] Symbolic Execution of Obfuscated Code
    Yadegari, Babak
    Debray, Saumya
    CCS'15: PROCEEDINGS OF THE 22ND ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY, 2015, : 732 - 744
  • [46] Lazy Counterfactual Symbolic Execution
    Hallahan, William T.
    Xue, Anton
    Bland, Maxwell Troy
    Jhala, Ranjit
    Piskac, Ruzica
    PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19), 2019, : 411 - 424
  • [47] Symbolic execution debugger (SED)
    Hentschel, Martin
    Bubel, Richard
    Hähnle, Reiner
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, 8734 : 255 - 262
  • [48] A Survey of Symbolic Execution Techniques
    Baldoni, Roberto
    Coppa, Emilio
    D'Elia, Daniele Cono
    Demetrescu, Camil
    Finocchi, Irene
    ACM COMPUTING SURVEYS, 2018, 51 (03) : 1 - 39
  • [49] A Personal Retrospective on Symbolic Execution
    Clarke, Lori A.
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2025, 51 (03) : 706 - 709
  • [50] ARRAY REPRESENTATION IN SYMBOLIC EXECUTION
    COENPORISINI, A
    DEPAOLI, F
    COMPUTER LANGUAGES, 1993, 18 (03): : 197 - 216