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 条
  • [21] Quantifying the Characteristics of Java']Java Programs that May Influence Symbolic Execution from a Test Data Generation Perspective
    Eler, Marcelo M.
    Endo, Andre T.
    Durelli, Vinicius H. S.
    2014 IEEE 38TH ANNUAL INTERNATIONAL COMPUTERS, SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), 2014, : 181 - 190
  • [22] A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution
    Thi Thu Ha Doan
    Thiemann, Peter
    PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2024, 2025, 15194 : 305 - 324
  • [23] Machine learning steered symbolic execution framework for complex software code
    Bu, Lei
    Liang, Yongjuan
    Xie, Zhunyi
    Qian, Hong
    Hu, Yi-Qi
    Yu, Yang
    Chen, Xin
    Li, Xuandong
    FORMAL ASPECTS OF COMPUTING, 2021, 33 (03) : 301 - 323
  • [24] A NOVEL SYMBOLIC EXECUTION FRAMEWORK FOR MULTI-PROCEDURE PROGRAM ANALYSIS
    Fan Wenqing
    Liang Hongling
    Yang Yixian
    Xu Guoai
    PROCEEDINGS OF 2009 2ND IEEE INTERNATIONAL CONFERENCE ON BROADBAND NETWORK & MULTIMEDIA TECHNOLOGY, 2009, : 858 - 863
  • [25] Symbolic Types for Lenient Symbolic Execution
    Chang, Stephen
    Knauth, Alex
    Torlak, Emina
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2
  • [26] An empirical study to quantify the characteristics of Java']Java programs that may influence symbolic execution from a unit testing perspective
    Eler, Marcelo M.
    Endo, Andre T.
    Durelli, Vinicius H. S.
    JOURNAL OF SYSTEMS AND SOFTWARE, 2016, 121 : 281 - 297
  • [27] Chopped Symbolic Execution
    Trabish, David
    Mattavelli, Andrea
    Rinetzky, Noam
    Cadar, Cristian
    PROCEEDINGS 2018 IEEE/ACM 40TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE), 2018, : 350 - 360
  • [28] Symbolic Router Execution
    Zhang, Peng
    Wang, Dan
    Gember-Jacobson, Aaron
    SIGCOMM '22: PROCEEDINGS OF THE 2022 ACM SIGCOMM 2022 CONFERENCE, 2022, : 336 - 349
  • [29] SYMBOLIC EXECUTION AND TESTING
    COWARD, PD
    INFORMATION AND SOFTWARE TECHNOLOGY, 1991, 33 (01) : 53 - 64
  • [30] Symbolic execution with abstraction
    Anand S.
    Pǎsǎreanu C.S.
    Visser W.
    International Journal on Software Tools for Technology Transfer, 2009, 11 (01) : 53 - 67