Directed dynamic symbolic execution of programs to confirm errors in programs

 
PIIS013234740001213-9-1
DOI10.31857/S013234740001213-9
Publication type Article
Status Published
Authors
Affiliation: Institute for System Programming them. V.P. Ivannikova RAS
Address: Russian Federation
Journal nameProgrammirovanie
EditionIssue 5
Pages31-42
Abstract

  

Keywords
Received26.10.2018
Publication date28.10.2018
Number of characters1286
Cite   Download pdf To download PDF you should sign in
Размещенный ниже текст является ознакомительной версией и может не соответствовать печатной

views: 1146

Readers community rating: votes 0

1. Ayewah, N., Hovemeyer, D., Morgenthaler, J.D., Penix, J., and Pugh, W. Experiences Using Static Analysis to Find Bugs, Journal IEEE Software, vol. 25, no. 5, September 2008, pp. 22–29.

2. Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O’Hearn, P.W., Papakonstantinou, I., Purbrick, J., and Rodri-guez, D. Moving fast with software verification, NFM, vol. 9058 of Lecture Notes in Computer Science, Springer, 2015, pp. 3–11.

3. Calcagno, C. and Distefano, D. Infer: An automatic program verifier for memory safety of C programs, NASA Formal Methods, vol. 6617 of Lecture Notes in Computer Science, Springer, 2011, pp. 459–465.

4. GOSTR 56939-2016 Zaschita informatsii. Razrabotka bezopasnogo programmnogo obespecheniya. Obschie trebovaniya. // Natsional'nyj standart Rossijskoj Federatsii. Federal'noe agentstvo po tekhnicheskomu regulirovaniyu i metrologii.

5. Turing A.M. On Computable Numbers, with an Application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, vol. s2–42, no. 1, 1 January 1937, pp. 230–265.

6. Belevantsev A.A. Mnogourovnevyj staticheskij analiz iskhodnogo koda dlya obespecheniya kachestva programm // Dissertatsiya na soiskanie uchenoj stepeni doktora fiziko-matematicheskikh nauk, Moskva, 2017, 229 s.

7. Johnson, B., Song, Y., Murphy-Hill, E., and Bowdidge, R. Why Don’t Software Developers Use Static Analysis Tools to Find Bugs? Proceedings ICSE’13 Proceedings of the 2013 International Conference on Software Engineering, San Francisco, CA, USA, May 18–26, 2013, pp. 672–681.

8. Sadowski, C., Aftandilian, E., Eagle, A., Miller-Cushon, L., and Jaspan, C. Lessons from Building Static Analysis Tools at Google, Communications of the ACM, vol. 61, no. 4, pp. 58–66.

9. Boyer, R.S., Elspas, B., and Levitt, K.N. SELECT — a formal system for testing and debugging programs by symbolic execution, Proceedings of the international conference on Reliable software, Los Angeles, California, April 21 – 23, 1975, pp. 234–245.

10. Guidelines for the Use of the C Language in CriticalSystems, ISBN 978-1-906400-10-1 (paperback),ISBN 978-1-906400-11-8 (PDF), March 2013.

11. Seacord, R.C. and Martin, R. MITRE CWE and CERT Secure Coding Standards, Addison-WesleyProfessional, 2009.

12. King, J.C. Symbolic execution and program testing, Magazine Communications of the ACM, vol. 19, no. 7, July 1976, pp. 385–394.

13. Ganesh, V. and Dill, D.L. A decision procedure for bit-vectors and arrays, CAV’07 Proceedings of the 19th international conference on Computer aided verification, Berlin, Germany, July 03 – 07, 2007, pp. 519–531.

14. De Moura, L. and Bjorner, N. Z3: an efficient SMT solver, TACAS’08/ETAPS’08 Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems, Budapest, Hungary, March 29 – April 06, 2008, pp. 337–340.

15. Baldoni, R., Coppa, E., D’Elia, D., Demetrescu, C., and Finocchi, I. A Survey of Symbolic Execution Techniques, arXiv:1610.00502v3 [cs.SE] 2 May, 2018.

16. Cha, S.K., Avgerinos, T., Rebert, A., and Brumley, D. Unleashing Mayhem on Binary Code,SP’12 Proceedings of the 2012 IEEE Symposium on Security and Privacy, May 20 – 25, 2012, pp. 380–394.

17. Avgerinos, T., Cha, S.K., Rebert, A., Schwartz, E.J., Woo, M., and Brumley, D. Automatic exploit generation, Magazine Communications of the ACM, vol. 57, no. 2, February 2014, pp. 74–84.

