Представьте, разработчики сделали смарт-контракт и прошли аудит. Запустили приложение, собрали миллиард долларов, а хакер взял и все украл — реальная ситуация в мире 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, чтобы ничего не пропустить:
- Telegram-канал
- Facebook.
- Twitter на русском и украинском языках
- Twitter на английском языке
- YouTube-канал
- hub на ForkLog
Изначально мы опубликовали этот материал в блоге Tezos Ukraine.