Формальная модель исполняемого кода программного обеспечения на основе графа исполнения для решения задачи бинарного морфинга

Рассматривается задача построения формальной модели исполняемого кода программного обеспечения, предназначенной для строгого математического описания процессов динамического преобразования (морфинга) программ в процессе их выполнения. Актуальность исследования обусловлена необходимостью разработки математического аппарата, обеспечивающего формальное обоснование методов изменения структуры исполняемого кода без нарушения функциональной корректности программ. Целью работы является разработка архитектурно-независимой формальной модели исполняемого кода, позволяющей определить инвариантные свойства программ при выполнении операций морфинга и установить условия сохранения их наблюдаемого поведения. Предложенная модель объединяет статическую и динамическую составляющие исполняемого кода. Статическая часть описывает программу как совокупность базовых блоков, объединенных графом потока управления с конфигурацией размещения кода в адресном пространстве и множеством управляющих ссылок между блоками. Динамическая составляющая включает формальное описание трассы исполнения программы, последовательности состояний вычислительной системы и наблюдаемого поведения, определяемого исключительно внешне наблюдаемыми результатами выполнения. Практическая значимость исследования заключается в создании единого формального аппарата, пригодного для последующего доказательства корректности алгоритмов морфинга исполняемого кода, разработки методов их верификации и анализа защищенности программных систем. Полученные результаты формируют теоретическую основу дальнейших исследований в области динамической трансформации исполняемого кода и разработки перспективных технологий защиты программного обеспечения.