Симкретная модель памяти с ленивой инициализацией и объектами символьного размера в символьной виртуальной машине KLEE

Динамическое символьное выполнение – хорошо известный метод тестирования приложений. Он вводит понятие символьной переменной – данных программы, не имеющих конкретного значения в момент объявления, – и использует их для систематического изучения путей выполнения в анализируемой программе. Однако не Санкт-Петербургский государственный университет каждое значение может быть легко смоделировано как символическое: например, некоторые значения могут принимать ограниченное число значений или иметь сложные инварианты, которые достаточно сложно смоделировать с использованием существующих логических теорий несмотря на то, что это не является проблемой для конкретных вычислений. В этой статье мы предлагаем реализацию инфраструктуры для работы с такими “трудно моделируемыми” значениями. Мы используем подход, известный как симкретное исполнение, и реализуем его надежную и масштабируемую версию в хорошо известном движке символьного выполнения KLEE. Мы используем эту инфраструктуру для поддержки символьного исполнения программ на языке LLVM со сложными структурами входных данных и входными буферами неопределенных размеров.

1. Cristian Cadar and Koushik Sen. “Symbolic execution for software testing: three decades later”. In: Communications of the ACM 56.2 (2013), pp. 82–90.

2. Clark Barrett and Cesare Tinelli. “Satisfiability modulo theories”. In: Handbook of model checking. Springer, 2018, pp. 305–343.

3. Leonardo de Moura and Nikolaj Bjørner. “Z3: An efficient SMT solver”. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer. 2008, pp. 337–340.

4. Haniel Barbosa et al. “cvc5: A versatile and industrial-strength SMT solver”. In: Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part I. Springer. 2022, pp. 415–442.

5. Aina Niemetz and Mathias Preiner. “Bitwuzla at the SMT-COMP 2020”. In: arXiv preprint arXiv:2006.01621 (2020).

6. Corina S Pa˘sa˘reanu, Neha Rungta, and Willem Visser. “Symbolic execution with mixed concrete-symbolic solving”. In: Proceedings of the 2011 International Symposium on Software Testing and Analysis. 2011, pp. 34–44.

7. Awanish Pandey, Phani Raj Goutham Kotcharlakota, and Subhajit Roy. “Deferred concretization in symbolic execution via fuzzing”. In: Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. 2019, pp. 228–238.

8. Misonijnik A. et al. “Automated testing of LLVM programs with complex input data structures”. In: Proceedings of ISP RAS 34.4 (2022), pp. 49–62.

9. Sarfraz Khurshid, Corina S Pa˘sa˘reanu, and Willem Visser. “Generalized symbolic execution for model checking and testing”. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer. 2003, pp. 553–568.

10. Cristian Cadar and Daniel Dunbar. KLEE. Version 2.3. 2022. URL: https://github.com/klee/klee/tree/v2.3.

11. Dirk Beyer. “Advances in Automatic Software Testing: Test-Comp 2022.” In: FASE. 2022, pp. 321–335.

12. Leonardo de Moura and Nikolaj Bjørner. Z3 4.12.1. Version 4.12.1. 2023. URL: https://github.com/Z3Prover/ z3/releases/tag/z3-4.12.1.

13. Brian Gough and Richard M Stallman. “An Introduction to GCC for the GNU Compilers gcc and g++”. In: Network Theory Ltd 258 (2004).

14. Peter Dinges and Gul Agha. “Targeted test input generation using symbolic-concrete backward execution”. In: Proceedings of the 29th ACM/IEEE international conference on Automated software engineering. 2014, pp. 31–36.

15. Koushik Sen, Darko Marinov, and Gul Agha. “CUTE: A concolic unit testing engine for C”. In: ACM SIGSOFT Software Engineering Notes 30.5 (2005), pp. 263–272.

16. David Trabish, Shachar Itzhaky, and Noam Rinetzky. “A bounded symbolic-size model for symbolic execution”. In: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 2021, pp. 1190–1201.

17. Michael Sima´ˇcek. “Symbolic-size memory allocation support for Klee”. PhD thesis. Masarykova univerzita, Fakulta informatiky, 2018.