Посібник із засобів безпеки для смарт-контрактів

Ми будемо використовувати три різні методики тестування та аналізу програм:

• Статичний аналіз за допомогою Slither. Усі шляхи програми апроксимуються та аналізуються одночасно за допомогою різних представлень програми (наприклад, граф потоку управління).
• Фазинг за допомогою Echidna. Код виконується за допомогою псевдовипадкової генерації транзакцій. Фазер намагатиметься знайти послідовність транзакцій, щоб порушити задану властивість.
• Символічне виконання за допомогою Manticore. Техніка формальної верифікації, яка перетворює кожен шлях виконання на математичну формулу, для якої можна перевірити обмеження.

Кожна техніка має свої переваги та недоліки і буде корисною в конкретних випадках:

* якщо всі шляхи досліджуються без тайм-ауту

Slither аналізує контракти за лічені секунди, однак статичний аналіз може призводити до хибних спрацьовувань і буде менш придатним для складних перевірок (наприклад, арифметичних). Запустіть Slither через API для простого доступу до вбудованих детекторів або через API для визначених користувачем перевірок.

Echidna має працювати кілька хвилин і видаватиме лише істинно позитивні результати. Echidna перевіряє надані користувачем властивості безпеки, написані на Solidity. Він може пропускати помилки, оскільки він заснований на випадковому дослідженні.

Manticore виконує аналіз "найважчої ваги". Як і Echidna, Manticore верифікує надані користувачем властивості. Для його запуску знадобиться більше часу, але він може довести дійсність властивості та не повідомлятиме про хибні спрацьовування.

Рекомендований робочий процес

Почніть із вбудованих детекторів Slither, щоб переконатися, що простих помилок немає зараз або не буде пізніше. Використовуйте Slither для перевірки властивостей, пов'язаних із успадкуванням, залежностями змінних і структурними проблемами. У міру зростання кодової бази використовуйте Echidna для перевірки більш складних властивостей кінцевого автомата. Поверніться до Slither, щоб розробити власні перевірки для захисту, недоступного в Solidity, наприклад, для захисту від перевизначення функції. Нарешті, використовуйте Manticore для виконання цільової верифікації критичних властивостей безпеки, наприклад, арифметичних операцій.

• Використовуйте CLI Slither для виявлення поширених проблем
• Використовуйте Echidna для тестування високорівневих властивостей безпеки вашого контракту
• Використовуйте Slither для написання власних статичних перевірок.
• Використовуйте Manticore, якщо вам потрібна поглиблена гарантія критичних властивостей безпеки

Примітка щодо модульних тестів. Модульні тести необхідні для створення якісного програмного забезпечення. Однак ці методи не найкраще підходять для виявлення недоліків безпеки. Зазвичай вони використовуються для перевірки позитивної поведінки коду (тобто код працює належним чином у звичайному контексті), тоді як недоліки безпеки, як правило, містяться в крайових випадках, які розробники не враховували. У нашому дослідженні десятків оглядів безпеки смарт-контрактів покриття модульними тестами не вплинуло на кількість або серйозність недоліків безпеки (opens in a new tab), які ми виявили в коді наших клієнтів.

Визначення властивостей безпеки

Щоб ефективно перевірити та верифікувати свій код, ви повинні визначити області, на які потрібно звернути увагу. Оскільки ваші ресурси, витрачені на безпеку є обмеженими, важливо визначити слабкі або найцінніші частини вашої кодової бази для оптимізації зусиль. Моделювання загроз може допомогти. Розгляньте:

• Швидка оцінка ризиків (opens in a new tab) (наш бажаний підхід, коли бракує часу)
• Посібник із моделювання загроз для систем, орієнтованих на дані (opens in a new tab) (також відомий як NIST 800-154)
• Моделювання загроз за Шостаком (opens in a new tab)
• STRIDE (opens in a new tab) / DREAD (opens in a new tab)
• PASTA (opens in a new tab)
• Використання тверджень (opens in a new tab)

Компоненти

Знання того, що ви хочете перевірити, також допоможе вам підібрати правильний інструмент.

До основних сфер, які часто є актуальними для смарт-контрактів, належать:

• Кінцевий автомат. Більшість контрактів можна представити як кінцевий автомат. Варто перевірити, що (1) неможливо досягти недійсного стану, (2) якщо стан дійсний, то він є досяжним і (3) жоден стан не блокує контракт.

  • Echidna та Manticore — це інструменти, яким варто надати перевагу для тестування специфікацій кінцевих автоматів.

• Контроль доступу. Якщо у вашій системі є привілейовані користувачі (наприклад, власник, контролери, ...) ви повинні переконатися, що (1) кожен користувач може виконувати тільки дозволені дії, і (2) жоден користувач не може блокувати дії більш привілейованого користувача.

  • Slither, Echidna та Manticore можуть перевірити правильність контролю доступу. Наприклад, Slither може перевірити, що лише у функцій з білого списку відсутній модифікатор onlyOwner. Echidna і Manticore корисні для більш складного контролю доступу, наприклад, дозволу, що надається лише в тому випадку, якщо контракт досягає заданого стану.

• Арифметичні операції. Перевірка коректності арифметичних операцій має вирішальне значення. Використання SafeMath усюди — це хороший крок для запобігання переповненню/антипереповненню, однак ви все одно повинні враховувати інші арифметичні недоліки, включаючи проблеми з округленням і недоліки, які блокують контракт.

  • Manticore — найкращий вибір тут. Echidna може бути використана, якщо арифметика виходить за рамки розв’язувача SMT.

• Правильність успадкування. Контракти Solidity значною мірою покладаються на множинне успадкування. Можна легко припуститися таких помилок, як відсутність виклику super у функції, що затінює, та неправильно інтерпретований порядок лінеаризації c3.

  • Slither — це інструмент для виявлення цих проблем.

• Зовнішні взаємодії. Контракти взаємодіють між собою, і деяким зовнішнім контрактам не варто довіряти. Наприклад, якщо ваш контракт покладається на зовнішніх оракулів, чи залишиться він безпечним, якщо половина доступних оракулів буде скомпрометована?

  • Manticore та Echidna — найкращий вибір для тестування зовнішніх взаємодій із вашими контрактами. Manticore має вбудований механізм для створення заглушок для зовнішніх контрактів.

• Відповідність стандартам. Стандарти Ethereum (наприклад, ERC20) мають історію недоліків у своєму дизайні. Пам'ятайте про обмеження стандарту, на якому ви будуєте.

  • Slither, Echidna і Manticore допоможуть вам виявити відхилення від заданого стандарту.

Шпаргалка з вибору інструментів

Залежно від ваших цілей потрібно буде перевіряти й інші сфери, але ці загальні напрямки є хорошою відправною точкою для будь-якої системи смарт-контрактів.

Наші публічні аудити містять приклади верифікованих або протестованих властивостей. Рекомендуємо прочитати розділи Автоматизоване тестування та верифікація в наступних звітах, щоб ознайомитися з реальними властивостями безпеки:

• 0x (opens in a new tab)
• Balancer (opens in a new tab)

Останні оновлення сторінки: 22 жовтня 2025 р.

p (opens in a new tab)

m (opens in a new tab)

c (opens in a new tab)

+9

Переглянути учасників