Лаборатория языковых инструментов
Символьное исполнение первого и второго порядка
Символьное исполнение (symbolic execution) - это метод анализа программ, основанный на решении задачи выполнимости формул в теориях (satisfiability modulo theories), в котором программа исполняется с символьными переменными вместо конкретных значений, а результатом исполнения являются формулы над этими символьными переменными. Символьное исполнение имеет множество применений, включая поиск ошибок и уязвимостей, генерацию тестов, верификацию, и т.д. В первой части доклада будут описаны проблемы традиционного символьного исполнения и некоторые алгоритмические и инженерные подходы к их решению. Во второй части доклада будет представлено расширение символьного исполнения для логики второго порядка, которое позволяет решать более сложные задачи, такие как автоматическое исправление ошибок и моделирование среды исполнения.
Материалы к докладу:
- Cristian Cadar, Daniel Dunbar, Dawson Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs // OSDI 2008
- Edward J. Schwartz, Thanassis Avgerinos, David Brumley. All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask) // S&P 2010
- Sergey Mechtaev, Alberto Griggio, Alessandro Cimatti, Abhik Roychoudhury. Symbolic Execution with Existential Second-Order Constraints // FSE 2018
Докладчик: Сергей Мечтаев, University College of London