On the Feasibility of Automated Built-in Function Modeling for PHP Symbolic Execution
On the Feasibility of Automated Built-in Function Modeling for PHP Symbolic Execution
复制标题
论PHP符号执行的自动内置函数建模的可行性
DOI：
10.1145/3442381.3450002
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Luo, Changhua
中科院分区：
文献类型：
--
作者：
Li, Penghui;Meng, Wei;Lu, Kangjie;Luo, Changhua
符号执行已被广泛应用于Web应用程序中的漏洞检测。对特定于语言的内置函数进行建模对于符号执行是必不可少的。由于内置函数往往很复杂，并且通常是用低级语言实现的，因此一个常见的策略是将它们手动转换为SMT-LIB语言以进行约束求解。这种翻译需要大量的人力和对功能行为的深刻理解。不正确的翻译会使最终结果无效。这个问题在PHP应用程序中很常见，因为它们的跨语言特性，即，在本文中，我们探讨了自动化建模PHP内置函数的符号执行过程的可行性。我们合成C程序的约束求解任务转换成一个C兼容的格式，并将它们与C实现的内置功能。我们应用符号执行的合成C程序，找到一个可行的路径，这给出了一个解决方案，可以应用到原来的PHP约束。通过这种方式，我们实现了PHP应用程序中内置函数的自动化建模，并将我们的自动化方法与最先进的手动建模工具进行了全面的比较。评估结果表明，我们的自动化方法更准确，功能覆盖率更高，并且可以利用类似数量的漏洞。我们的实证分析还表明，手动和自动化方法具有不同的优势，在某些情况下相互补充。因此，最佳实践是将两者联合收割机结合起来，以优化符号执行的准确性、正确性和覆盖率。
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.
登录
查看更多内容
DOI：
--
发表时间：
2020
期刊：
--
影响因子：
--
作者：
Fraser Brown;D. Stefan;D. Engler
通讯作者：
Fraser Brown;D. Stefan;D. Engler
DOI：
10.1109/dsn.2019.00064
发表时间：
2019-06
期刊：
2019 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)
影响因子：
--
作者：
Jin Huang;Yu Li;Junjie Zhang;Rui Dai
通讯作者：
Jin Huang;Yu Li;Junjie Zhang;Rui Dai
DOI：
10.1007/978-3-642-81955-1_19
发表时间：
1983
期刊：
J. Log. Algebraic Methods Program.
影响因子：
--
作者：
G. Robinson;L. Wos
通讯作者：
L. Wos
永远运行符号执行
DOI：
10.1145/3395363.3397360
发表时间：
2020
期刊：
--
影响因子：
--
作者：
Busse F
通讯作者：
Busse F