Использование алгебраических моделей программ для обнаружения метаморфного вредоносного кода

Полиморфные и метаморфные вирусы – это наиболее сложные вредоносные программы, сталкиваясь с которыми, антивирусные сканеры могут испытывать значительные затруднения. Каждый раз, когда подобные вирусы заражают новые приложения или воспроизводят себя, они полностью изменяют свой код, чтобы избежать обнаружения; эта техника называется “обфускация”. Указанное свойство создаёт серьёзную проблему для антивирусного программного обеспечения, которое полагается на классические методы обнаружения вредоносного кода. Это связано с тем, что в коде полиморфных и метаморфных вирусов нет постоянной последовательности инструкций, которую антивирус мог быть рассматривать в качестве идентификатора для поиска. В конечном итоге единственной характеристикой, которая остаётся неизменной для всех поколений одного и того же вируса, является их поведение (семантика). По-видимому, единственный способ достоверно определить наличие метаморфного вредоносного кода – это поиск по шаблону, который имеет ту же семантику (эквивалентное поведение), что и некоторая репрезентативная выборка вируса. Таким образом, обнаружение метаморфного вредоносного кода тесно связано с проблемой проверки эквивалентности для программ. В данной работе рассматривается новая теоретико-автоматная модель, которая может послужить основой для разработки антивирусов. Представленный подход основан на технике проверки эквивалентности в алгебраических моделях последовательных программ. Алгебраическая модель программ – это абстрактная модель вычислений, где программы рассматриваются как конечный автомат, работающий со структурами Крипке. Модели такого типа позволяют рассматривать только те характеристики операторов программы, которые широко используются для обфускирующих преобразований. В настоящей работе приводится обзор (включая последние результаты) методов решения проблемы проверки эквивалентности для различных алгебраических моделей программ и оценка устойчивости некоторых обфускирующих преобразований, которые обычно используются метаморфными вирусами.