Формальна верифікація: фіча Tezos, про яку ніхто не говорить

Формальна верифікація: фіча Tezos, про яку ніхто не говорить

Надто довго, не читав: формальна верифікація — це як доказ математичної теореми, але для коду. В результаті тестувальник або отримує доказ, що код коректно працює з будь-якими параметрами, або дізнається про існуючі баги. Формальну верифікацію проходять ядра Windows і MacOS, системи управління космічними ракетами, ПЗ атомних електростанцій та інші програмні комплекси, де зайвий пробіл може завдати збитків на мільярди доларів.

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

Як розробники тестують смарт-контракти

Допустимо, Боб написав смарт-контракт токена BB. Він складається з трьох функцій: «Визначити адресу відправника», «Додати нового користувача до бази даних» та «Перевести токени від відправника до одержувача».

Боб вирішує протестувати контракт. Він ставить собі баланс 50 BB, а потім намагається відправити Алісі 100 BB. Контракт забирає у Боба 100 BB і зараховує їх Алісі. Баланс Боба тепер складає −50, тому що він забув написати функцію «Перевірити, чи достатньо відправника коштів».

Наш Боб щойно провів ручне тестування: самостійно щось зробив, а потім сам перевірив результат. Це повільно, і якщо в коді використовуються сотні аргументів, то й ненадійно. Тож Боб перейшов на автоматизовані тести.

Боб фіксує помилку і пише тест: якщо відправити 100 ВВ з його адреси на адресу Аліси, то контракт має видати помилку «Недостатньо коштів». Контракт проходить тест, Боб задоволений. А чи з’явиться новий баг, якщо спробувати надіслати −50, 0 або 0,0000000001 BB? Боб сумує і йде ганяти той же скрипт з новими й новими параметрами.

Чому тестування нічого не доводить

Чим складніше логіка роботи договору, тим більше необхідно тестів з різними спектрами аргументів. В ідеалі треба перевірити коректність роботи всього коду, від присвоєння аргументів до виконання функцій. І навіть 100% покриття коду тестами не дає гарантію того, що начебто нормальна транзакція на 322,3782 BB не викличе якийсь небезпечний баг через те, що Боб поставив зайвий пробіл.

Ручне та автоматизоване тестування дають відповіді на запитання «При цих параметрах чи робить код те, що задумав розробник?». Формальна верифікація відповідає: «Чи завжди код робить те, що задумав розробник?»

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

6 = 2 × 3

84 = 2 × 2 × 3 × 7

4620 = 2 × 2 × 3 × 7 × 5 × 11

Теорему можна тестувати нескінченно: раптом знайдеться таке число, яке можна розкласти двома способами? У результаті тестування не доведе, що теорема правильна для всіх натуральних чисел.

Математики сперечалися про прості числа ще з часів Стародавньої Греції. Тільки в 1801 Карл Гаус сформулював теорему та опублікував її математичний доказ. Говорячи мовою тестувальників, він її формально верифікував.

Що таке формальна верифікація

Формальна верифікація — це доказ того, що код програми або смарт-контракту відповідає своєму опису і працює як задумано: за коректних параметрів він працює коректно, за некоректних — видає відповідні помилки. Така перевірка знаходить усі можливі помилки в коді та дозволяє розробникам зробити контракт безпечним на 99,9% (ніхто не скасовував баги у компіляторі та середовищі виконання).

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

При звичайному тестуванні розробник визначає лише вхідні параметри, з якими він виконуватиме код. Але машини формальної верифікації не виконують код, що верифікується: вони дивляться на нього як на математичне завдання виду a + b = x і шукають такі вхідні параметри a і b, щоб отримати результат x.

Наприклад, якщо Боб вкаже результат “Баланс користувача став негативним”, то машина або видасть йому набір вхідних параметрів, який викликає баг і призводить до негативного балансу, або скаже, що таких параметрів не існує.

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

При чому тут Tezos

Мова віртуальної машини Tezos Michelson і сама машина формально верифіковані — у них немає багів та вразливостей.

Крім того, розробники зробили для Michelson бібліотеку Mi-Cho-Coq, за допомогою якої машина формальної верифікації Coq розуміє інструкції Michelson. Це спрощує перенесення контракта в формальну специфікацію і складання теореми для перевірки.

Артур Брайтман на Hong Kong Blockchain Week 2020 назвав формальну верифікацію одним із трьох стовпів Tezos та пояснив, чому вона важлива:

«Формальна верифікація Tezos — це техніка тестування. Її вперше почали застосовувати в ракетобудуванні та аеронавтиці. В 1996 ракета Аріан-5 вибухнула в першу хвилину польоту, тому що одна зі змінних модуля орієнтування переповнилася. Якщо у вас є код, помилка в якому завдасть величезних збитків, то варто переконатися, що все працює як треба. І формальна верифікація — один із найвищих стандартів для перевірки коду»

У результаті Tezos вийшов надійнішим та зручнішим для створення додатків та контрактів з високим ступенем безпеки.

Підпишіться на соціальні мережі Tezos Ukraine, щоб нічого не пропустити:

  1. Telegram-канал
  2. Facebook.
  3. Twitter російською та українською мовами
  4. Twitter англійською мовою
  5. YouTube-канал
  6. Instagram
  7. LinkedIn
  8. hub на ForkLog

наступний

Tezos за місяць: технології, економіка та спільнота в листопаді

Читайте схожі пости

Де зараз найвигідніший фармінг на Tezos?

Де зараз найвигідніший фармінг на Tezos?

Ф’ючерси на Tezos: тестуємо децентралізовану платформу деривативів Zenith

Ф’ючерси на Tezos: тестуємо децентралізовану платформу деривативів Zenith

Як купити Porsche за tez: огляд Smartlink Marketplace

Як купити Porsche за tez: огляд Smartlink Marketplace

Читайте блог і не пропускайте новини про TezosЧитати блог

Спільнота