Skip to main content
Erschienen in: Programming and Computer Software 6/2018

01.11.2018

An Approach to Reachability Determination for Static Analysis Defects with the Help of Dynamic Symbolic Execution

verfasst von: A. Yu. Gerasimov, L. V. Kruglov, M. K. Ermakov, S. P. Vartanov

Erschienen in: Programming and Computer Software | Ausgabe 6/2018

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Program analysis methods for error detection are conventionally divided into two groups: static analysis methods and dynamic analysis methods. In this paper, we present a combined approach that allows one to determine reachability for defects found by static program analysis techniques through applying dynamic symbolic execution to a program. This approach is an extension of our previous approach to determining the reachability of specific program instructions by using dynamic symbolic execution. The approach is sequentially applied to several points in the program: a defect source point, a defect sink point, and additional intermediate conditional jumps related to a defect under analysis. Our approach can be briefly described as follows. First, static analysis of the program executable code is carried out to gather information about execution paths that guide dynamic symbolic execution to the source point of a defect. Then, dynamic symbolic execution is performed to generate an input dataset for reaching the defect source point and the defect sink point through intermediate conditional jumps. Dynamic symbolic execution is guided by the heuristic of the minimum distance from the previous path to the next defect trace point when selecting execution paths. The distance metric is computed using an extended call graph of the program, which combines its call graph and portions of its control flow graph that include all paths leading to the defect sink point. We evaluate our approach by using several open-source command line programs from Debian Linux. The evaluation confirms that the proposed approach can be used for classification of defects found by static program analysis. However, we found some limitations that prevent deploying this approach to industrial program analyzers. Mitigating these limitations is one of the possible directions for future research.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literatur
1.
Zurück zum Zitat Vogelsang, A., Fehnker, A., Huuck, R., and Reif, W., Software metrics in static program analysis, Proc. 12th Int. Conf. Formal Engineering Methods and Software Engineering, Shanghai, 2010, pp. 485–500. Vogelsang, A., Fehnker, A., Huuck, R., and Reif, W., Software metrics in static program analysis, Proc. 12th Int. Conf. Formal Engineering Methods and Software Engineering, Shanghai, 2010, pp. 485–500.
2.
Zurück zum Zitat Kim, Y., Kim, Y., Kim, T., Lee, G., Jang, Y., and Kim, M., Automated unit testing of large industrial embedded software using concolic testing, Proc. 28th IEEE/ACM Int. Conf. Automated Software Engineering, Silicon Valley, 2013, pp. 519–528. Kim, Y., Kim, Y., Kim, T., Lee, G., Jang, Y., and Kim, M., Automated unit testing of large industrial embedded software using concolic testing, Proc. 28th IEEE/ACM Int. Conf. Automated Software Engineering, Silicon Valley, 2013, pp. 519–528.
3.
Zurück zum Zitat Xie, Y., Chou, A., and Engler, D., ARCHER: Using symbolic, path-sensitive analysis to detect memory access errors, Proc. 9th European Software Engineering Conf. held jointly with 11th ACM Sigsoft Int. Symp. Foundations of Software Engineering (ESEC/FSE), Helsinki, 2003, pp. 327–336. Xie, Y., Chou, A., and Engler, D., ARCHER: Using symbolic, path-sensitive analysis to detect memory access errors, Proc. 9th European Software Engineering Conf. held jointly with 11th ACM Sigsoft Int. Symp. Foundations of Software Engineering (ESEC/FSE), Helsinki, 2003, pp. 327–336.
4.
Zurück zum Zitat Bessey, A., Block, K., Chelf, B., Chow, A., Fulton, B., Hallem, S., Henri-Gros, C., Kamsky, A., McPeak, S., and Engler, D., A few billion lines of code later: Using static analysis to find bugs in the real world, Commun. ACM, 2010, vol. 53, no. 2, pp. 66–75.CrossRef Bessey, A., Block, K., Chelf, B., Chow, A., Fulton, B., Hallem, S., Henri-Gros, C., Kamsky, A., McPeak, S., and Engler, D., A few billion lines of code later: Using static analysis to find bugs in the real world, Commun. ACM, 2010, vol. 53, no. 2, pp. 66–75.CrossRef
5.
Zurück zum Zitat Ivannikov, V.P., Belevantsev, A.A., Borodin, A.E., Ignat’ev, V.N., Zhurikhin, D.M., Avetisyan, A.I., and Leonov, M.I., Static analyzer Svace for finding defects in source code of programs, Tr. Inst. Sistemnogo Program. Ross. Akad. Nauk, 2014, vol. 26, no. 1, pp. 231–250. Ivannikov, V.P., Belevantsev, A.A., Borodin, A.E., Ignat’ev, V.N., Zhurikhin, D.M., Avetisyan, A.I., and Leonov, M.I., Static analyzer Svace for finding defects in source code of programs, Tr. Inst. Sistemnogo Program. Ross. Akad. Nauk, 2014, vol. 26, no. 1, pp. 231–250.
6.
Zurück zum Zitat Engler, D., Chelf, B., Chou, A., and Hallen, S., Checking system rules using system-specific, programmer-written compiler extensions, Proc. 4th Conf. Operating System Design and Implementation (OSDI), San-Diego, 2000, vol. 4. Engler, D., Chelf, B., Chou, A., and Hallen, S., Checking system rules using system-specific, programmer-written compiler extensions, Proc. 4th Conf. Operating System Design and Implementation (OSDI), San-Diego, 2000, vol. 4.
7.
Zurück zum Zitat Johnson, B., Song, Y., Murphy-Hill, E., and Bowdidge, R., Why don’t software developers use static analysis tools to find bugs? Proc. Int. Conf. Software Engineering (ICSE), San Francisco, 2013. Johnson, B., Song, Y., Murphy-Hill, E., and Bowdidge, R., Why don’t software developers use static analysis tools to find bugs? Proc. Int. Conf. Software Engineering (ICSE), San Francisco, 2013.
8.
Zurück zum Zitat Christakis, M., Muller, P., and Wustholz, V., An experimental evaluation of deliberate unsoundness in a static program analyzer, Proc. Int. Workshop Verification, Model Checking, and Abstract Interpretation (VMCAI), Springer, 2015, pp. 336–354. Christakis, M., Muller, P., and Wustholz, V., An experimental evaluation of deliberate unsoundness in a static program analyzer, Proc. Int. Workshop Verification, Model Checking, and Abstract Interpretation (VMCAI), Springer, 2015, pp. 336–354.
9.
Zurück zum Zitat Livshits, B., Sridharan, M., Smaragdakis, Y., Lhotak, O., Amaral, J.N., Chang, B.-Y.E., Guyer, S.Z., Khedker, U.P., Mohler, A., and Vardoulakis, D., In defense of soundness: A manifesto, Commun. ACM, 2015, vol. 58, no. 2. Livshits, B., Sridharan, M., Smaragdakis, Y., Lhotak, O., Amaral, J.N., Chang, B.-Y.E., Guyer, S.Z., Khedker, U.P., Mohler, A., and Vardoulakis, D., In defense of soundness: A manifesto, Commun. ACM, 2015, vol. 58, no. 2.
10.
Zurück zum Zitat Cadar, C., Dunbar, D., and Endger, D., KLEE: Unassisted and automatic generation of high-coverage tests for complex systems, Proc. 8th USENIX Conf. Operating Systems Design and Implementation (OSDI), San Diego, 2008, pp. 209–224. Cadar, C., Dunbar, D., and Endger, D., KLEE: Unassisted and automatic generation of high-coverage tests for complex systems, Proc. 8th USENIX Conf. Operating Systems Design and Implementation (OSDI), San Diego, 2008, pp. 209–224.
11.
Zurück zum Zitat Averginos, T., Cha, S.K., Revert, A., Schwartz, E.J., Woo, M., and Brumley, D., Automatic exploit generation, Commun. ACM, 2014, vol. 57, no. 2, pp. 74–84. Averginos, T., Cha, S.K., Revert, A., Schwartz, E.J., Woo, M., and Brumley, D., Automatic exploit generation, Commun. ACM, 2014, vol. 57, no. 2, pp. 74–84.
12.
Zurück zum Zitat Chipunov, V., Kuznetsov, V., and Candea, G., The S2E platform: Design, implementation, and applications, ACM Trans. Comput. Syst., 2012, vol. 30, no.1. Chipunov, V., Kuznetsov, V., and Candea, G., The S2E platform: Design, implementation, and applications, ACM Trans. Comput. Syst., 2012, vol. 30, no.1.
13.
Zurück zum Zitat Manevich, R., Sridharan, M., Adams, S., Das, M., and Yang, Z., PSE: Explaining program failures via post-mortem static analysis, Proc. 12th ACM SIGSOFT Int. Symp. Foundations of Software Engineering, New York, 2004, pp. 63–72. Manevich, R., Sridharan, M., Adams, S., Das, M., and Yang, Z., PSE: Explaining program failures via post-mortem static analysis, Proc. 12th ACM SIGSOFT Int. Symp. Foundations of Software Engineering, New York, 2004, pp. 63–72.
14.
Zurück zum Zitat Song, D., Brumley, D., Yin, H., Caballero, J., Jager, I., Kang, M.G., Liang, Z., Newsome, J., Poosankam, P., and Saxena, P., BitBlaze: A new approach to computer security via binary analysis, Proc. 4th Int. Conf. Information Systems Security (ICISS), Hydarabad, India, 2008, pp. 1–25. Song, D., Brumley, D., Yin, H., Caballero, J., Jager, I., Kang, M.G., Liang, Z., Newsome, J., Poosankam, P., and Saxena, P., BitBlaze: A new approach to computer security via binary analysis, Proc. 4th Int. Conf. Information Systems Security (ICISS), Hydarabad, India, 2008, pp. 1–25.
15.
Zurück zum Zitat Sen, K., Marinov, D., and Agha, G., CUTE: A concolic unit testing engine for C, Proc. 10th European Software Engineering Conf. held jointly with 13th ACM SIGSOFT Int. Symp. Foundations of Software Engineering (ESEC/FSE), Lisbon, 2005, pp. 263–272. Sen, K., Marinov, D., and Agha, G., CUTE: A concolic unit testing engine for C, Proc. 10th European Software Engineering Conf. held jointly with 13th ACM SIGSOFT Int. Symp. Foundations of Software Engineering (ESEC/FSE), Lisbon, 2005, pp. 263–272.
17.
Zurück zum Zitat Cadar, C., Ganesh, V., Pawlowski, P., Dill, D.L., and Engler, D.R., EXE: Automatically generating inputs of death, Proc. 13th ACM Conf. Computer and Communications Security (CCS), Alexandria, USA, 2006, pp. 322–335. Cadar, C., Ganesh, V., Pawlowski, P., Dill, D.L., and Engler, D.R., EXE: Automatically generating inputs of death, Proc. 13th ACM Conf. Computer and Communications Security (CCS), Alexandria, USA, 2006, pp. 322–335.
18.
Zurück zum Zitat Schwartz, E.J., Averginos, T., and Brumley, D., All you ever wanted to know about dynamic tait analysis and forward symbolic execution (but might have been afraid to ask), Proc. IEEE Symp. Security and Privacy (SP), Oakland, 2010, pp. 317–331. Schwartz, E.J., Averginos, T., and Brumley, D., All you ever wanted to know about dynamic tait analysis and forward symbolic execution (but might have been afraid to ask), Proc. IEEE Symp. Security and Privacy (SP), Oakland, 2010, pp. 317–331.
19.
Zurück zum Zitat Csallner, C. and Smaragdakis, Y., Check’N’Crash: Combining static checking and testing, Proc. 27th Int. Conf. Software Engineering (ICSE), St. Louis, 2005, pp. 422–431. Csallner, C. and Smaragdakis, Y., Check’N’Crash: Combining static checking and testing, Proc. 27th Int. Conf. Software Engineering (ICSE), St. Louis, 2005, pp. 422–431.
20.
Zurück zum Zitat Chebaro, O., Kosmatov, N., Giorgetti, A., and Julliand, J., Programs slicing enhances a verification technique combining static and dynamic analysis, Proc. 27th Annual ACM Symp. Applied Computing, Trento, 2012, pp. 1284–1291. Chebaro, O., Kosmatov, N., Giorgetti, A., and Julliand, J., Programs slicing enhances a verification technique combining static and dynamic analysis, Proc. 27th Annual ACM Symp. Applied Computing, Trento, 2012, pp. 1284–1291.
21.
Zurück zum Zitat Kim, T., Park, J., Kulinda, I., and Jang, Y., Concolic testing framework for industrial embedded software, Proc. 21st Asia-Pacific Software Engineering Conf. (APSEC), Jeju, South Korea, 2014, vol. 2, pp. 7–10. Kim, T., Park, J., Kulinda, I., and Jang, Y., Concolic testing framework for industrial embedded software, Proc. 21st Asia-Pacific Software Engineering Conf. (APSEC), Jeju, South Korea, 2014, vol. 2, pp. 7–10.
22.
Zurück zum Zitat Hanna, A., Ling, H.Z., Yang, X., and Debbabi, M., A synergy between static and dynamic analysis or the detection of software security vulnerabilities, Proc. Confederated Int. Congress CoopIS, DOA, IS, and ADBASE on the Move to Meaningful Internet Systems: Part 2, Vilamoura, 2009, pp. 815–832. Hanna, A., Ling, H.Z., Yang, X., and Debbabi, M., A synergy between static and dynamic analysis or the detection of software security vulnerabilities, Proc. Confederated Int. Congress CoopIS, DOA, IS, and ADBASE on the Move to Meaningful Internet Systems: Part 2, Vilamoura, 2009, pp. 815–832.
23.
Zurück zum Zitat Csallner, C. and Smaragdakis, Y., DSD-Crasher: A hybrid analysis tool for bug finding, Proc. Int. Symp. Software Testing and Analysis (ISSTA), Portland, 2006, pp. 245–254. Csallner, C. and Smaragdakis, Y., DSD-Crasher: A hybrid analysis tool for bug finding, Proc. Int. Symp. Software Testing and Analysis (ISSTA), Portland, 2006, pp. 245–254.
24.
Zurück zum Zitat Artho, C. and Biere, A., Combined static and dynamic analysis, Electron. Notes Theor. Comput. Sci., 2005, vol. 131, pp. 3–14.CrossRef Artho, C. and Biere, A., Combined static and dynamic analysis, Electron. Notes Theor. Comput. Sci., 2005, vol. 131, pp. 3–14.CrossRef
25.
Zurück zum Zitat Chebaro, O., Kostomarov, N., Giorgetti, A., and Julliand, J., Combining static analysis and test generation for C program debugging, Proc. 4th Int. Conf. Tests and Proofs (TAP), Malaga, 2010, pp. 94–100. Chebaro, O., Kostomarov, N., Giorgetti, A., and Julliand, J., Combining static analysis and test generation for C program debugging, Proc. 4th Int. Conf. Tests and Proofs (TAP), Malaga, 2010, pp. 94–100.
26.
Zurück zum Zitat Schutte, J., Fedler, R., and Tetze, D., ConDroid: Targeted dynamic analysis of Android applications, Proc. 26th IEEE Int. Conf. Advanced Information Networking and Applications (AINA), Gwangui, South Korea, 2015. Schutte, J., Fedler, R., and Tetze, D., ConDroid: Targeted dynamic analysis of Android applications, Proc. 26th IEEE Int. Conf. Advanced Information Networking and Applications (AINA), Gwangui, South Korea, 2015.
27.
Zurück zum Zitat Ge, X., Taneja, K., Xie, T., and Tillmann, N., DyTa: Dynamic symbolic execution guided with static verification results, Proc. 33rd Int. Conf. Software Engineering (ICSE), Honolulu, 2011, pp. 992–994. Ge, X., Taneja, K., Xie, T., and Tillmann, N., DyTa: Dynamic symbolic execution guided with static verification results, Proc. 33rd Int. Conf. Software Engineering (ICSE), Honolulu, 2011, pp. 992–994.
28.
Zurück zum Zitat Gerasimov, A.Yu. and Kruglov, L.V., Computation of input data to reach a particular function in a program by the method of iterative dynamic analysis, Tr. Inst. Sistemnogo Program. Ross. Akad. Nauk, 2016, vol. 28, no. 5, pp. 159–174. Gerasimov, A.Yu. and Kruglov, L.V., Computation of input data to reach a particular function in a program by the method of iterative dynamic analysis, Tr. Inst. Sistemnogo Program. Ross. Akad. Nauk, 2016, vol. 28, no. 5, pp. 159–174.
29.
Zurück zum Zitat Stallman, R.M., Using the GNU compiler collection: A GNU manual for GCC version 4.3.3, Free Software Foundation Inc., 2004. Stallman, R.M., Using the GNU compiler collection: A GNU manual for GCC version 4.3.3, Free Software Foundation Inc., 2004.
30.
Zurück zum Zitat Isaev, I.K. and Sidorov, D.V., The use of dynamic analysis for generation of input data that demonstrates critical bugs and vulnerabilities in programs, Program. Comput. Software, 2010, vol. 36, no. 4, pp. 225–236.MathSciNetCrossRef Isaev, I.K. and Sidorov, D.V., The use of dynamic analysis for generation of input data that demonstrates critical bugs and vulnerabilities in programs, Program. Comput. Software, 2010, vol. 36, no. 4, pp. 225–236.MathSciNetCrossRef
31.
Zurück zum Zitat Free Software Foundation, GNU binutils. http:// www.gnu.org/software/binutils. Accessed November 1, 2017. Free Software Foundation, GNU binutils. http:// www.gnu.org/software/binutils. Accessed November 1, 2017.
Metadaten
Titel
An Approach to Reachability Determination for Static Analysis Defects with the Help of Dynamic Symbolic Execution
verfasst von
A. Yu. Gerasimov
L. V. Kruglov
M. K. Ermakov
S. P. Vartanov
Publikationsdatum
01.11.2018
Verlag
Pleiades Publishing
Erschienen in
Programming and Computer Software / Ausgabe 6/2018
Print ISSN: 0361-7688
Elektronische ISSN: 1608-3261
DOI
https://doi.org/10.1134/S0361768818060051

Weitere Artikel der Ausgabe 6/2018

Programming and Computer Software 6/2018 Zur Ausgabe