18. MacIntyre, B., Gandy, M., Dow, S., and Bolter, J.D. DART: a toolkit for rapid design exploration of augmented reality experiences, UIST’04 Proceedings of the 17th annual ACM symposium on User interface software and technology, Santa Fe, NM, USA, October 24 –27, 2004, pp. 197–206.

19. Koushik, Sen K., Marinov, D., and Agha, G. CUTE: A Concolic Unit Testing Engine for C, ESEC/FSE-13 Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, Lisbon, Portugal, September 05–09, 2005, pp. 263–272.

20. Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., and Engler, D.R. EXE: Automatically Generating Inputs of Death, Journal ACM Transactions on Information and System Security (TISSEC), vol. 12, no. 2, December 2008, Article No. 10.

21. Godefroid, P., Levin, M.Y., and Molnar, D. Automated whitebox fuzz testing, Proceedings of 16th Annual Network & Distributed System Security Symposium, The Catamaran Resort Hotel and Spa, San Diego, CA, USA, 8–11 February, 2008, pp. 151–166.

22. Cadar, C., Dunbar, D., and Engler, D. KLEE: unassisted and automatic generation of highcoverage tests for complex systems programs, OSDI’08 Proceedings of the 8th USENIX conference on Operating systems design and implementation, San Diego, California, December 08–10, 2008, pp. 209–224.

23. Chipounov, V., Kuznetsov, V., and Candea, G. S2E: a platform for in-vivo multi-path analysis of software systems, ASPLOS XVI Proceedings of the sixteenth international conference on Architectural support for programming languages and operating systems, Newport Beach, California, USA, March 05–11, 2011, pp. 265–278.

24. Taneja, K., Xie, T., Tillmann, N., de Halleux, J., and Schulte, W. Guided Path Exploration for Regression Test Generation, Proceeding ISSTA’11 Proceedings of the 2011 International Symposium on Software Testing and Analysis, Toronto, Ontario, Canada, July 17–21, 2011, pp. 1–11.

25. Yang, G., Person, S., Rungta, N., and Khurshid, S. Directed Incremental Symbolic Execution, PLDI’11 Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, San Jose, California, USA, June 04–08, 2011, pp. 504–515.

26. Zamfir, C. and Candea, G. Execution Synthesis: A Technique for Automated Software Debugging, EuroSys ’10 Proceedings of the 5th European conference on Computer systems, Paris, France, April 13–16, 2010, pp. 321–334.

27. Ma, K-K., Phang, K.Y., Foster, J.S., and Hicks, M. Directed symbolic execution, SAS’11 Proceedings of the 18th international conference on Static analysis, Venice, Italy, September 14–16, 2011, pp. 95–111.

28. Parvez, R., Ward, P.A.S., and Ganesh, V. Combining Static Analysis and Targeted Symbolic Execution for Scalable Bug-finding in Application Binaries, CASCON’16 Proceedings of the 26th Annual International Conference on Computer Science and Software Engineering, Toronto, Ontario, Canada, October 31–November 02, 2016, pp. 116–127.

29. Borodin A. E. Mezhprotsedurnyj kontekstno-chuvstvitel'nyj staticheskij analiz dlya poiska oshibok v iskhodnom kode programm na yazykakh Si i Si++ // Dissertatsiya na soiskanie uchenoj stepeni kandidata fiziko-matematicheskikh nauk, Moskva, 2016, 137 s.

30. Gerasimov A.Yu. Obzor podkhodov k uluchsheniyu kachestva rezul'tatov staticheskogo analiza programm // Trudy Instituta sistemnogo programmirovaniya RAN, t. 29, vyp. 3, 2017, str. 75–98.

31. Gerasimov A.Yu., Kruglov L.V., Ermakov M.K., Vartanov S.P. Podkhod k opredeleniyu dostizhimosti programmnykh defektov, obnaruzhennykh metodom staticheskogo analiza, pri pomoschi dinamicheskogo simvol'nogo ispolneniya // Trudy Instituta sistemnogo programmirovaniya RAN, t. 29, vyp. 5, 2017, str. 111–134.

32. Gerasimov A.Yu. Ob ogranicheniyakh metoda klassifikatsii defektov v programmakh, najdennykh metodami staticheskogo analiza programm pri pomoschi dinamicheskogo simvol'nogo ispolneniya // Trudy 60-j Vserossijskoj nauchnoj konferentsii MFTI. 20–26 noyabrya 2017 g. Prikladnaya matematika i inormatika. M.: MFTI, 2017. 320 s.

