# An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution
## 4 Detection Methodology
### Avoid Duplicated Feasible Paths
Furthermore, with such dynamic analytical approaches, it might not be possible to acquire a deeper understanding of how an application should behave, which may lead to lower rates of detection. ## 8 Conclusions

This paper proposed an approach to detect feasible paths based on minimal SSA representation and symbolic execution based on PHP. It starts by parsing the source code to present an AST, followed by converting the AST to minimal SSA form, which is later optimized to produce a minimal SSA form to decrease the number of instructions and the number of \(\phi\) functions that would be analyzed. A symbolic input for each superglobal variable and uninitialized variable is assigned, and the paths and the conditions among each path are generated. Furthermore, we introduced a method for avoiding detecting duplicated feasible paths. The path conditions were the target for the Z3 solver to check the satisfiability. To evaluate the proposed approach, we conducted experiments using seven test programs that have been used in the related studies and 10 large scale web applications. The results obtained indicated that the proposed approach improved the time required to generate the paths and avoided detecting duplicated feasible paths. For future works, we plan to implement the proposed approach based on another language such as C or Java. The proposed approach can be improved by implementing it on a multiprocessor or distributed systems, which it will help to decrease the time required to generate the paths, especially for large systems. The proposed method (PWM) has the ability to avoid detection of duplicated feasible paths; thus, it could be combined with other evolutionary algorithms (i.e., as part of the fitness function in genetic algorithms) to reduce the number of iterations that will detect the same feasible paths more than once (duplicated paths). In addition, we will attempt to combine the proposed approach with taint analysis to detect security vulnerability in web applications. We expect the proposed approach to help decrease the false positive and false negative rates of static taint analysis. Moreover, the proposed approach could be extended to export the features of the source code, which could help machine learning algorithms to obtain knowledge on program flaws. Methodology, Z.F.Z. and K.S. ; software, A.W.M. ; formal analysis, A.W.M. ; data curation, A.W.M. ; writing--original draft preparation, A.W.M. ; writing--review and editing, Z.F.Z. and K.S. ; supervision, Z.F.Z. and K.S. All authors contributed substantially to the work reported. All authors have read and agreed to the published version of the manuscript. This research received no external funding. The C and PHP source codes of each test program used in this study are publicly available at [[https://github.com/[PERSON]/FP-C-PHP-Datasets](https://github.com/[PERSON]/FP-C-PHP-Datasets)]([https://github.com/[PERSON]/FP-C-PHP-Datasets](https://github.com/Amarashdeh/FP-C-PHP-Datasets)); accessed on 15 May 2021. The authors would like to thank Universiti Sains Malaysia and Arab Open University, Saudi Arabia for supporting this study. The authors declare no conflict of interest. The following abbreviations are used in this manuscript: \begin{tabular}{l l} AST & Abstract Syntax Tree \\ API & Application Programming Interface \\ CUTE & Concolic Unit Testing Engine \\ CFG & Control Flow Graph \\ DART & Directed Automated Random Testing \\ DFD & Duplicated Feasible paths Detected \\ EXE & Execution Generated Executions \\ FD & Feasible Path Detected \\ PHP & Hypertext Preprocessor \\ IR & Intermediate Representation \\ Jpf & Java PathFinder \\ LoC & Line of Code \\ LIVM & Low-Level Virtual Machine \\ MSR-LA & Microsoft Research License Agreement \\ MSSA & Minimal Static Single Assignment \\ PWM & Path Weight Method \\ SMT & Satisfiability Modulo Theory \\ STP & Simple Theorem Prover \\ SSA & Static Single Assignment \\ TFP & True Feasible Paths \\ \end{tabular} 

The following symbols are used in this manuscript: