Publication Date
2018
Document Type
Thesis
Committee Members
Phu H. Phung (Committee Member), Krishnaprasad Thirunarayan (Committee Member), Junjie Zhang (Advisor)
Degree Name
Master of Science (MS)
Abstract
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.
Page Count
57
Department or Program
Department of Computer Science and Engineering
Year Degree Awarded
2018
Copyright
Copyright 2018, all rights reserved. My ETD will be available under the "Fair Use" terms of copyright law.
