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|
|Number of pages||12|
|State||Published - Apr 19 2021|
|Event||2021 World Wide Web Conference, WWW 2021 - Ljubljana, Slovenia|
Duration: Apr 19 2021 → Apr 23 2021
|Name||The Web Conference 2021 - Proceedings of the World Wide Web Conference, WWW 2021|
|Conference||2021 World Wide Web Conference, WWW 2021|
|Period||4/19/21 → 4/23/21|
Bibliographical noteFunding Information:
The work was partly supported by a grant from the Research Grants Council of the Hong Kong SAR, China (CUHK 14210219). Kangjie Lu was supported in part by the NSF awards CNS-1815621 and CNS-1931208. Any opinions, findings, conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the RGC of HK or the NSF.
Â© 2021 ACM.
- Constraint solving
- Symbolic execution