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

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

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

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

* якщо всі шляхи досліджено без перевищення часу очікування (тайм-ауту)

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

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

Мантікора виконує «найважчий» аналіз. Як і Ехідна, Мантікора перевіряє надані користувачем властивості. Їй знадобиться більше часу для виконання, але вона може довести дійсність властивості та не видаватиме хибних спрацьовувань.

Пропонований робочий процес

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

• Використовуйте CLI Слізер для виявлення поширених проблем
• Використовуйте Ехідна для тестування високорівневих властивостей безпеки вашого контракту
• Використовуйте Слізер для написання власних статичних перевірок
• Використовуйте Мантікора, коли вам потрібна глибока впевненість у критичних властивостях безпеки

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

Компоненти

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

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

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

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

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

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

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

  • Мантікора — найкращий вибір у цьому випадку. Ехідна можна використовувати, якщо арифметика виходить за межі можливостей SMT-вирішувача.

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

  • Слізер — це інструмент, який гарантує виявлення цих проблем.

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

  • Мантікора та Ехідна — найкращий вибір для тестування зовнішніх взаємодій із вашими контрактами. Мантікора має вбудований механізм для створення заглушок (stub) зовнішніх контрактів.

• Відповідність стандартам. Стандарти Етеріуму (наприклад, ERC-20) мають історію недоліків у своєму дизайні. Будьте свідомі обмежень стандарту, на якому ви будуєте.

  • Слізер, Ехідна та Мантікора допоможуть вам виявити відхилення від заданого стандарту.

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

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

Наші публічні аудити містять приклади верифікованих або протестованих властивостей. Розгляньте можливість прочитання розділів Automated Testing and Verification у наступних звітах, щоб ознайомитися з реальними властивостями безпеки:

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