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
来源：
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] Dynamic Symbolic Execution for the Analysis of Web Server Applications in Java']Java
    Balasubramanian, Daniel
    Zhang, Zhenkai
    McDermet, Dan
    Karsai, Gabor
    SAC '19: PROCEEDINGS OF THE 34TH ACM/SIGAPP SYMPOSIUM ON APPLIED COMPUTING, 2019, : 2178 - 2185
  • [22] Probabilistic Programming for Java']Java using Symbolic Execution and Model Counting
    Visser, Willem
    Pasareanu, Corina S.
    SOUTH AFRICAN INSTITUTE OF COMPUTER SCIENTISTS AND INFORMATION TECHNOLOGISTS (SACSIT 2017), 2017, : 319 - 328
  • [23] JDART: Dynamic Symbolic Execution for Java']Java Bytecode (Competition Contribution)
    Mues, Malte
    Howar, Falk
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2020, 2020, 12079 : 398 - 402
  • [24] Verification of Java']Java programs using symbolic execution and invariant generation
    Pasareanu, CS
    Visser, W
    MODEL CHECKING SOFTWARE, 2004, 2989 : 164 - 181
  • [25] JPF-SE: A symbolic execution extension to Java']Java PathFinder
    Anand, Saswat
    Pasareanu, Corina S.
    Visser, Willem
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2007, 4424 : 134 - +
  • [26] Runtime Exception Detection in Java']Java Programs Using Symbolic Execution
    Kadar, Istvan
    Hegedus, Peter
    Ferene, Rudolf
    ACTA CYBERNETICA, 2014, 21 (03): : 331 - 352
  • [27] Anxiety: a dynamic symbolic execution framework
    Gerasimov, Alexander
    Vartanov, Sergey
    Ermakov, Mikhail
    Kruglov, Leonid
    Kutz, Daniil
    Novikov, Alexander
    Asryan, Seryozha
    2017 IVANNIKOV ISPRAS OPEN CONFERENCE (ISPRAS), 2017, : 16 - 21
  • [28] Synthesizing Framework Models for Symbolic Execution
    Jeon, Jinseong
    Qiu, Xiaokang
    Fetter-Degges, Jonathan
    Foster, Jeffrey S.
    Solar-Lezama, Armando
    2016 IEEE/ACM 38TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE), 2016, : 156 - 167
  • [29] AwaitViz: a Visualizer of Java']JavaScript's async/await execution order
    Tominaga, Ena
    Arahori, Yoshitaka
    Gondow, Katsuhiko
    SAC '19: PROCEEDINGS OF THE 34TH ACM/SIGAPP SYMPOSIUM ON APPLIED COMPUTING, 2019, : 2515 - 2524
  • [30] JS']JSForce: A Forced Execution Engine for Malicious Java']JavaScript Detection
    Hu, Xunchao
    Cheng, Yao
    Duan, Yue
    Henderson, Andrew
    Yin, Heng
    SECURITY AND PRIVACY IN COMMUNICATION NETWORKS, SECURECOMM 2017, 2018, 238 : 704 - 720
12345