Software vulnerability detection using backward trace analysis and symbolic execution

Hongzhe Li, Taebeom Kim, Munkhbayar Bat-Erdene, Heejo Lee

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)

Abstract

Software vulnerability has long been considered an important threat to the safety of software systems. When source code is accessible, we can get much help from the information of source code to detect vulnerabilities. Static analysis has been used frequently to scan code for errors that cause security problems when source code is available. However, they often generate many false positives. Symbolic execution has also been proposed to detect vulnerabilities and has shown good performance in some researches. However, they are either ineffective in path exploration or could not scale well to large programs. During practical use, since most of paths are actually not related to security problems and software vulnerabilities are usually caused by the improper use of security-sensitive functions, the number of paths could be reduced by tracing sensitive data backwardly from security-sensitive functions so as to consider paths related to vulnerabilities only. What's more, in order to leave ourselves free from generating bug triggering test input, formal reasoning could be used by solving certain program conditions. In this research, we propose backward trace analysis and symbolic execution to detect vulnerabilities from source code. We first find out all the hot spot in source code file. Based on each hot spot, we construct a data flow tree so that we can get the possible execution traces. Afterwards, we do symbolic execution to generate program constraint(PC) and get security constraint(SC) from our predefined security requirements along each execution trace. A program constraint is a constraint imposed by program logic on program variables. A security constraint(SC) is a constraint on program variables that must be satisfied to ensure system security. Finally, this hot spot will be reported as a vulnerability if there is an assignment of values to program inputs which could satisfy PC but violates SC, in other words, satisfy PCèSC. We have implemented our approach and conducted experiments on test cases which we randomly choose from Juliet Test Suites provided by US National Security Agency(NSA). The results show that our approach achieves Precision value of 83.33%, Recall value of 90.90% and F1 Value of 86.95% which gains the best performance among competing tools. Moreover, our approach can efficiently mitigate path explosion problem in traditional symbolic execution.

Original languageEnglish
Title of host publicationProceedings - 2013 International Conference on Availability, Reliability and Security, ARES 2013
Pages446-454
Number of pages9
DOIs
Publication statusPublished - 2013 Dec 1
Event2013 8th International Conference on Availability, Reliability and Security, ARES 2013 - Regensburg, Germany
Duration: 2013 Sep 22013 Sep 6

Other

Other2013 8th International Conference on Availability, Reliability and Security, ARES 2013
CountryGermany
CityRegensburg
Period13/9/213/9/6

Fingerprint

Trace analysis
National security
Static analysis
Security systems
Explosions
Experiments

Keywords

  • Program constraint
  • Static analysis
  • Symbolic execution
  • Vulnerability detection

ASJC Scopus subject areas

  • Safety, Risk, Reliability and Quality

Cite this

Li, H., Kim, T., Bat-Erdene, M., & Lee, H. (2013). Software vulnerability detection using backward trace analysis and symbolic execution. In Proceedings - 2013 International Conference on Availability, Reliability and Security, ARES 2013 (pp. 446-454). [6657275] https://doi.org/10.1109/ARES.2013.59

Software vulnerability detection using backward trace analysis and symbolic execution. / Li, Hongzhe; Kim, Taebeom; Bat-Erdene, Munkhbayar; Lee, Heejo.

Proceedings - 2013 International Conference on Availability, Reliability and Security, ARES 2013. 2013. p. 446-454 6657275.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Li, H, Kim, T, Bat-Erdene, M & Lee, H 2013, Software vulnerability detection using backward trace analysis and symbolic execution. in Proceedings - 2013 International Conference on Availability, Reliability and Security, ARES 2013., 6657275, pp. 446-454, 2013 8th International Conference on Availability, Reliability and Security, ARES 2013, Regensburg, Germany, 13/9/2. https://doi.org/10.1109/ARES.2013.59
Li H, Kim T, Bat-Erdene M, Lee H. Software vulnerability detection using backward trace analysis and symbolic execution. In Proceedings - 2013 International Conference on Availability, Reliability and Security, ARES 2013. 2013. p. 446-454. 6657275 https://doi.org/10.1109/ARES.2013.59
Li, Hongzhe ; Kim, Taebeom ; Bat-Erdene, Munkhbayar ; Lee, Heejo. / Software vulnerability detection using backward trace analysis and symbolic execution. Proceedings - 2013 International Conference on Availability, Reliability and Security, ARES 2013. 2013. pp. 446-454
@inproceedings{da8fa3a244f24d94aa4f816b911f4743,
title = "Software vulnerability detection using backward trace analysis and symbolic execution",
abstract = "Software vulnerability has long been considered an important threat to the safety of software systems. When source code is accessible, we can get much help from the information of source code to detect vulnerabilities. Static analysis has been used frequently to scan code for errors that cause security problems when source code is available. However, they often generate many false positives. Symbolic execution has also been proposed to detect vulnerabilities and has shown good performance in some researches. However, they are either ineffective in path exploration or could not scale well to large programs. During practical use, since most of paths are actually not related to security problems and software vulnerabilities are usually caused by the improper use of security-sensitive functions, the number of paths could be reduced by tracing sensitive data backwardly from security-sensitive functions so as to consider paths related to vulnerabilities only. What's more, in order to leave ourselves free from generating bug triggering test input, formal reasoning could be used by solving certain program conditions. In this research, we propose backward trace analysis and symbolic execution to detect vulnerabilities from source code. We first find out all the hot spot in source code file. Based on each hot spot, we construct a data flow tree so that we can get the possible execution traces. Afterwards, we do symbolic execution to generate program constraint(PC) and get security constraint(SC) from our predefined security requirements along each execution trace. A program constraint is a constraint imposed by program logic on program variables. A security constraint(SC) is a constraint on program variables that must be satisfied to ensure system security. Finally, this hot spot will be reported as a vulnerability if there is an assignment of values to program inputs which could satisfy PC but violates SC, in other words, satisfy PC{\`e}SC. We have implemented our approach and conducted experiments on test cases which we randomly choose from Juliet Test Suites provided by US National Security Agency(NSA). The results show that our approach achieves Precision value of 83.33{\%}, Recall value of 90.90{\%} and F1 Value of 86.95{\%} which gains the best performance among competing tools. Moreover, our approach can efficiently mitigate path explosion problem in traditional symbolic execution.",
keywords = "Program constraint, Static analysis, Symbolic execution, Vulnerability detection",
author = "Hongzhe Li and Taebeom Kim and Munkhbayar Bat-Erdene and Heejo Lee",
year = "2013",
month = "12",
day = "1",
doi = "10.1109/ARES.2013.59",
language = "English",
isbn = "9780769550084",
pages = "446--454",
booktitle = "Proceedings - 2013 International Conference on Availability, Reliability and Security, ARES 2013",

}

