Подход к определению достижимости программных дефектов, обнаруженных методом статического анализа, при помощи динамического символьного исполнения

Автор: Герасимов А.Ю., Круглов Л.В., Ермаков М.К., Вартанов С.П.

Журнал: Труды Института системного программирования РАН @trudy-isp-ran

Статья в выпуске: 5 т.29, 2017 года.

Бесплатный доступ

Среди методов анализа программ на наличие дефектов выделяют методы статического и динамического анализа. В данной статье мы предлагаем комбинированный подход, заключающийся в применении динамического символьного исполнения для определения достижимости дефектов, найденных при помощи статического анализа. Предлагаемый подход является развитием ранее предложенного подхода определения достижимости определенной инструкции в программе методами динамического символьного исполнения, примененном последовательно для нескольких точек в программе, включающих точки инициализации дефекта, условные переходы в трассе дефекта и точку реализации дефекта. С начала производится статический анализ исполняемого кода программы с целью выделения путей исполнения, которые приводят к точке инициализации дефекта. Далее производится вычисление входных данных, приводящих к точке инициализации дефекта методом динамического символьного исполнения и прохождения базовых блоков, лежащих на трассе дефекта, включая точку реализации дефекта. Выбор наиболее перспективного пути для исполнения программы производится при помощи метрики минимального расстояния от пути исполнения на предыдущей итерации до следующей точки на трассе дефекта. Метрика вычисляется на основе путей в графе вызовов в программе, расширенного графом потока управления функций на путях исполнения, приводящих к реализации дефектов. Предлагаемый подход был проверен на нескольких программах с открытым исходным кодом из комплекта утилит командной строки операционной системы Debian Linux. В результате экспериментальной проверки было подтверждена возможность применения данного подхода к классификации дефектов, найденных при помощи статического анализа программ. Также, были обнаружены некоторые ограничения, препятствующие внедрению данного подхода в промышленные инструменты анализа. Одним из направлений дальнейших исследований может быть выбрано исследование подходов к снятию этих ограничений.

Еще

Статический анализ программ, динамический анализ программ

Короткий адрес: https://sciup.org/14916468

IDR: 14916468   |   DOI: 10.15514/ISPRAS-2017-29(5)-7

