Автоматическое тестирование LLVM-программ со сложными входными структурами данных

Символьное исполнение является известным подходом для автоматической генерации регрессионных тестов и поиска ошибок/уязвимостей в программах. Данная работа посвящена созданию практичного метода к символьному исполнению LLVM-программ, пригодного для работы со сложными входными структурами данных. Метод основан на известной идее ленивой инициализации, позволяющей избавить пользователя от необходимости вручную создавать ограничения на входные структуры данных и полностью автоматизировать процесс символьного исполнения программы. Предлагается два улучшения ленивой инициализации для сегментированной символьной моделей памяти – использование временных меток и информации о типах. Предложенный метод реализован в символьной виртуальной машине KLEE для платформы LLVM и протестирован на реальных C-структурах данных — списках, биномиальных кучах, AVL-деревьях, красно-чёрных деревьях, двоичных деревьях и борах (префиксных деревьях).

1. Korel B., Al-Yami A.M. Automated Regression Test Generation. ACM SIGSOFT Software Engineering Notes, vol. 23, issue 2, 1998, pp. 143-152.

2. Cadar C., Sen K. Symbolic execution for software testing: three decades later. Communications of the ACM, vol. 56, issue 2, 2013, pp. 82-90.

3. Baldoni R., Coppa E. et al. A survey of symbolic execution techniques. ACM Computing Surveys (CSUR), vol. 51, issue 3, 2018, pp. 1-39.

4. Barrett C., Tinelli C. Satisfiability Modulo Theories. In Handbook of Model Checking, Springer, 2018, pp. 305-343.

5. Volanschi N., Lawall J. The impact of generic data structures: decoding the role of lists in the linux kernel. In Proc. of the 35th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2020, pp. 103-114.

6. Corbet J. Trees II: red-black trees. URL: https://lwn.net/Articles/184495/, 2006.

7. Bacthu N., Banerjee A. et al. Dynamic and compressed trie for use in route lookup. United States Patent Application 20180212876, URL: https://www.freepatentsonline.com/20180212876.pdf, 2018.

8. Braione P., Denaro G. et al. Combining symbolic execution and search-based testing for programs with complex heap inputs. In Proc. of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2017), 2017, pp. 90-101.

9. Galeotti J.P., Rosner N. et al. Analysis of invariants for efficient bounded verification. In Proc. of the 19th International Symposium on Software Testing and Analysis (ISSTA '10), 2010, pp. 25-36.

10. Khurshid S., Puasuareanu C.S., Visser W. Generalized symbolic execution for model checking and testing. In Proc. of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2003, pp. 553-568.

11. Kapus T., Cadar C.A segmented memory model for symbolic execution. In Proc. of the 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2019, pp. 774-784.

12. Cadar C., Dunbar D., Engler D. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proc. of the 8th USENIX Conference on Operating Systems Design and Implementation, 2008, pp. 209-224.

13. ISO/IEC 9899:201x - N1570 - Programming languages – C. URL: https://web.cs.dal.ca/~vlado/pl/C_Standard_2011-n1570.pdf.

14. Cadar C., Dunbar D. KLEE. URL: https://github.com/klee/klee/tree/v2.3, 2022.

15. de Moura L., Bjorner N. Z3: An Efficient SMT Solver. Lecture Notes in Computer Science, vol. 4963, 2008, pp. 337-340.

16. Gough B., Stallman R. M. An Introduction to GCC for the GNU Compilers gcc and g++. Network Theory Ltd, 2004, 144 p.

17. Geldenhuys J., Aguirre N. et al. Bounded Lazy Initialization. Lecture Notes in Computer Science, vol. 7871, 2013, pp. 229-243.

18. Puasuareanu C. S., Rungta N. Symbolic PathFinder: symbolic execution of Java bytecode. In Proc. of the IEEE/ACM International Conference on Automated Software Engineering, 2010, pp. 179-180.

19. Rosner N., Geldenhuys J. et al. BLISS: improved symbolic execution by bounded lazy initialization with SAT support. IEEE Transactions on Software Engineering, vol. 41, issue 7, 2015, pp. 639-660.

20. Braione P., Denaro G., Pezze M. Symbolic Execution of Programs with Heap Inputs. In Proc. of the 10th Joint Meeting on Foundations of Software Engineering, 2015, pp. 602-613.

21. Ramos D. A., Engler D. Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In Proc. of the 24th USENIX Security Symposium (USENIX Security 15), 2015, pp. 49-64.

22. Rutledge R., Orso A. PG-KLEE: Trading Soundness for Coverage. In Proc. of the IEEE/ACM 42nd International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), 2020, pp. 65-68.