33. Isaev I.K., Sidorov D.V. Primenenie dinamicheskogo analiza dlya generatsii vkhodnykh dannykh, demonstriruyuschikh kriticheskie oshibki i uyazvimosti v programmakh // Programmirovanie, № 4, 2010, str. 1–16.

34. Fedotov A.N., Kaushan V.V., Gajsaryan S.S., Kurmangaleev Sh.F. Postroenie predikatov bezopasnosti dlya nekotorykh tipov programmnykh defektov // Trudy Instituta sistemnogo programmirovaniya RAN, t. 29, vyp. 6, 2017, str. 151–162.

35. Li, M., Chen, Y., Wang, L., and Xu, G. Dynamically Validating Static Memory Leak Warnings, ISSTA 2013 Proceedings of the 2013 International Symposium on Software Testing and Analysis, Lugano, Switzerland, July 15–20, 2013, pp. 112–122.

36. Xu, R-G., Godefroid, P., and Majumdar, R. Testing for buffer overflows with length abstracton, ISSTA’08 Proceedings of the 2008 international symposium on Software testing and analysis, Seattle, WA, USA, July 20–24, 2008, pp. 27–38.

37. Fortify Analysis Software. https://software.microfocus.com/enus/ solutions/applicationsecurity? jumpid=va_912rzvtnd7/

38. Burnim, J. and Sen, K. Heuristics for Scalable Dynamic Test Generation, ASE’08 Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, September 15–19, 2008, pp. 443–446.

39. Cui H., Hu G., Wu J., and Yang J. Verifying Systems Rules Using Rule-Directed Symbolic Execution, ASPLOS’13 Proceedings of the eighteenth international conference on Architectural support for programming languages and operating systems, Houston, Texas, USA, March 16–20, 2013, pp. 329–342.

40. Neugschwandtner, M., Comparetti, P.M., Haller, I., and Bos, H. The BORG: Nanoprobing Binaries for Buffer Overreads, Proceeding CODASPY ’15 Proceedings of the 5th ACM Conference on Data and Application Security and Privacy, San Antonio, Texas, USA, March 02–04, 2015, pp. 87–97.

41. Ivannikov V.P., Belevantsev A.A., Borodin A.E., Ignat'ev V.N., Zhurikhin D.M., Avetisyan A.I., Leonov M.I. Staticheskij analizator Svace dlya poiska defektov v iskhodnom kode programm // Trudy Instituta sistemnogo programmirovaniya RAN, t. 26, vyp. 1, 2014, str. 231–250.

42. Gerasimov, A., Vartanov, S., Ermakov, M., Kruglov, L., Kutz, D., Novikov, A., and Asryan, S. Anxiety: A Dynamic Symbolic Execution Framework, Proceedings of 2017 Ivannikov ISPRAS Open Conference (ISPRAS), Moscow, Russian Federation, November 30 – December 1, 2017, pp. 16–22.

43. Schwartz, E.J., Thanassis, A.T., and Brumley D. All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask), SP’10 Proceedings of the 2010 IEEE Symposium on Security and Privacy, The Claremont Resort, Oakland, CA, USA, May 16–19, 2010, pp. 317–331.

44. Ge, X., Taneja, K., Xie, T., and Tillmann, N. DyTa: Dynamic Symbolic Execution Guided with Static Verification Results, ICSE’11 Proceedings of the 33rd International Conference on Software Engineering, Waikiki, Honolulu, HI, USA, May 21–28, 2011, pp. 992–994.

45. Chebaro, O., Kosmatov, N., Giorgetti, A., and Julliand, J. The sante tool: value analysis, program slicing and test generation for C program debugging, TAP’11 Proceedings of the 5th international conference on Tests and proofs, Zurich, Switzerland, June 30 –July 01, 2011, pp. 78–83.

46. Cuoq, P., Signoles, J., Baudin, P., Bonichon, R., Canet, G., Correnson, L., Monate, B., Prevosto, V., and Puccetti, A. Experience report: Ocaml for an industrial-strength static analysis framework, ICFP ’09 Proceedings of the 14th ACM SIGPLAN international conference on Functional programming, Edinburgh, Scotland, August 31 – September 02, 2009, pp. 281–286.

47. Williams, N., Marre, B., Mouy, P., and Roger, M. PathCrawler: automatic generation of path tests by combining static and dynamic analysis, EDCC’05 Proceedings of the 5th European conference on Dependable Computing, Budapest, Hungary, April 20–22, 2005, pp. 281–292.

Система Orphus

Loading...
Up