Алгебраїчний підхід у формалізації вразливостей в бінарному коді
Пошук вразливостей у програмному забезпеченні є на поточний момент актуальним завданням та джерелом наукових викликів. Описаний у статті алгебраїчний підхід покликаний збільшити ефективність та достовірність алгоритмів пошуку. Запропоновано засоби формального опису поведінки бінарного коду та вразли...
Збережено в:
| Опубліковано в: : | Control systems & computers |
|---|---|
| Дата: | 2019 |
| Автори: | , , |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
2019
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/181087 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Алгебраїчний підхід у формалізації вразливостей в бінарному коді / О.О. Летичевський, Я.В. Гринюк, В.М. Яковлев // Control systems & computers. — 2019. — № 6. — С. 5-20. — Бібліогр.: 9 назв. — укр. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-181087 |
|---|---|
| record_format |
dspace |
| spelling |
Летичевський, О.О. Гринюк, Я.В. Яковлев, В.М. 2021-10-31T19:15:09Z 2021-10-31T19:15:09Z 2019 Алгебраїчний підхід у формалізації вразливостей в бінарному коді / О.О. Летичевський, Я.В. Гринюк, В.М. Яковлев // Control systems & computers. — 2019. — № 6. — С. 5-20. — Бібліогр.: 9 назв. — укр. 2706-8145 DOI https://doi.org/10.15407/usim.2019.06.005 https://nasplib.isofts.kiev.ua/handle/123456789/181087 004.05, 004.4[2+9], 004.94, 519.7 Пошук вразливостей у програмному забезпеченні є на поточний момент актуальним завданням та джерелом наукових викликів. Описаний у статті алгебраїчний підхід покликаний збільшити ефективність та достовірність алгоритмів пошуку. Запропоновано засоби формального опису поведінки бінарного коду та вразливостей у термінах алгебри поведінок, а також двоступеневий загальний алгоритм пошуку, описано прототип відповідної програмної системи. Цель статьи. Хотя символьное моделирование может быть эффективно использовано для поиска уязвимостей в программном коде, соответствующие программные инструменты работают весьма медленно. Кроме того, проблема достижимости при символьном выполнении программ является неразрешимой в общем случае. В статье предлагается формализация представления двоичного кода и уязвимостей на основе алгебры поведений, а также подход, позволяющий ускорить поиск уязвимостей и сократить область символьного моделирования. Алгебра поведений используется для представления поведения как двоичного кода, так и уязвимости. Однако, хотя получение представления бинарного кода в терминах алгебры поведений может быть автоматизировано, создание описания уязвимостей требует разработки корректной и эффективной методологии. При использовании представлений в терминах алгебры поведений задача поиска уязвимостей может быть решена в два этапа — относительно быстрого алгебраического сопоставления и собственно символьного моделирования на основе данных, полученных на этапе сопоставления. Методы. Разработка описаний уязвимостей в терминах алгебры поведений и алгоритма алгебраического сопоставления позволяет ускорить алгоритмы поиска уязвимостей в двоичном программном коде. Результаты. Предложена методика разработки описаний уязвимостей двоичного кода в терминах алгебры поведений. Разработан алгоритм алгебраического сопоставления, включенный в научный прототип, который успешно использован для проверки известных уязвимостей в нескольких программах. Purpose. Although the symbolic modeling could be effectively used for the code vulnerabilities detection, the relevant software tools are very slow. Also, the reachability problem during the symbolic program execution is unresolvable in the common case. In the article, the formalization of representation of binary code and vulnerabilities based on the behavior algebra, and an approach that allow speeding up the vulnerabilities search, and reducing the area of the symbolic modeling are proposed. The behavior algebra used for the representation of the formal binary code behavior, as well as for describing the vulnerabilities behavior. However, while the representation of the binary code in the terms of behavior algebra could be automated, creation of the vulnerabilities description requires development of the correct and effective methodology. Using the behavior algebra representation, the task of vulnerabilities detection can be solved in two steps – relatively fast algebraic matching, and the symbolic modeling itself, based on the data provided by the algebraic matcher. Methods. By the development of the vulnerabilities description in the terms of behavior algebra, and the algebraic matching algorithm the speed of detection of vulnerabilities in the binary code can be increased. Results. The methodology of development of the vulnerabilities description in the terms of the behavior algebra has been proposed. The algebraic matching algorithm has been implemented in the scientific prototype system, which has been successfully used to check several programs for the known vulnerabilities. uk Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України Control systems & computers Fundamental Problems in Computer Science Алгебраїчний підхід у формалізації вразливостей в бінарному коді Алгебраический подход к формализации уязвимостей в бинарном коде Algebraic Approach to Vulnerabilities Formalization in the Binary Code Article published earlier |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| title |
Алгебраїчний підхід у формалізації вразливостей в бінарному коді |
| spellingShingle |
Алгебраїчний підхід у формалізації вразливостей в бінарному коді Летичевський, О.О. Гринюк, Я.В. Яковлев, В.М. Fundamental Problems in Computer Science |
| title_short |
Алгебраїчний підхід у формалізації вразливостей в бінарному коді |
| title_full |
Алгебраїчний підхід у формалізації вразливостей в бінарному коді |
| title_fullStr |
Алгебраїчний підхід у формалізації вразливостей в бінарному коді |
| title_full_unstemmed |
Алгебраїчний підхід у формалізації вразливостей в бінарному коді |
| title_sort |
алгебраїчний підхід у формалізації вразливостей в бінарному коді |
| author |
Летичевський, О.О. Гринюк, Я.В. Яковлев, В.М. |
| author_facet |
Летичевський, О.О. Гринюк, Я.В. Яковлев, В.М. |
| topic |
Fundamental Problems in Computer Science |
| topic_facet |
Fundamental Problems in Computer Science |
| publishDate |
2019 |
| language |
Ukrainian |
| container_title |
Control systems & computers |
| publisher |
Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України |
| format |
Article |
| title_alt |
Алгебраический подход к формализации уязвимостей в бинарном коде Algebraic Approach to Vulnerabilities Formalization in the Binary Code |
| description |
Пошук вразливостей у програмному забезпеченні є на поточний момент актуальним завданням та джерелом наукових викликів. Описаний у статті алгебраїчний підхід покликаний збільшити ефективність та достовірність алгоритмів пошуку. Запропоновано засоби формального опису поведінки бінарного коду та вразливостей у термінах алгебри поведінок, а також двоступеневий загальний алгоритм пошуку, описано прототип відповідної програмної системи.
Цель статьи. Хотя символьное моделирование может быть эффективно использовано для поиска уязвимостей в программном коде, соответствующие программные инструменты работают весьма медленно. Кроме того, проблема достижимости при символьном выполнении программ является неразрешимой в общем случае. В статье предлагается формализация представления двоичного кода и уязвимостей на основе алгебры поведений, а также подход, позволяющий ускорить поиск уязвимостей и сократить область символьного моделирования. Алгебра поведений используется для представления поведения как двоичного кода, так и уязвимости. Однако, хотя получение представления бинарного кода в терминах алгебры поведений может быть автоматизировано, создание описания уязвимостей требует разработки корректной и эффективной методологии. При использовании представлений в терминах алгебры поведений задача поиска уязвимостей может быть решена в два этапа — относительно быстрого алгебраического сопоставления и собственно символьного моделирования на основе данных, полученных на этапе сопоставления. Методы. Разработка описаний уязвимостей в терминах алгебры поведений и алгоритма алгебраического сопоставления позволяет ускорить алгоритмы поиска уязвимостей в двоичном программном коде. Результаты. Предложена методика разработки описаний уязвимостей двоичного кода в терминах алгебры поведений. Разработан алгоритм алгебраического сопоставления, включенный в научный прототип, который успешно использован для проверки известных уязвимостей в нескольких программах.
Purpose. Although the symbolic modeling could be effectively used for the code vulnerabilities detection, the relevant software tools are very slow. Also, the reachability problem during the symbolic program execution is unresolvable in the common case. In the article, the formalization of representation of binary code and vulnerabilities based on the behavior algebra, and an approach that allow speeding up the vulnerabilities search, and reducing the area of the symbolic modeling are proposed. The behavior algebra used for the representation of the formal binary code behavior, as well as for describing the vulnerabilities behavior. However, while the representation of the binary code in the terms of behavior algebra could be automated, creation of the vulnerabilities description requires development of the correct and effective methodology. Using the behavior algebra representation, the task of vulnerabilities detection can be solved in two steps – relatively fast algebraic matching, and the symbolic modeling itself, based on the data provided by the algebraic matcher. Methods. By the development of the vulnerabilities description in the terms of behavior algebra, and the algebraic matching algorithm the speed of detection of vulnerabilities in the binary code can be increased. Results. The methodology of development of the vulnerabilities description in the terms of the behavior algebra has been proposed. The algebraic matching algorithm has been implemented in the scientific prototype system, which has been successfully used to check several programs for the known vulnerabilities.
|
| issn |
2706-8145 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/181087 |
| citation_txt |
Алгебраїчний підхід у формалізації вразливостей в бінарному коді / О.О. Летичевський, Я.В. Гринюк, В.М. Яковлев // Control systems & computers. — 2019. — № 6. — С. 5-20. — Бібліогр.: 9 назв. — укр. |
| work_keys_str_mv |
AT letičevsʹkiioo algebraíčniipídhíduformalízacíívrazlivosteivbínarnomukodí AT grinûkâv algebraíčniipídhíduformalízacíívrazlivosteivbínarnomukodí AT âkovlevvm algebraíčniipídhíduformalízacíívrazlivosteivbínarnomukodí AT letičevsʹkiioo algebraičeskiipodhodkformalizaciiuâzvimosteivbinarnomkode AT grinûkâv algebraičeskiipodhodkformalizaciiuâzvimosteivbinarnomkode AT âkovlevvm algebraičeskiipodhodkformalizaciiuâzvimosteivbinarnomkode AT letičevsʹkiioo algebraicapproachtovulnerabilitiesformalizationinthebinarycode AT grinûkâv algebraicapproachtovulnerabilitiesformalizationinthebinarycode AT âkovlevvm algebraicapproachtovulnerabilitiesformalizationinthebinarycode |
| first_indexed |
2025-12-07T18:48:32Z |
| last_indexed |
2025-12-07T18:48:32Z |
| _version_ |
1850876428469403648 |