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 条
  • [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] 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
  • [4] Symbolic PathFinder: integrating symbolic execution with model checking for Java']Java bytecode analysis
    Pasareanu, Corina S.
    Visser, Willem
    Bushnell, David
    Geldenhuys, Jaco
    Mehlitz, Peter
    Rungta, Neha
    AUTOMATED SOFTWARE ENGINEERING, 2013, 20 (03) : 391 - 425
  • [5] Validating Converted Java']Java Code via Symbolic Execution
    Sneed, Harry M.
    Verhoef, Chris
    SOFTWARE QUALITY: COMPLEXITY AND CHALLENGES OF SOFTWARE ENGINEERING IN EMERGING TECHNOLOGIES, 2017, 269 : 70 - 83
  • [6] Java']Java Ranger: Statically Summarizing Regions for Efficient Symbolic Execution of Java']Java
    Sharma, Vaibhav
    Hussein, Soha
    Whalen, Michael W.
    McCamant, Stephen
    Visser, Willem
    PROCEEDINGS OF THE 28TH ACM JOINT MEETING ON EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING (ESEC/FSE '20), 2020, : 123 - 134
  • [7] JaVerT: Java']JavaScript Verification and Testing Framework
    Gardner, Philippa
    PPDP'18: PROCEEDINGS OF THE 20TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, 2018,
  • [8] 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
  • [9] 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
  • [10] Runtime Exception Detection in Java']Java Programs Using Symbolic Execution
    Kadar, Istvan
    Hegedus, Peter
    Ferene, Rudolf
    ACTA CYBERNETICA, 2014, 21 (03): : 331 - 352
12345