BC/NW 2025 № 1 (42):13.2
УСОВЕРШЕНСТВОВАННЫЙ
СИМВОЛЬНЫЙ ДИНАМИЧЕСКИЙ АНАЛИЗ МНОГОПОТОЧНЫХ ПРИЛОЖЕНИЙ С ПОМОЩЬЮ МОДИФИКАЦИИ
KLEE
Скоробогатов
Д.Г., Зайнутдинов М.М., Орлов Д.А., Хиль С.Ю.
Многопоточность, повышая производительность,
усложняет анализ кода.
Традиционные методы тестирования часто
не способны охватить все возможные взаимодействия между потоками, что приводит
к пропущенным ошибкам.
Инструмент анализа KLEE, основанный на
LLVM, широко используется для символьного анализа, однако его возможности ограничены
при работе с многопоточными приложениями [1].
В рамках данной работы представлена
модификация KLEE, разработанная для более эффективного анализа многопоточных
программ.
Модифицирован KLEE 2.2, обновив
устаревшие LLVM/Clang и исправив возникающие ошибки API. Были исправлены критические
ошибки управления памятью, выявленные с помощью AddressSanitizer, и внесены
существенные изменения в реализацию StackFrame, StackType, Thread и
ExecutionState для корректной работы с многопоточностью.
Модификация KLEE представляет собой значительный
шаг вперед в области символьного анализа многопоточных приложений.
Разработанные мной решения, включающие
реализацию глубокого копирования объектов, связанных с потоками,
централизованное управление памятью и улучшенную обработку списков потоков,
позволяют более эффективно обнаруживать скрытые ошибки и уязвимости в сложных
многопоточных программных системах, повышая надежность и безопасность
разрабатываемого программного обеспечения.
В будущем планируется разработать новые
методы оптимизации символьного
исполнения для повышения
производительности и масштабируемости.
Представленная работа открывает новые
перспективы для развития и применения символьного исполнения в анализе и
верификации многопоточных программ.
Литература
1.
А.Г. Зыков, И.В. Кочетков, В.И. Поляков. Применение системы KLEE для автоматизации
тестирования программ на языках C/C++. Научно-практический журнал “Программные
продукты и системы” — 14.06.2016 — С. 101–106.