Abstract
Symbolic execution has been widely applied in detecting vulnerabilities in web applications. Modeling language-specific built-in functions is essential for symbolic execution. Since built-in functions tend to be complicated and are typically implemented in low-level languages, a common strategy is to manually translate them into the SMT-LIB language for constraint solving. Such translation requires an excessive amount of human effort and deep understandings of the function behaviors. Incorrect translation can invalidate the final results. This problem aggravates in PHP applications because of their cross-language nature, i.e., , the built-in functions are written in C, but the rest code is in PHP. In this paper, we explore the feasibility of automating the process of modeling PHP built-in functions for symbolic execution. We synthesize C programs by transforming the constraint solving task in PHP symbolic execution into a C-compliant format and integrating them with C implementations of the built-in functions. We apply symbolic execution on the synthesized C program to find a feasible path, which gives a solution that can be applied to the original PHP constraints. In this way, we automate the modeling of built-in functions in PHP applications. We thoroughly compare our automated method with the state-of-the-art manual modeling tool. The evaluation results demonstrate that our automated method is more accurate with a higher function coverage, and can exploit a similar number of vulnerabilities. Our empirical analysis also shows that the manual and automated methods have different strengths, which complement each other in certain scenarios. Therefore, the best practice is to combine both of them to optimize the accuracy, correctness, and coverage of symbolic execution.
Original language | English (US) |
---|---|
Title of host publication | The Web Conference 2021 - Proceedings of the World Wide Web Conference, WWW 2021 |
Publisher | Association for Computing Machinery, Inc |
Pages | 58-69 |
Number of pages | 12 |
ISBN (Electronic) | 9781450383127 |
DOIs | |
State | Published - Apr 19 2021 |
Event | 2021 World Wide Web Conference, WWW 2021 - Ljubljana, Slovenia Duration: Apr 19 2021 → Apr 23 2021 |
Publication series
Name | The Web Conference 2021 - Proceedings of the World Wide Web Conference, WWW 2021 |
---|
Conference
Conference | 2021 World Wide Web Conference, WWW 2021 |
---|---|
Country/Territory | Slovenia |
City | Ljubljana |
Period | 4/19/21 → 4/23/21 |
Bibliographical note
Publisher Copyright:© 2021 ACM.
Keywords
- Constraint solving
- PHP
- Symbolic execution