Алгебраїчні шаблони вразливостей бінарного коду
Пошук вразливостей у програмному забезпеченні є на поточний час актуальним завданням та джерелом наукових викликів. Описаний у статті алгебраїчний підхід покликаний збільшити ефективність та достовірність алгоритмів пошуку. Запропоновано засоби формального опису поведінки бінарного коду та вразливос...
Збережено в:
| Дата: | 2020 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут програмних систем НАН України
2020
|
| Назва видання: | Проблеми програмування |
| Теми: | |
| Онлайн доступ: | http://dspace.nbuv.gov.ua/handle/123456789/180422 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Алгебраїчні шаблони вразливостей бінарного код / В.М. Яковлев // Проблеми програмування. — 2020. — № 1. — С. 47-54. — Бібліогр.: 11 назв. — укр. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
irk-123456789-180422 |
|---|---|
| record_format |
dspace |
| spelling |
irk-123456789-1804222021-09-25T01:26:21Z Алгебраїчні шаблони вразливостей бінарного коду Яковлев, В.М. Методи та засоби комп'ютерного моделювання Пошук вразливостей у програмному забезпеченні є на поточний час актуальним завданням та джерелом наукових викликів. Описаний у статті алгебраїчний підхід покликаний збільшити ефективність та достовірність алгоритмів пошуку. Запропоновано засоби формального опису поведінки бінарного коду та вразливостей в термінах алгебри поведінок, а методику створення шаблонів вразливостей бінарного коду. Одной из актуальных проблем в ИТ-индустрии является обнаружение уязвимостей в программном обеспечении. В последнее десятилетие стали весьма популярными и многообещающими подходы к решению данной проблемы, основанные на символьных методах. Данная статья описывает подход к поиску уязвимостей в двоичном коде, основанный на формальных методах символьного моделирования и алгебраического сопоставления. В данной статье предлагается формализация представления двоичного кода и уязвимостей на основе алгебры поведений, а также методика формирования шаблонов уязвимостей. Такие шаблоны могут быть использованы не только для описания, но и для поиска уязвимостей в произвольном двоичном коде. Алгебра поведений используется для представления поведения как двоичного кода, так и уязвимости. Однако, хотя получение представления бинарного кода в терминах алгебры поведений может быть автоматизировано, создание описания уязвимостей требует разработки корректной и эффективной методологии. При использовании представлений в терминах алгебры поведений задача поиска уязвимостей может быть решена в два этапа – относительно быстрого алгебраического сопоставления и собственно символьного моделирования на основе данных, полученных на этапе сопоставления. Разработка описаний уязвимостей в терминах алгебры поведений и алгоритма алгебраического сопоставления позволяет ускорить алгоритмы поиска уязвимостей в двоичном программном коде. Предложена методика разработки описаний уязвимостей двоичного кода в терминах алгебры поведений. Преимущество алгебраического подхода состоит в том что уязвимости в коде могут быть определены более точно, а описание уязвимости в терминах алгебры поведений позволяет учесть ее различные варианты. Кроме того, эксперименты с прототипом показали, что «двухуровневая» система поиска уязвимостей работает быстрее, чем «чистая» система символьного моделирования: вначале выполняется быстрый этап сопоставления, а затем медленный этап символьного моделирования на данных, полученных на предыдущем этапе. Detection of software systems’ vulnerabilities is an actual problem in the IT industry nowadays. The approaches to the solution of this problem, based on the symbolic methods, became very popular and promising during the last decade. The article describes an approach to the vulnerabilities detection in the binary code, based on the formal methods of symbolic modeling and algebraic matching. In the article, the formalization of representation of binary code and vulnerabilities based on the behavior algebra, and the method of creation of formal patterns of vulnerabilities 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. 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. The methodology of development of the vulnerabilities description in the terms of the behavior algebra has been proposed. The advantage of the algebraic approach is that the code vulnerabilities can be found more precisely, and the vulnerability description in the terms of behavior algebra can take in account different possible kinds of it. Also, the experiments with the implementation prototype shown that the “two-level” vulnerability detection system is faster than “pure” symbolic modeling: the fast matching step is executed first, and the slow modeling step is executed next on the results, provided by the matching step. 2020 Article Алгебраїчні шаблони вразливостей бінарного код / В.М. Яковлев // Проблеми програмування. — 2020. — № 1. — С. 47-54. — Бібліогр.: 11 назв. — укр. 1727-4907 DOI: https://doi.org/10.15407/pp2020.01.047 http://dspace.nbuv.gov.ua/handle/123456789/180422 004.05, 004.4[2+9], 004.94, 519.7 uk Проблеми програмування Інститут програмних систем НАН України |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| language |
Ukrainian |
| topic |
Методи та засоби комп'ютерного моделювання Методи та засоби комп'ютерного моделювання |
| spellingShingle |
Методи та засоби комп'ютерного моделювання Методи та засоби комп'ютерного моделювання Яковлев, В.М. Алгебраїчні шаблони вразливостей бінарного коду Проблеми програмування |
| description |
Пошук вразливостей у програмному забезпеченні є на поточний час актуальним завданням та джерелом наукових викликів. Описаний у статті алгебраїчний підхід покликаний збільшити ефективність та достовірність алгоритмів пошуку. Запропоновано засоби формального опису поведінки бінарного коду та вразливостей в термінах алгебри поведінок, а методику створення шаблонів вразливостей бінарного коду. |
| format |
Article |
| author |
Яковлев, В.М. |
| author_facet |
Яковлев, В.М. |
| author_sort |
Яковлев, В.М. |
| title |
Алгебраїчні шаблони вразливостей бінарного коду |
| title_short |
Алгебраїчні шаблони вразливостей бінарного коду |
| title_full |
Алгебраїчні шаблони вразливостей бінарного коду |
| title_fullStr |
Алгебраїчні шаблони вразливостей бінарного коду |
| title_full_unstemmed |
Алгебраїчні шаблони вразливостей бінарного коду |
| title_sort |
алгебраїчні шаблони вразливостей бінарного коду |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2020 |
| topic_facet |
Методи та засоби комп'ютерного моделювання |
| url |
http://dspace.nbuv.gov.ua/handle/123456789/180422 |
| citation_txt |
Алгебраїчні шаблони вразливостей бінарного код / В.М. Яковлев // Проблеми програмування. — 2020. — № 1. — С. 47-54. — Бібліогр.: 11 назв. — укр. |
| series |
Проблеми програмування |
| work_keys_str_mv |
AT âkovlevvm algebraíčníšablonivrazlivostejbínarnogokodu |
| first_indexed |
2025-07-15T20:24:18Z |
| last_indexed |
2025-07-15T20:24:18Z |
| _version_ |
1837745900914475008 |
| fulltext |
Методи та засоби комп’ютерного моделювання
© В.М. Яковлев, 2020
ISSN 1727-4907. Проблеми програмування. 2020. № 1 47
УДК 004.05, 004.4[2+9], 004.94, 519.7 https://doi.org/10.15407/pp2020.01.047
В.М. Яковлев
АЛГЕБРАЇЧНІ ШАБЛОНИ ВРАЗЛИВОСТЕЙ
БІНАРНОГО КОДУ
Пошук вразливостей у програмному забезпеченні є на поточний час актуальним завданням та джере-
лом наукових викликів. Описаний у статті алгебраїчний підхід покликаний збільшити ефективність
та достовірність алгоритмів пошуку. Запропоновано засоби формального опису поведінки бінарного
коду та вразливостей в термінах алгебри поведінок, а методику створення шаблонів вразливостей б і-
нарного коду.
Ключові слова: вразливості програмного забезпечення, символьне моделювання, алгебраїчне зістав-
лення, алгебра поведінок.
Вступ
Однією з найважливіших сучасних
проблем в галузі інформаційних техноло-
гій є виявлення вразливостей в бінарному
коді. Проблема настільки серйозна, що
дослідження в цьому напрямку організо-
вуються й фінансуються на рівні держав-
них структур. Зокрема, в США в 2018 році
на базі Національного Директорату з Захи-
сту та Програмах (National Protection and
Programs Directorate, NPPD) створено Аге-
нтство з Кібербезпеки та Інфраструктури
(Cybersecurity and Infrastructure Security
Agency, CISA), наділене широкими права-
ми щодо захисту програмних систем та
комп’ютерних мереж. У 2016 році створе-
но Європейську Організацію з Кібербезпе-
ки (European Cyber Security Organisation,
ECSO), а в квітні 2019 року Рада Європи
схвалила Акт з Кібербезпеки (Cybersecurity
Act), який, зокрема, встановлює загально-
європейські правила сертифікації комп’ю-
терних систем та створює загальноєвро-
пейське Агентство з Кібербезпеки на базі
існуючого Загальноєвропейського Агентс-
тва з Мережевої та Інформаційної безпеки
(European Union Agency for Network and
Information Security, ENISA).
Американське агентство DARPA в
2016 році започаткувало спеціальний кон-
курс, Cyber Grand Challenge [1], що заохо-
чує дослідницькі організації до створення
систем для автоматизованого, масштабо-
ваного та швидкісного програмного забез-
печення для виявлення вразливостей та
кіберінфекцій. Всі троє переможців конку-
рсу 2016 року в своїх продуктах застосо-
вували алгебраїчний підхід, яких дозволяє
більш ефективно реалізувати алгоритми
виявлення вразливостей.
Переможець конкурсу Mayhem [2],
розроблений командою ForAllSecure з Піт-
сбургу, включає інструменти, які викорис-
товують символічне виконання, зокрема,
комбінований (concolic) підхід, що підви-
щує ефективність обходу програмних
шляхів. Крім того, індексована пам’ять та
увід користувача розглядаються як симво-
льні значення, що забезпечило більш пов-
не покриття програмного середовища.
Команда Xandra TECHx [3] з Ітаки,
штат Нью-Йорк, та Шарлоттсвіля посіла
друге місце у загальному заліку в фіналь-
ній події. Тим не менш, ця команда була
першою у вирішенні проблеми виявлення
та запобігання визискам (exploit) за раху-
нок використання символьного інструмен-
ту пошуку.
Система Mechanical Phish [4], роз-
роблена командою «Шелфи» з Санта-
Барбари, Каліфорнія, також використовує
символьне виконання з розмиванням вхід-
них даних.
Також існує багато інших подібних
інструментів, які працюють з бінарним
кодом, використовують символьні техніки
моделювання. До них належать S2E [5] та
інші системи з обмеженим символьним
виконанням, такі як CUTE [6] та Клі [7].
В даній статті пропонується засто-
сування алгебраїчного підходу до вияв-
лення вразливостей за допомогою алгебра-
їчних моделей та виявлення поведінок, які
https://doi.org/10.15407/pp2020.01.047
https://www.cisa.gov/
https://www.cisa.gov/
Методи та засоби комп’ютерного моделювання
48
б відповідали певним зразкам у бінарному
коді. Ця методика базується на алгебраїч-
ній системі програмування (APS), і покла-
дена в основу прототипу алгебраїчної сис-
теми виявлення вразливих місць у бінар-
ному коді з використанням алгебраїчного
методу відповідності.
1. Алгебра поведінок
Вразливість розглядається як пове-
дінка системи, яка потенційно дозволяє
зловмиснику виконувати такі дії, як, на-
приклад, пошкодження або крадіжка да-
них. Для конкретизації такої поведінки
використовується певний алгебраїчний
формалізм. Прикладом такого формалізму
є алгебра поведінок, представлена Деві-
дом Гілбертом та Олександром Летичевсь-
ким [8].
Розглянемо множини поведінок та
дій. Кожна поведінка складається з певних
дій та іншої поведінки. Алгебра поведінок
– це двосортна алгебра над множинами
поведінок та дії з наступними операціями:
- операція префіксингу a.B озна-
чає, що перед поведінкою B виконується
дія a;
- операція недетермінованого ви-
бору поведінок u + v встановлює альтер-
нативну поведінку.
Алгебра включає три термінальні
константи: успішне припинення Δ, тупик 0
та невідома поведінка ⊥. Алгебра поведін-
ки також збагачена двома операціями: па-
ралельні (||) та послідовні (;) композиції
поведінок. Терм, створений з операцій ал-
гебри поведінки над поведінками та діями,
формує вираз алгебри поведінок. Будь-яка
поведінка може бути представлена як на-
бір рівнянь, які містять ім’я поведінки в
лівій частині та вираз алгебри поведінок у
правій. Наприклад, наведена далі поведін-
ка визначає поведінку програми, яка дру-
кує щось у циклі.
Program = initCycle.Cycle; Δ
Cycle = print.Cycle + endCycle
initCycle, endCycle та print – це дії, а
Program і Cycle – поведінки.
Всі дії об’єкта, для якого описуєть-
ся поведінка, передбачає зміну його стану,
що визначається як множина атрибутів,
представлена у вигляді типізованих змін-
них або функцій. Кожна дія також визна-
чається парою формальних виразів – пере-
думовою та постумовою дії. Семантика
цих виразів визначається складністю об'є-
кта, що формалізується. Наприклад, наве-
дена далі дія передбачає можливість зміни
стану об'єкта, визначеного атрибутами A і B:
Action(A, B) =
(A> B) && !(A == 0) ->
B = (B + 1) / A.
Семантика дії, яка представлена в
С-подібному синтаксисі, означає, що якщо
передумова (A > B) && !(A == 0)
справедлива для конкретного значення A і
B або підходить для символічних (довіль-
них) значень з A і B, тоді ми можемо змі-
нити атрибут B:
B = (В + 1) / А.
Дію можна параметризувати за ат-
рибутами, що згадуються в її передумові
дії. Для множини поведінок ми можемо
визначити іншу поведінку високого рівня,
яка міститиме усі інші поведінки.
Підстановка високорівневої поведі-
нки для дій дає набір послідовностей дій,
тобто різні сценарії зазначеної поведінки
високого рівня. Ця процедура називається
розгортанням поведінки. Набір формул
над атрибутами визначає об'єкт на кожно-
му кроці розгортання. Формули містять
символьні атрибути, а процес розгортання
називається символьним моделюванням.
2. Семантика бінарного коду
Розглянемо виконавчий модуль,
який складається з набору інструкцій про-
цесора, представлених у вигляді бінарного
коду. Дизасемблювавши бінарний код,
отримаємо набір асемблерний текст. У
подальшому розглядатимемо асемблер
Intel x86 [9]. Поведінка програми визнача-
ється послідовністю інструкцій, а різні сце-
нарії виконання генеруються за рахунок
зміни вхідних даних. У формальній моделі
кожна інструкція відповідає певній дії.
Потік управління програмою може
бути представлений виразами алгебри по-
Методи та засоби комп’ютерного моделювання
49
ведінки. У поведінковому виразі А = a.B,
a – позначає певну дію, яка відповідає
поточній інструкції, а B – представляє
поведінку решти програми, що виникає
після дії a. В інструкціях, що містять аль-
тернативи в контрольному потоці, потріб-
на операція “+”. Приклад поведінкових
виразів і відповідний код показані далі:
Параметризовані дії та імена пове-
дінок позначаються відповідно інструкці-
ям та адресам операторів в асемблерному
лістингу. Кожна дія моделі змінює її стан,
який визначається певною формулою в
атрибутному середовищі. Розглянемо
структуру такого середовища.
З урахуванням структури новітніх
процесорів Intel, середовище складається з
наступних компонентів:
- набору регістрів загального та
спеціального призначення. Деякі атрибути
ідентифікуються за іменами регістрів: ax,
al, bx, bl, .., eax, ebx,…, rax,
rbx,…, ebp, esp, rbp, rsp, rip;
- фізичної пам'яті, яку можна роз-
глядати як функцію Memory(addr), де
addr визначає адресу наявної пам'яті.
Семантика інструкції визначається
передумовою і відповідною зміною сере-
довища. Наприклад, якщо розглянути се-
мантику інструкції cjne A B z, то перед-
умова визначається значеннями операндів
інструкції, а поведінка описується диз'юн-
кцією:
Bx1 = cjne.Bz +!cjne.Bx2
Bx2 =…
Дії:
cjne(n,A,B) = !(A == B) ->
PI = PI+z+3; FLAG_C = (B > A)
!cjne(n,A,B) = (A == B) ->
PI = PI + 3;
Тобто, якщо два операнди рівні, пе-
реходимо до поведінки Bz, змінюємо вка-
зівник на значення z+3 та признаємо буле-
ве значення атрибуту FLAG_C. В іншому
випадку змінюємо вказівник на 3 та пере-
ходимо до наступної інструкції. Після від-
повідної трансляції набори поведінок та
дій можуть бути отримані з асемблерного
лістинга автоматично.
3. Алгебраїчні шаблони
вразливостей
Шаблон вразливості визначає пове-
дінку програми, що призводить до стану
вразливості. Треба розрізняти стан помил-
ки програми та стан вразливості, оскільки
останній, як правило, містить також дії, що
відповідають введенню в програму певних
даних, обробка яких призводить до «спра-
цювання» вразливості. Шаблон вразливос-
ті складається з виразів алгебри поведінки
та відповідних дій. Загальна форма моделі
вразливості – це поведінка:
VulnerabilityPattern = Input;
ProgramBehavior;
VulnerabilityPoint
Наведений шаблон складається з
трьох узагальнених поведінок.
Input – це поведінка програми, яка
представляє інструкції, що діють від зов-
нішнього середовища. Вона може включа-
ти введення даних з командного рядку,
зчитування файлів, отримання даних з ме-
режі тощо. Переважно, введення реалізу-
ється як системний виклик основного коду
операційної системи.
ProgramBehavior – це частина
програми, яка виконується між точками
введення даних та вразливості. В описі
поведінки може бути більше однієї такої
поведінки.
VulnerabilityPoint представляє
дії, які тягнуть за собою «спрацювання»
вразливості. Узагальнена поведінка охоп-
лює всі можливі сценарії або послідовності
інструкцій, що призводять до вразливості.
Це є найскладніша частина формалізації
Методи та засоби комп’ютерного моделювання
50
структури вразливості з огляду на необ-
хідність зібрати всі можливі сценарії. На-
приклад, копіювання пам'яті може бути
представлено декількома способами та,
відповідно, різними послідовностями ін-
струкцій. Одним із таких способів є копі-
ювання областей пам’яті в циклі.
writeMemory =
mov(1,
GeneralRegister,
MemoryOperand).
mov(2,
MemoryOperand,
GeneralRegister).
add(1,GeneralRegister,1).
add(2,GeneralRegister,1).
X3;
(writeMemory + Delta)
Така поведінка означає, що запис у
пам'ять виконується в циклі, і кінець пове-
дінки відповідає його завершенню. Пара-
метр GeneralRegister посилається будь-
який регістр загального призначення, а
MemoryOperand позначає вміст фізичної
пам'яті. X3 є довільною поведінкою.
Відповідні дії виглядають наступ-
ним чином:
mov(1,GeneralRegister,
MemoryOperand) = 1 ->
GenPurpose(x) &&
x = Memory(y),
mov(2 MemoryOperand,
GeneralRegister) = 1 ->
Memory(z) = x,
add(1, r, 1) = 1-> y = y + 1
add(2, r, 1) = 1-> z = z + 1
Цей простий приклад поведінки має
на увазі, що вміст фізичної пам'яті за адре-
сою y передається в регістр x і предикат
GenPurpose (x) дорівнює true або x ==
ax || x == bx || x == cx || x ==
dx для дії mov (1,…). Дія mov (2,…) пе-
редає вміст регістру x у фізичну пам'ять за
адресою z. У діях add (1,…) та add
(2,…) ми збільшуємо адреси, за якими ми
звертаємося до пам’яті. Змінна r означає,
що не має значення, де саме знаходяться
адреси, за якими ми звертаємося до облас-
тей пам’яті – в регістрі загального призна-
чення або в пам'яті. При розгортанні пове-
дінки враховуються лише необхідні нам
об’єкти, зазначені у виразах алгебри пове-
дінки.
Розглянемо декілька узагальнених
шаблонів вразливостей, пов’язаних з пере-
повненням буфера пам’яті, що є найбільш
розповсюдженою причиною вразливостей
програм.
Поведінка Input, що відповідає
введенню даних у програму, в загальній
формі виглядає як
Input=mov(i,
GeneralRegister,
MemoryAddr).
X1.
mov(j,
Memory(x),
GeneralRegister).
Input,
mov(i,
GeneralRegister,
MemoryAddr)=
1-> Dirty(GeneralRegister),
mov(j,Memory(x),GeneralRegister)=
Dirty(GeneralRegister) ->
Dirty(x) &
!Dirty(GeneralRegister)
В сучасних операційних системах
введення даних у програмний буфер здійс-
нюється шляхом копіювання в цей буфер
даних з системного буфера, представлено-
го прямою адресою MemoryAddr. Оскільки
в одноадресній архітектурі Intel будь-яке
копіювання має відбуватися через регістр
загального призначення, маємо дві дії, пе-
рша з яких копіює байт з системного бу-
фера в регістр, а друга – з регістра в лока-
льний програмний буфер за адресою x.
При цьому ми відмічаємо вміст ре-
гістра, і далі вміст локального буфера як
Dirty.
Треба зазначити, що наведена пове-
дінка Input відповідає найпростішому
варіанту реалізації введення даних, оскіль-
ки в розширеній множині інструкцій Intel
існують інструкції копіювання пам’ять-
пам’ять, наприклад, movs. Таким чином,
поведінка Input має бути доповнена ін-
Методи та засоби комп’ютерного моделювання
51
шими існуючими реалізаціями алгоритму
введення даних.
Тепер розглянемо розповсюджений
сценарій вразливості, пов’язаний з перепо-
вненням буфера, розташованого в області
стека. «Спрацювання» такої вразливості
може призвести до порушення роботи про-
грами, або, при певних умовах, до вико-
нання зловмисного коду.
StackVulnerability =
(mov(l,
Memory(s),
GeneralRegister).
Delta +
!mov(l,
Memory(s),
GeneralRegister)).
StackVulnerability,
Вказана поведінка означає, що з ре-
гістрів пам’ять у циклі пишеться у пам’ять,
яка може вміщувати експлойт.
mov(l, Memory(s),
GeneralRegister) =
Dirty(GeneralRegister) &
(s <= BP) -> 1,
mov(m, Memory(s),
GeneralRegister) =
!(m = l) &
Dirty(GeneralRegister)
-> Dirty(s),
mov(n, Memory(s),
GeneralRegister) =
!(n = l) & (Dirty(s) &
!Dirty(GeneralRegister))
-> !Dirty(s)
mov(m, GeneralRegister,
Memory(s)) =
!(m = l) & Dirty(s) ->
Dirty(GeneralRegister),
mov(n, GeneralRegister,
Memory(s))=
!(n = l) & (!Dirty(s) &
Dirty(GeneralRegister)) ->
!Dirty(GeneralRegister)
Наведена поведінка відповідає од-
ній з реалізацій процедури копіювання
буфера вводу в буфер, розташований у
стеку. «Спрацювання» вразливості відбу-
вається, коли для дії mov(l, Memory(s),
GeneralRegister) спрацьовує переду-
мова Dirty(GeneralRegister) &
(s<=BP), що є переповненням стеку.
Інший вірогідний сценарій вразли-
вості пов’язаний із зверненням до пам’яті,
розташованої поза межами буфера, розта-
шованого в області динамічної пам’яті, або
«купи».
HeapVulnerability = AllocHeap;V2;
AccessHeap,
Дві важливі частини поведінки опи-
сують виділення пам’яті в «купі» та звер-
нення до пам’яті в «купі» з метою читання
або запису.
Шаблон, що відповідає поведінці
виділення пам’яті, виглядає наступним
чином:
AllocHeap = mov(I,AX,y),
V3;
mov(j,AX,z),
mov(I,AX,y)=1->N=AX,
mov(j,AX,z) = 1->addr=AX;
Forall( a+N > j >= a,
Allocated(j) ),
Наведений шаблон описує операцію
виділення N байт пам’яті. Функція виді-
лення пам’яті приймає значення N як ар-
гумент, передаючи його через регістр AX.
Після звернення до менеджера пам’яті ад-
реса виділеної області повертається через
згаданий регістр. Одночасно, модель мар-
кує виділені комірки пам’яті як
Allocated. Нарешті,
AccessHeap=ReadHeap+WriteHeap,
ReadHeap=(mov(k,
GeneralRegister,
h).
Delta +
!mov(k,
GeneralRegister,
h)).
ReadHeap,
mov(k, GeneralRegister, h) =
Allocated(h) & (h >=N | h < 0)
-> 1
WriteHeap=(mov(l,
Memory(h),
GeneralRegister).
Delta +
!mov(l,
Методи та засоби комп’ютерного моделювання
52
Memory(h),
GeneralRegister)
).WriteHeap,
mov(l,
Memory(h),
GeneralRegister) =
Allocated(h) &
(h >= N | h < 0) -> 1,
Таким чином, наведені поведінки
«спрацьовують», коли операції читання
або запису звертаються до пам’яті поза
межами виділеного блоку.
Ще один варіант – поведінка, що
описує звернення до статичної пам’яті (зо-
внішні змінні), дещо відрізняється від на-
веденої для динамічної пам’яті. Нагадаємо,
такі блоки пам’яті існують в програмі
впродовж всього часу її роботи.
AccessStatic=ReadStatic+
WriteStatic,
ReadStatic=lea(x,
GeneralRegister,
offset).
V4;DoRead,
DoRead=(mov(y,GeneralRegister,s).
Delta +
!mov(y,GeneralRegister,s)
).DoRead,
WriteStatic=lea(x,
GeneralRegister,
offset).
V5;
mov(y,
GeneralRegister,
s),
lea(x,GeneralRegister,offset)=
1->Size(s)=offset,
mov(y,GeneralRegister,s)=
s>=Size(s) | s < 0 -> 1,
Як правило, передумовою звернен-
ня до блоку статичної пам’яті є налашту-
вання певного регістру на адресу цього
блоку, що здійснюється через інструкцію
lea(…), а подальші дії аналогічні тим, що
відбувається при зверненні до пам’яті ін-
ших типів.
Очевидно, наведені приклади шаб-
лонів вразливостей описують дані вразли-
вості лише частково, тому що існують інші
сценарії подібних дій. Більш того, існує
багато інших видів вразливостей, і ство-
рення відповідних шаблонів є предметом
подальших досліджень.
4. Алгебраїчне зіставлення
Процедура алгебраїчного зіставлен-
ня до певної міри схожа на традиційний
пошук відповідностей, що використову-
ється в антивірусних програмах. Тради-
ційні шаблони програмного коду містять
конкретні значення, які співставляються з
кодом, що перевіряється, тоді як алгебраї-
чне зіставлення передбачає вирішення або
доведення кожного кроку зіставлення. Ця
властивість алгебраїчного підходу дозво-
ляє охопити більше випадків вразливостей
та значно підвищує точність виявлення,
зменшуючи кількість випадків хибного
виявлення.
Алгебраїчне зіставлення виконуєть-
ся під час символьного моделювання біна-
рного коду. При зіставленні на рівні пове-
дінок на кожному кроці виявляється істин-
ність виразу Env && Prec, де Env – сим-
вольне середовище, а Prec- передумова
відповідної дії. У такому випадку викону-
ється формула постумови дії у середовищі
шаблона та в середовищі моделі програми.
Символьне моделювання виконується до
виявлення вразливостей або вичерпання
шляхів у просторі пошуку.
Висновки
Основна проблема алгебраїчного
підходу полягає у тому, що досяжність у
загальному випадку не визначається. Ти-
повими проблемами також є експоненцій-
ний вибух простору станів або можливих
програмних сценаріїв. Такі проблеми мо-
жуть вирішуватися за допомогою альтер-
нативних символьних методів, таких як
генерація інваріантів, апроксимація або
зворотне символьне моделювання. За до-
помогою налаштувань пошуку можливо
зменшити простір станів, наприклад, ви-
значити певне обмежене покриття рядків
коду. З іншого боку, таке звуження прос-
тору пошуку може спричинити до того, що
деякі вразливості буде пропущено.
Іншою проблемою є узагальнення
алгебраїчних шаблонів. Власне узагаль-
Методи та засоби комп’ютерного моделювання
53
нення засновується на аналізі великої кіль-
кості прикладів та визначенні загальних
рис можливих сценаріїв. Оскільки наразі
універсальна методика побудови та уза-
гальнення шаблонів відсутня, немає гаран-
тій того, що побудований шаблон охоплює
всі можливі сценарії.
Тим не менш, важлива перевага ал-
гебраїчного підходу полягає у тому, що
вразливості можуть бути виявлені набага-
то точніше порівняно з традиційними під-
ходами. Крім того, описи вразливостей
можуть охоплювати цілі сімейства можли-
вих сценаріїв виконання коду.
Ефективність виявлення вразливос-
тей може бути підвищена за рахунок реалі-
зації зіставлення на декількох рівнях, на-
приклад, на рівні тільки поведінок, що
може виконуватися досить швидко, і лише
по тому – на рівні моделювання поведінок
з доведенням досяжності на сильно звуже-
ному просторі пошуку.
З огляду на проведені численні екс-
перименти з робочим прототипом системи
алгебраїчного зіставлення на основі алгеб-
раїчної системи APS [10] згаданий підхід
довів свою перспективність, що обумов-
лює необхідність подальших досліджень.
Література
1. DARPA, “Cyber Grand Challenge.” [Online].
Available: https://www.
cybergrandchallenge.com/.
2. Cha S.K., Avgerinos T., Rebert A., Brumley
D., “Unleashing Mayhem on binary code,”
Proceedings. IEEE Symposium on Security
and Privacy. 2012. P. 380–394.
3. Nguyen-Tuong A., Melski D., Davidson J.W.,
Co M., Hawkins W., Hiser J.D., Morris D.,
Nguen D., and Rizzi E. “Xandra: An
autonomous cyber battle system for the Cyber
Grand Challenge,” IEEE Security & Privacy.
2008. Vol. 16. N. 2. P. 42–53.
4. Mechaphish, “Github repository.” [Online].
Available from:https://github. com/
mechaphish/mecha-docs.
5. Chipounov V., Kuznetsov V., Candea G.
“S2E: A platform for invivo multi-path
analysis of software systems.” Asplos. 2011.
Vol. 46. P. 1–14.
6. Sen K., Marinov D., Agha G., Sen K.,
Marinov D., Agha G. “CUTE: A concolic unit
testing engine for C.” 10th European Software
Engineering Conference and 13th ACM
SIGSOFT International Symposium on
Foundations of Software Engineering
(ESEC/FSE’05). 2005. Vol. 30. N 5. P. 263.
7. Cadar C., Dunbar D., Engler D.R. “KLEE:
Unassisted and automatic generation of high-
coverage tests for complex systems
programs,” Proceedings of the 8th USENIX
Conference on Operating Systems Design and
Implementation. 2008. P. 209–224.
8. Gilbert D., Letichevsky A. “Interaction of
agents and environments,” Recent trends in
algebraic development technique, LNCS 1827
(D. Bert and C. Choppy, eds.), Springer-
Verlag, 1999.
9. Intel 64 and IA-32. “Architectures software
developer’s manual.” Intel Corporation.
1997–2016.
10. Algebraic Programming System, APS,
[Online]. www.apsystem.org.ua
References
1. DARPA, “Cyber Grand Challenge.” [Online].
Available: https://www.
cybergrandchallenge.com/.
2. Cha S.K., Avgerinos T., Rebert A., Brumley
D., “Unleashing Mayhem on binary code,”
Proceedings. IEEE Symposium on Security
and Privacy. 2012. P. 380–394.
3. Nguyen-Tuong A., Melski D., Davidson J.W.,
Co M., Hawkins W., Hiser J.D., Morris D.,
Nguen D., and Rizzi E. “Xandra: An
autonomous cyber battle system for the Cyber
Grand Challenge,” IEEE Security & Privacy.
2008. Vol. 16. N. 2. P. 42–53.
4. Mechaphish, “Github repository.” [Online].
5. Available from:https://github. com/
mechaphish/mecha-docs.
6. Chipounov V., Kuznetsov V., Candea G.
“S2E: A platform for invivo multi-path
analysis of software systems.” Asplos. 2011.
Vol. 46. P. 1–14.
7. Sen K., Marinov D., Agha G., Sen K.,
Marinov D., Agha G. “CUTE: A concolic unit
testing engine for C.” 10th European Software
Engineering Conference and 13th ACM
SIGSOFT International Symposium on
https://github/
http://www.apsystem.org.ua/
https://github/
Методи та засоби комп’ютерного моделювання
54
Foundations of Software Engineering
(ESEC/FSE’05). 2005. Vol. 30. N. 5. P. 263.
8. Cadar C., Dunbar D., Engler D.R. “KLEE:
Unassisted and automatic generation of high-
coverage tests for complex systems
programs,” Proceedings of the 8th USENIX
Conference on Operating Systems Design and
Implementation. 2008. P. 209–224.
9. Gilbert D., Letichevsky A. “Interaction of
agents and environments,” Recent trends in
algebraic development technique, LNCS 1827
(D. Bert and C. Choppy, eds.), Springer-
Verlag, 1999.
10. Intel 64 and IA-32. “Architectures software
developer’s manual.” Intel Corporation.
1997–2016.
11. Algebraic Programming System, APS,
[Online]. www.apsystem.org.ua
Одержано 30.01.2020
Про автора:
Яковлев Віктор Михайлович,
провідний математик.
Кількість наукових публікацій в
українських виданнях – 7.
Кількість наукових публікацій в
зарубіжних виданнях – 1.
http://orcid.org/ 0000-0001-6000-5215.
Місце роботи автора:
Інститут кібернетики імені В.М. Глушкова
НАН України,
03187, м. Київ-187,
проспект Академіка Глушкова, 40.
E-mail: victoryakovlev@ukr.net
http://www.apsystem.org.ua/
|