RUS  ENG
Полная версия
ЖУРНАЛЫ // Труды института системного программирования РАН // Архив

Труды ИСП РАН, 2023, том 35, выпуск 3, страницы 91–108 (Mi tisp789)

“Symcrete” memory model with lazy initialization and objects of symbolic sizes in KLEE

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

S. A. Morozova, A. V. Misonizhnikb, D. A. Mordvinovc, D. V. Koznovc, D. A. Ivanovd

a National Research University Higher School of Economics
b IT Solutions Inc.
c Saint Petersburg State University
d Huawei Technologies Co., Ltd.

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

Ключевые слова: символьное исполнение, анализ программного обеспечения, ленивая инициализация, симкретное исполнение, smt-решатели

Язык публикации: английский

DOI: 10.15514/ISPRAS-2023-35(3)-7



© МИАН, 2024