Яковлев В. М. Алгебраїчні методи виявлення вразливостей в бінарному коді

Досліджуються можливості підвищення ефективності застосування символьних методів у задачах кібербезпеки, зокрема, в задачі пошуку вразливостей у бінарному коді. Пропонується підхід, що грунтується на теорії інсерційного моделювання та алгебрі поведінок. Визначається семантика моделі програми та семантика мови програмування низького рівня на прикладі мови Ассемблера Intel х86. Розглядається формалізація поведінки моделі шляхом побудови системи поведінкових рівнянь, а також формалізація опису вразливостей коду у вигляді спеціальних шаблонів у термінах алгебри поведінок. Пропонується методика і технологія створення таких шаблонів. Представлено алгоритм приведення систем рівнянь алгебри поведінок до канонічної форми, доведено його коректність та складність. Цей алгоритм покладено в основу алгоритму алгебраїчного співставлення, доведено досяжність вразливості в моделі програми. Розроблено алгоритм лінійного алгебраїчного співставлення, який, у поєднанні з алгоритмами символьного моделювання, значно підвищує ефективність пошуку вразливостей у бінарному коді за рахунок звуження простору пошуку і обмеження його «підозрілими» поведінками. Доведено, що цей алгоритм має лінійну складність. Показано процедуру отримання визиску (екстлойту) на основі отриманих поведінок і умов, що ведуть до вразливості. Представлено реалізацію алгоритму алгебраїчного співставлення у прототипі програмної системи пошуку вразливостей. Розглянуто шляхи можливого застосування представленої технології для пошуку нештатних входів у програмах (бекдорів).