TY - GEN

T1 - Software vulnerability detection using backward trace analysis and symbolic execution

AU - Li, Hongzhe

AU - Kim, Taebeom

AU - Bat-Erdene, Munkhbayar

AU - Lee, Heejo

PY - 2013/12/1

Y1 - 2013/12/1

N2 - Software vulnerability has long been considered an important threat to the safety of software systems. When source code is accessible, we can get much help from the information of source code to detect vulnerabilities. Static analysis has been used frequently to scan code for errors that cause security problems when source code is available. However, they often generate many false positives. Symbolic execution has also been proposed to detect vulnerabilities and has shown good performance in some researches. However, they are either ineffective in path exploration or could not scale well to large programs. During practical use, since most of paths are actually not related to security problems and software vulnerabilities are usually caused by the improper use of security-sensitive functions, the number of paths could be reduced by tracing sensitive data backwardly from security-sensitive functions so as to consider paths related to vulnerabilities only. What's more, in order to leave ourselves free from generating bug triggering test input, formal reasoning could be used by solving certain program conditions. In this research, we propose backward trace analysis and symbolic execution to detect vulnerabilities from source code. We first find out all the hot spot in source code file. Based on each hot spot, we construct a data flow tree so that we can get the possible execution traces. Afterwards, we do symbolic execution to generate program constraint(PC) and get security constraint(SC) from our predefined security requirements along each execution trace. A program constraint is a constraint imposed by program logic on program variables. A security constraint(SC) is a constraint on program variables that must be satisfied to ensure system security. Finally, this hot spot will be reported as a vulnerability if there is an assignment of values to program inputs which could satisfy PC but violates SC, in other words, satisfy PCèSC. We have implemented our approach and conducted experiments on test cases which we randomly choose from Juliet Test Suites provided by US National Security Agency(NSA). The results show that our approach achieves Precision value of 83.33%, Recall value of 90.90% and F1 Value of 86.95% which gains the best performance among competing tools. Moreover, our approach can efficiently mitigate path explosion problem in traditional symbolic execution.

AB - Software vulnerability has long been considered an important threat to the safety of software systems. When source code is accessible, we can get much help from the information of source code to detect vulnerabilities. Static analysis has been used frequently to scan code for errors that cause security problems when source code is available. However, they often generate many false positives. Symbolic execution has also been proposed to detect vulnerabilities and has shown good performance in some researches. However, they are either ineffective in path exploration or could not scale well to large programs. During practical use, since most of paths are actually not related to security problems and software vulnerabilities are usually caused by the improper use of security-sensitive functions, the number of paths could be reduced by tracing sensitive data backwardly from security-sensitive functions so as to consider paths related to vulnerabilities only. What's more, in order to leave ourselves free from generating bug triggering test input, formal reasoning could be used by solving certain program conditions. In this research, we propose backward trace analysis and symbolic execution to detect vulnerabilities from source code. We first find out all the hot spot in source code file. Based on each hot spot, we construct a data flow tree so that we can get the possible execution traces. Afterwards, we do symbolic execution to generate program constraint(PC) and get security constraint(SC) from our predefined security requirements along each execution trace. A program constraint is a constraint imposed by program logic on program variables. A security constraint(SC) is a constraint on program variables that must be satisfied to ensure system security. Finally, this hot spot will be reported as a vulnerability if there is an assignment of values to program inputs which could satisfy PC but violates SC, in other words, satisfy PCèSC. We have implemented our approach and conducted experiments on test cases which we randomly choose from Juliet Test Suites provided by US National Security Agency(NSA). The results show that our approach achieves Precision value of 83.33%, Recall value of 90.90% and F1 Value of 86.95% which gains the best performance among competing tools. Moreover, our approach can efficiently mitigate path explosion problem in traditional symbolic execution.

KW - Program constraint

KW - Static analysis

KW - Symbolic execution

KW - Vulnerability detection

UR - http://www.scopus.com/inward/record.url?scp=84892391747&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84892391747&partnerID=8YFLogxK

U2 - 10.1109/ARES.2013.59

DO - 10.1109/ARES.2013.59

M3 - Conference contribution

SN - 9780769550084

SP - 446

EP - 454

BT - Proceedings - 2013 International Conference on Availability, Reliability and Security, ARES 2013

ER -