Направленное динамическое символьное исполнение программ для подтверждения ошибок в программах

Необходимость применения методов автоматического анализа программ с целью обнаружения ошибок, являющихся источником уязвимостей безопасности программы, в последнее время не вызывает сомнений у специалистов в области сертификации и обеспечения качества программ. Межгосударственный стандарт разработки безопасного программного обеспечения (ПО) предъявляет требование применения инструментов статического анализа исходного кода программ, как одной из меробеспечения качества ПО на стадии его разработки, а также применения методов динамического анализа и фаззинг-тестирования кода программ на этапе квалификационного тестирования. Фундаментальные ограничения методов автоматического анализа и тестирования программ не позволяют проводить одновременно исчерпывающий и точный анализ программ на наличие программных ошибок. В связи с этим в последнее время проводятся научные исследования, направленные на уменьшение влияния фундаментальных ограничений различных методов на качество и производительность методов автоматического обнаружения ошибок в программном обеспечении. В данной статье рассматривается подход к совмещению методов статического анализа исходного кода программ и динамического символьного исполнения программ с целью повышения эффективности обнаружения ошибок в программах.

Ключевые слова

Получено

26.10.2018

Дата публикации

28.10.2018

Кол-во символов

1286

Цитировать Скачать pdf Для скачивания PDF необходимо авторизоваться

ГОСТ	Герасимов А. Ю. Направленное динамическое символьное исполнение программ для подтверждения ошибок в программах // Программирование – 2018. – Выпуск 5 C. 31-42 [Электронный ресурс]. URL: http://ras.jes.su/progr/s207987840000461-6-1 (дата обращения: 30.04.2024). DOI: 10.31857/S013234740001213-9
MLA	Gerasimov, A. "Directed dynamic symbolic execution of programs to confirm errors in programs." Programmirovanie 5 (2018):31-42. DOI: 10.31857/S013234740001213-9
APA	Gerasimov A. (2018). Directed dynamic symbolic execution of programs to confirm errors in programs. Programmirovanie (5), pp.31-42 DOI: 10.31857/S013234740001213-9

Размещенный ниже текст является ознакомительной версией и может не соответствовать печатной.

всего просмотров: 1153

Оценка читателей: голосов 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. ГОСТР 56939-2016 Защита информации. Разработка безопасного программного обеспечения. Общие требования. // Национальный стандарт Российской Федерации. Федеральное агентство по техническому регулированию и метрологии.

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. Белеванцев А.А. Многоуровневый статический анализ исходного кода для обеспечения качества программ // Диссертация на соискание ученой степени доктора физико-математических наук, Москва, 2017, 229 с.

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. Бородин А. Е. Межпроцедурный контекстно-чувствительный статический анализ для поиска ошибок в исходном коде программ на языках Си и Си++ // Диссертация на соискание ученой степени кандидата физико-математических наук, Москва, 2016, 137 с.

30. Герасимов А.Ю. Обзор подходов к улучшению качества результатов статического анализа программ // Труды Института системного программирования РАН, т. 29, вып. 3, 2017, стр. 75–98.

31. Герасимов А.Ю., Круглов Л.В., Ермаков М.К., Вартанов С.П. Подход к определению достижимости программных дефектов, обнаруженных методом статического анализа, при помощи динамического символьного исполнения // Труды Института системного программирования РАН, т. 29, вып. 5, 2017, стр. 111–134.

32. Герасимов А.Ю. Об ограничениях метода классификации дефектов в программах, найденных методами статического анализа программ при помощи динамического символьного исполнения // Труды 60-й Всероссийской научной конференции МФТИ. 20–26 ноября 2017 г. Прикладная математика и инорматика. М.: МФТИ, 2017. 320 с.

33. Исаев И.К., Сидоров Д.В. Применение динамического анализа для генерации входных данных, демонстрирующих критические ошибки и уязвимости в программах // Программирование, № 4, 2010, стр. 1–16.

34. Федотов А.Н., Каушан В.В., Гайсарян С.С., Курмангалеев Ш.Ф. Построение предикатов безопасности для некоторых типов программных дефектов // Труды Института системного программирования РАН, т. 29, вып. 6, 2017, стр. 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. Иванников В.П., Белеванцев А.А., Бородин А.Е., Игнатьев В.Н., Журихин Д.М., Аветисян А.И., Леонов М.И. Статический анализатор Svace для поиска дефектов в исходном коде программ // Труды Института системного программирования РАН, т. 26, вып. 1, 2014, стр. 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.