Preview

Труды Института системного программирования РАН

Расширенный поиск

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

https://doi.org/10.15514/ISPRAS-2022-34(4)-4

Полный текст:

Аннотация

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

Об авторах

Александр Владимирович МИСОНИЖНИК
Санкт-Петербургский государственный университет
Россия

Получил степень магистра в области информационных технологий в Санкт-Петербургском государственном университете в 2021 году



Алексей Александрович БАБУШКИН
Санкт-Петербургский государственный университет
Россия

Получил степень бакалавра в области математики и компьютерных наук в Санкт-Петербургском государственном университете в 2022 году



Сергей Антонович МОРОЗОВ
Национальный исследовательский университет “Высшая школа экономики”
Россия

Студент 3 курса бакалавриата “Прикладная математика и информатика”



Юрий Олегович КОСТЮКОВ
Санкт-Петербургский государственный университет
Россия

Аспирант кафедры системного программирования 



Дмитрий Александрович МОРДВИНОВ
Санкт-Петербургский государственный университет
Россия

Кандидат физ.-мат. наук, доцент кафедры системного программирования



Дмитрий Владимирович КОЗНОВ
Санкт-Петербургский государственный университет
Россия

Доктор технических наук, профессор кафедры системного программирования



Список литературы

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.


Рецензия

Для цитирования:


МИСОНИЖНИК А.В., БАБУШКИН А.А., МОРОЗОВ С.А., КОСТЮКОВ Ю.О., МОРДВИНОВ Д.А., КОЗНОВ Д.В. Автоматическое тестирование LLVM-программ со сложными входными структурами данных. Труды Института системного программирования РАН. 2022;34(4):49-62. https://doi.org/10.15514/ISPRAS-2022-34(4)-4

For citation:


MISONIZHNIK A.V., BABUSHKIN A.A., MOROZOV S.A., KOSTYUKOV Yu.O., MORDVINOV D.A., KOZNOV D.V. Automated testing of LLVM programs with complex input data structures. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2022;34(4):49-62. (In Russ.) https://doi.org/10.15514/ISPRAS-2022-34(4)-4



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)