Skip to Main Content
 

Global Search Box

 
 
 
 

ETD Abstract Container

Abstract Header

Building An Abstract-Syntax-Tree-Oriented Symbolic Execution Engine for PHP Programs

Abstract Details

2018, Master of Science (MS), Wright State University, Computer Science.
This thesis presents the design, implementation, and evaluation of an abstract-syntax-tree-oriented symbolic execution engine for the PHP programming language. As a symbolic execution engine, our system emulate the execution of a PHP program by assuming that all inputs are with symbolic rather than concrete values. While our system inherits the basic definition of symbolic execution, it fundamentally differs from existing symbolic execution implementations that mainly leverage intermediate representation (IRs) to operate. Specifically, our system directly takes the abstract syntax tree (AST) of a program as input and subsequently interprets this AST. Performing symbolic execution using AST offers unique advantages. First, it enables one-to-one mapping between the source code and the analysis results such as control flows and data flows. Second, it makes possible the direct instrumentation on source code to enable developer-aware changes. Third, it has higher applicability since IR is not always available. The design and implementation of our symbolic execution engine essentially feature an interpreter that interprets the AST based on symbolic values. Different from an interpreter that deterministically follows a single execution path by operating on concrete input values, the interpreter we have built needs to generate all paths, where each path has a constraint and its own environment. Constraints and environments of paths need to be dynamically created and maintained while the AST is evaluated. Our interpreter is context-dependent, where all user-defined functions are faithfully when they are called. Once all paths for a program is generated, we will automatically translate the constraint of each path into assertions that can be verified by satisfiability modulo theories (SMT) solver (e.g., Z3). The SMT solver can further verifies assertions for each path and report i) concrete input values that enable this path or ii) the infeasibility of this path. We have tested our system using both prototype PHP programs iii) and real PHP programs collected from WordPress plugins. The experimental results have demonstrated our system is highly effective in performing symbolic execution.
Junjie Zhang, Ph.D. (Advisor)
Krishnaprasad Thirunarayan, Ph.D. (Committee Member)
Phu H. Phung, Ph.D. (Committee Member)
57 p.

Recommended Citations

Citations

  • Huang, J. (2018). Building An Abstract-Syntax-Tree-Oriented Symbolic Execution Engine for PHP Programs [Master's thesis, Wright State University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=wright1527358331843492

    APA Style (7th edition)

  • Huang, Jin. Building An Abstract-Syntax-Tree-Oriented Symbolic Execution Engine for PHP Programs. 2018. Wright State University, Master's thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=wright1527358331843492.

    MLA Style (8th edition)

  • Huang, Jin. "Building An Abstract-Syntax-Tree-Oriented Symbolic Execution Engine for PHP Programs." Master's thesis, Wright State University, 2018. http://rave.ohiolink.edu/etdc/view?acc_num=wright1527358331843492

    Chicago Manual of Style (17th edition)