6 декабря 2021

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

Представьте, разработчики сделали смарт-контракт и прошли аудит. Запустили приложение, собрали миллиард долларов, а хакер взял и все украл — реальная ситуация в мире DeFi. Формальная верификация помогла бы избежать взлома контракта, но про нее почти не вспоминают. Но почему, если она может сохранить миллиарды?

Слишком длинно, не прочел: формальная верификация — это как доказательство математической теоремы, но для кода. В результате тестировщик либо получает доказательство, что код корректно работает с любыми входящими параметрами, либо узнает о существующих багах. Формальную верификацию проходят ядра Windows и MacOS, системы управления космическими ракетами, ПО атомных электростанций и другие программные комплексы, где лишний пробел может нанести убытки в миллиарды долларов.

Как разработчики тестируют смарт-контракты

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

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

Наш Боб только что провел ручное тестирование: самостоятельно что-то сделал, а потом сам же проверил результат. Это медленно, а если в коде используются сотни аргументов, то и ненадежно. Поэтому Боб перешел на автоматизированные тесты.

Боб фиксит ошибку и пишет тест: если отправить 100 BB с его адреса на адрес Алисы, то контракт должен выдать ошибку «Недостаточно средств». Контракт проходит тест, Боб доволен. А появится ли новый баг, если попытаться отправить −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 Ukraine.

Обсудить в Discord!