Список литературы Подход к определению достижимости программных дефектов, обнаруженных методом статического анализа, при помощи динамического символьного исполнения

  • Vogelsang A., Fehnker A., Huuck R., Reif W. Software Metrics in Static Program Analysis. ICFEM'10 Proceedings of the 12th International Conference on Formal Engineering Methods and Software Engineering, Shanghai, Shina, November 17-19, 2010, pp. 485-500
  • Kim Y., Kim Y., Kim T., Lee G., Jang Y., Kim M. Automated unit testing of large industrial embedded software using concolic testing. ACE'13 Proceedings of the 28yh IEEE/ACM International Conference on Automated Software Engineering, Silicaon Valley, CA, USA, November 11-15, 2013, pp. 519-528
  • Xie Y., Chou A., Engler D. ARCHER: Using Symbolic, Path-Sensitive Analysis to Detect Memory Access Errors. ESEC/FSE-11 Proceedings of the 9th European Software Engineering Conference held jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering, Helsinki, Finland, September 01-05, 2003, pp. 327-336
  • Bessey A., Block K., Chelf B, Chow A., Fulton B., Hallem S., Henri-Gros C., Kamsky A., McPeak S., Engler D. A few billion lines of code later: using static analysis to find bugs in the real world. Communications od ACM, vol. 53, issue 2, February 2010, pp. 66-75
  • Ivannikov V.P., Belevantsev A.A., Borodin A.E., Ignat'ev V.N., Zhurikhin D.M., Avetisyan A.I., Leonov M.I. Static analyzer Svace for finding of defects in program source code. Trudy ISP RAN/Proc. ISP RAS, vol. 26, issue 1, 2014, pp. 231-250 DOI: 10.15514/ISPRAS-2014-26(1)-7
  • Engler D., Chelf B., Chou A., Hallen S. Checking system rules using system-specific, programmer-written compiler extensions. OSDI’00 Proceedings of the 4th conference on Symposium on Operating System Design and Implementation, vol. 4, article No.1, San-Diego, CA, USA, October 22-25, 2000
  • Johnson B., Song Y., Murphy-Hill E., Bowdidge R., Why don’t software developers use static analysis tools to find bugs? ICSE’13 Proceedings of the 2013 International conference on Software Engineering. San Francisco, CA, USA, May 18-26, 2013
  • Christakis M., Müller P., Wüstholz An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzers. VMCAI’15 International Workshop on Verification, Model Checking and Abstract Interpretation, Springer, 2015, pp. 336-354
  • Livshits B., Sridharan M., Smaragdakis Y., Lhoták O., Amaral J.N., Chang B.-Y. E., Guyer S.Z., Khedker U.P., Møhler A., Vardoulakis D. In defence of soundness: a manifesto. Communications of ACM, vol. 58, no. 2, February 2015
  • Cadar C., Dunbar D., Endger D. KLEE: unassisted and automatic generation of high-coverage tests for complex systems. OSDI’08 Proceedings of the 8th USENIX conference on Operating Systems Design and Implementation, San Diego, CA, USA, December 08-10, 2008, pp. 209-224
  • Averginos T., Cha S.K., Revert A., Schwartz E.J., Woo M., Brumley D. Automatic Exploit Generation. Communications of the ACM, volume 57, issue 2, February 2014, pp. 74-84
  • Chipunov V., Kuznetsov V., Candea G. The S2E Platform: Design, Implementation, and Applications. ACM Transactions on Computer Systems (TOCS) -Special Issue APLOS 2011, article no. 2, volume 30, issue 1, February 2012
  • Manevich R., Sridharan M., Adams S., Das M., Yang Z. PSE: explaining program failures via post-mortem static analysis. SIGSOFT’04/FSE-12 Proceedings of the 12th ACM SIGSOFT 12th International Symposium on Foundations of Software Engineering, Newport Beach, NY, USA, 2004, pp. 63-72
  • Song D., Brumley D., Yin H., Caballero J., Jager I., Kang M.G., Liang Z., Newsome J., Poosankam P., Saxena P. BitBlaze: a New Approach to Computer Security via Binary Analysis. ICISS’08 Proceedings of the 4th international Conference on Information Systems Security, Hydarabad, India, December 16-20, 2008, pp. 1-25
  • Sen K., Marinov D., 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
  • King J.C. Symbolic Execution and Program Testing. Communications of the ACM, volume 19, issue 7, 1976, pp. 385-394
  • Cadar C., Ganesh V., Pawlowski P., Dill D.L., Engler D.R. EXE: automatically generating inputs of death. CCS’06 Proceedings of the 13th ACM Conference on Computer and Communications Security, Alexandria, Virginia, USA, October 30 -November 03, 2006, pp. 322-335
  • Schwartz E.J., Averginos T., Brumley D. All You Ever Wanted to Know About Dynamic Tait Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask). SP’10 Proceedings of the 2010 IEEE Symposium on Security and Privacy, Oakland, CA, USA, May 16-19, 2010, pp. 317-331
  • Csallner C., Smaragdakis Y. Check’N’Crash: combining static checking and testing. ICSE’05 Proceedings of the 27th international conference on software engineering, St. Louis, MO, USA, May 15-21, 2005, pp. 422-431
  • Chebaro O., Kosmatov N., Giorgetti A., Julliand J. Programs slicing enhances a verification technique combining static and dynamic analysis. SAC’12 Proceedings of the 27th Annual ACM Symposium of Applied Computing, Trento, Italy, March 26-30, 2012, pp. 1284-1291
  • Kim T., Park J., Kulinda I., Jang Y. Concolic Testing Framework for Industrial Embedded Software. APSEC’14 Proceedings of the 2014 21st Asia-Pacific Software Engineering Conference, volume 2, Jeju, South Korea, December 01-04, 2014, pp. 7-10
  • Hanna A., Ling H.Z., Yang X., Debbabi M. A synergy between static and dynamic analysis or the detection of software security vulnerabilities. OTM’09 Proceedings of the Confederated International Congress, CoopIS, DOA, IS and ADBASE 2009 on the Move to Meaningful Internet Systems: part II. Vilamoura, Portugal, November 01-06, 2009, pp. 815-832
  • Csallner C, Smaragdakis Y. DSD-Crasher: a hybrid analysis tool for bug finding. IISTA’06 Proceedings of the 2006 International Symposium on Software Testing and Analysis. Portland, Maine, USA, July 17-20, 2006, pp. 245-254
  • Artho C, BIere A. Combined Static and Dynamic Analysis. Electronic Notes in Theoretical Computer Science (ENTCS), volume 131, May, 2005, pp. 3-14
  • Chebaro o., Kostomarov N., Giorgetti A., Julliand J. Combining static analysis and test generation for C program debugging. TAP’10 Proceedings of the 4th International Conference on Tests and Proofs. Málaga, Spain, July 01-02, 2010, pp. 94-100
  • Schütte J., Fedler R., Tetze D. ConDroid: targeted dynamic analysis of Android Applications. AINA’15 Proceedings of IEEE 26th international Conference on Advanced Information Networking and Applications, Gwangui, South Korea, March 24-27, 2015
  • Ge X., Taneja K., Xie T., 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, Mau 21-28, 2011, pp. 992-994
  • Gerasimov A.Y., Kruglov L.V. Input data generation for reaching specific function in program by iterative dynamic analysis method. Trudy ISP RAN/Proc. ISP RAS, vol, 28, issue 5, 2016, pp. 159-174 DOI: 10.15514/ISPRAS-2016-28(5)-10
  • Stallman R. M. Using the GNU Compiler Collection: a GNU Manual for GCC Version 4.3.3. Free Software Foundation Inc., May, 2004
  • Isaev I.K., Sidorov D.V. The use of dynamic analysis for generation of input data that demonstrates critical bugs and vulnerabilities in programs. Programming and Computer Software, 2010, vol. 36, No. 4, pp. 225-236 DOI: 10.1134/S0361768810040055
  • GNU binutils http://www.gnu.org/software/binutils, accessed 01.11.2017
Еще
Статья научная