An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution
Static analysis is one of the techniques used today to analyze source codes and minimize the issue of software vulnerability. Static analysis has the ability to observe all possible software paths in an application through the scrutiny of a web application’s source code. Among those paths, some may...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2021-06-01
|
| Series: | Applied Sciences |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2076-3417/11/12/5384 |
| _version_ | 1827690178683076608 |
|---|---|
| author | Abdalla Wasef Marashdih Zarul Fitri Zaaba Khaled Suwais |
| author_facet | Abdalla Wasef Marashdih Zarul Fitri Zaaba Khaled Suwais |
| author_sort | Abdalla Wasef Marashdih |
| collection | DOAJ |
| description | Static analysis is one of the techniques used today to analyze source codes and minimize the issue of software vulnerability. Static analysis has the ability to observe all possible software paths in an application through the scrutiny of a web application’s source code. Among those paths, some may be considered feasible paths, which refer to any paths that the test cases can execute. The detection of feasible paths in the results of a static analysis helps to minimize the false positive rate. However, the detection of feasible paths can be challenging, especially for programs that have multiple conditions in the same branch. The aim is to ensure that each feasible path is detected only once (not duplicated). This paper proposes an approach based on minimal static single assignment (MSSA) form and symbolic execution to detect feasible paths. The proposed approach starts by converting the source code into an abstract syntax tree (AST), followed by converting the AST to minimal SSA representation, which helps to decrease the number of instructions in the SSA form. An algorithm was built to examine all of the instructions of the SSA form, identify whole paths in the source code, and extract constraints along each path. A path weight method (PWM) is proposed in this work to avoid detecting duplicated feasible paths. The satisfiability modulo theory (SMT) solver was used to check the satisfiability of each path condition. The proposed approach was tested on seven well-known test programs that have been used in related studies and 10 large scale programs. The experimental results indicate that the proposed method (PWM) can avoid detecting duplicated feasible paths, and the proposed approach reduced the time required for generating the paths compared to that in related studies. |
| first_indexed | 2024-03-10T10:32:44Z |
| format | Article |
| id | doaj.art-efa5b84c44d348a48f758ff371fa2690 |
| institution | Directory Open Access Journal |
| issn | 2076-3417 |
| language | English |
| last_indexed | 2024-03-10T10:32:44Z |
| publishDate | 2021-06-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Applied Sciences |
| spelling | doaj.art-efa5b84c44d348a48f758ff371fa26902023-11-21T23:32:55ZengMDPI AGApplied Sciences2076-34172021-06-011112538410.3390/app11125384An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic ExecutionAbdalla Wasef Marashdih0Zarul Fitri Zaaba1Khaled Suwais2School of Computer Sciences, Universiti Sains Malaysia, Pulau Pinang 11800, MalaysiaSchool of Computer Sciences, Universiti Sains Malaysia, Pulau Pinang 11800, MalaysiaFaculty of Computer Studies, Arab Open University, P.O.Box 84901, Riyadh 11681, Saudi ArabiaStatic analysis is one of the techniques used today to analyze source codes and minimize the issue of software vulnerability. Static analysis has the ability to observe all possible software paths in an application through the scrutiny of a web application’s source code. Among those paths, some may be considered feasible paths, which refer to any paths that the test cases can execute. The detection of feasible paths in the results of a static analysis helps to minimize the false positive rate. However, the detection of feasible paths can be challenging, especially for programs that have multiple conditions in the same branch. The aim is to ensure that each feasible path is detected only once (not duplicated). This paper proposes an approach based on minimal static single assignment (MSSA) form and symbolic execution to detect feasible paths. The proposed approach starts by converting the source code into an abstract syntax tree (AST), followed by converting the AST to minimal SSA representation, which helps to decrease the number of instructions in the SSA form. An algorithm was built to examine all of the instructions of the SSA form, identify whole paths in the source code, and extract constraints along each path. A path weight method (PWM) is proposed in this work to avoid detecting duplicated feasible paths. The satisfiability modulo theory (SMT) solver was used to check the satisfiability of each path condition. The proposed approach was tested on seven well-known test programs that have been used in related studies and 10 large scale programs. The experimental results indicate that the proposed method (PWM) can avoid detecting duplicated feasible paths, and the proposed approach reduced the time required for generating the paths compared to that in related studies.https://www.mdpi.com/2076-3417/11/12/5384detectionfeasible pathsSSAstatic analysissymbolic execution |
| spellingShingle | Abdalla Wasef Marashdih Zarul Fitri Zaaba Khaled Suwais An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution Applied Sciences detection feasible paths SSA static analysis symbolic execution |
| title | An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution |
| title_full | An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution |
| title_fullStr | An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution |
| title_full_unstemmed | An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution |
| title_short | An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution |
| title_sort | approach for detecting feasible paths based on minimal ssa representation and symbolic execution |
| topic | detection feasible paths SSA static analysis symbolic execution |
| url | https://www.mdpi.com/2076-3417/11/12/5384 |
| work_keys_str_mv | AT abdallawasefmarashdih anapproachfordetectingfeasiblepathsbasedonminimalssarepresentationandsymbolicexecution AT zarulfitrizaaba anapproachfordetectingfeasiblepathsbasedonminimalssarepresentationandsymbolicexecution AT khaledsuwais anapproachfordetectingfeasiblepathsbasedonminimalssarepresentationandsymbolicexecution AT abdallawasefmarashdih approachfordetectingfeasiblepathsbasedonminimalssarepresentationandsymbolicexecution AT zarulfitrizaaba approachfordetectingfeasiblepathsbasedonminimalssarepresentationandsymbolicexecution AT khaledsuwais approachfordetectingfeasiblepathsbasedonminimalssarepresentationandsymbolicexecution |