Вычисление входных данных для достижения определенной функции в программе методом итеративного динамического анализа

Динамическое символьное исполнение - это хорошо известная техника, применяемая для решения различных задач анализа программ: генерация входных данных для увеличения тестового покрытия программы, для эксплуатации уязвимостей и т.д. В то же время значительное падение производительности при динамическом символьном исполнении также является хорошо известной, в общем случае NP-сложной проблемой в связи с экспоненциальным взрывом количества анализируемых путей и решением задачи SAT/SMT при разрешении предиката пути. Применение метода грубой силы при попытке анализа всех достижимых путей в программе, как правило, не имеет смысла в условиях жесткого ограничения времени решения поставленных задач. Поэтому применяются различные методы и эвристики для увеличения производительности анализа и сокращения анализируемого пространства. Мы представляем подход совмещения статического анализа исполняемого кода, основанного на использовании библиотеки binutils, и метода динамического символьного исполнения, основанного на инструменте итеративного динамического анализа Avalanche, для направленной генерации входных данных программы с целью достижения заранее определенной функции в программе. На первом шаге предлагаемого подхода строится усеченный граф вызовов программы, который содержит только те функции, вызов которых в конечном счете приводит к вызову заранее определенной функции. Далее мы дополняем граф вызовов графом потока управления внутри функций, включенных в усеченный граф вызовов. С использованием усеченного графа потока управления программы, который содержит только вызовы и условные переходы, приводящие в конечном итоге к вызову заранее определенной функции, вычисляется метрика наиболее перспективного пути для проведения дальнейшего анализа. Предложенный подход позволил значительно (до двенадцати раз для некоторых реальных программ) сократить время достижения заранее определенной функции по сравнению с методом грубой силы.

статический анализ, динамический анализ, генерация входных данных

1. Myers G. J., Badgett T., Sandler C. The Art of Software Testing. Third Edition. John Wiley & Sons, Inc., Hoboken, New Jersey, 2012, 240 p.

2. Ю.Г. Карпов. MODEL CHECKING. Верификация параллельных и распределенных систем. СПб:БХВ-Петербург. 2010

3. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking, М.:МЦНМО, 2002

4. Kyung-Suk Lhee, S.J. Chapin. Buffer Overflow and Format String Overflow Vulnerabilities. Software-Practice & Experience - Special Issue: Security Software, Volume 33 Issue 5, 25 April 2003, pp. 423-460

5. Ari Takanen, Jared D. Demott, Charles Miller. Fuzzing for Software Security Testing and Quality Assurance. Artech House, 2008

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

7. Cadar C., Dunbar D., Engler. D. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008), December 8-10, 2008, San Diego, CA, USA

8. Chipounov V., Kuznetsov V., Candea G. The S2E Platform: Design, Implementation, and Applications. ACM Transactions on Computer Systems (TOCS) Special issue: Best papers of ASPLOS, February 2012.

9. В.В. Каушан, Ю.В. Маркин, В.А. Падарян, А.Ю. Тихонов. Методы поиска ошибок в бинарном коде. Препринты Института системного программирования РАН, препринт 24, 2013 г.

10. L. de Moura, N. Bjørner. Z3: an Efficient SMT Solver. Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008

11. Ganesh V. Decision Procedures for Bit-Vectors, Arrays and Integers. (PhD. Thesis) Computer Science Department, Stanford University, Stanford, CA, U.S., Sept 2007

12. Исаев И.К., Сидоров Д.В., Герасимов А.Ю., Ермаков М.К. Avalanche: Применение динамического анализа для автоматического обнаружения ошибок в программах использующих сетевые сокеты. Труды ИСП РАН, том 21, 2011 г., стр. 55-70

13. I. Johnson. Formal Verification with SMT Solvers: Why and How. ACL2 Theorem Proving Seminar at the University of Texas, Autin, 2009

14. Новикова Н.М. Основы оптимизации. Москва. 1998. 17-22 c.

15. S.A. Cook. The complexity of theorem-proving procedures. Proceedings of the third annual ACM symposium on Theory of computing, New York, USA, NY,1971, pp 151-158

16. М.К. Ермаков, А.Ю. Герасимов. Avalanche: применение параллельного и распределенного динамического анализа программ для ускорения поиска дефектов и уязвимостей. Труды ИСП РАН, том 25, 2013 г., стр. 29-38. DOI: 10.15514/ISPRAS-2013-25-2

17. С.П. Вартанов, Д.В. Сидоров. Оптимизация задачи проверки выполнимости булевских ограничений при помощи кэширования промежуточных результатов. Труды ИСП РАН, том 22, 2012 г., стр. 281-292. DOI: 10.15514/ISPRAS-2012-22-16

18. Thanassis Agerinos, Sang Kil Cha, Brent Lim Tze Hao, David Broomley. AEG: Automatic Exploit Generation. Proceedings of the Network and Distributed Security Symposyum, Carnegie Mellon University, 2011

19. GNU Binutils [HTML] (http://www.gnu.org/software/binutils/)

20. Schütte J., Fedler R., Titze D. ConDroid: Targeted Dynamic Analysis of Android Applications. Advanced Information Networking and Applications (AINA), IEEE, Gwangui, 2105, DOI:10.1109/AINA.2015.238

21. Wong M., Lie D. IntelliDroid: A Targeted Input Generator for the Dynamic Analysis of Android Malware. In Proceedings of the 2016 Network and Distributed System Security Symposium (NDSS), Feb 2016.