Что такое формальная верификация смарт-контрактов
Главная
Статьи
Что такое формальная верификация смарт-контрактов

Что такое формальная верификация смарт-контрактов

Профессионал
Опубликовано Mar 2, 2023Обновлено Jul 12, 2023
5m

Эта статья написана сообществом. Автор: Дэвид Тардити, вице-президент по инженерным вопросам в компании CertiK, которая осуществляет аудит смарт-контрактов в Web3.

Осторожно! Много текста

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

Введение

Смарт-контракты — это компьютерные программы, размещенные на блокчейне. Они запускаются автоматически при определенных условиях. Эти программы бывают простыми или сложными, и в них могут храниться активы стоимостью в миллионы и даже миллиарды долларов.  

Наличие уязвимостей в коде контракта может иметь катастрофические последствия, включая потерю всех хранящихся в нем активов. Так, в 2021 году из автоматического маркет-мейкера (AMM) Uranium Finance было похищено $50 миллионов из-за одной ошибки в смарт-контракте.

Также в 2021 году компания Compound Finance потеряла $80 миллионов в виде незаработанных вознаграждений из-за одной опечатки в коде. А в 2022 году из Wormhole Bridge украли $320 миллионов из-за уязвимости в одном из смарт-контрактов.

Таким образом, крайне важно устранить все уязвимости в программе смарт-контракта до его запуска. Ведь смарт-контракты имеют открытый исходный код, который станет общедоступным после развертывания. Если злоумышленник обнаружит ошибку, он сможет немедленно ею воспользоваться. Кроме того, устранить какие-либо дефекты по истечении времени будет невозможно, поскольку код смарт-контракта обычно нельзя изменить после развертывания.

Как работает верификация смарт-контрактов  

Формальная верификация смарт-контрактов осуществляется путем представления логики и действий смарт-контракта в виде математической теоремы. Затем аудиторы используют автоматические инструменты для проверки ее корректности.

Верификация проходит следующим образом:

  1. Определение технических характеристик и важных свойств контракта на формальном языке.

  2. Перевод кода контракта в формальный вид, такой как математическая теорема или уравнение.

  3. Запуск автоматизированных средств доказательства теорем или валидации моделей для проверки технических характеристик и свойств контракта.

  4. Повторение процесса верификации для поиска и устранения ошибок или отклонений от необходимых свойств.

Важность верификации смарт-контрактов

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

Далее приведены примеры того, как верификация смарт-контрактов помогла предотвратить значительные финансовые потери и другие негативные последствия.  

Uniswap

Uniswap — это широко известный AMM. После разработки смарт-контракта Uniswap V1 он прошел формальную верификацию, в результате чего были выявлены и исправлены ошибки округления, которые могли привести к потере средств в Uniswap V1. 

Balancer

Balancer V2 — еще один AMM, прошедший формальную верификацию. В результате проверки в смарт-контракте была обнаружена и исправлена ошибка в расчете комиссий для флеш-кредитов, из-за которой средства на бирже могли быть украдены.

SafeMoon

После запуска SafeMoon V1 проект прошел формальную верификацию и выявил ошибку. Из-за нее владелец контракта мог отказаться от права собственности, осуществив перед этим определенные действия, а затем вновь приобрести его.

Эта ошибка осталась незамеченной в ходе большинства ручных аудитов форков SafeMoon V1, поскольку для ее обнаружения требовалось проанализировать определенные комбинации значений в программных переменных. Такая работа затруднительна для человека, но довольно проста для машины.

Сочетание формальной верификации и ручного аудита

Формальная верификация обеспечивает систематический и автоматический способ проверки логики и действий смарт-контракта на соответствие необходимым свойствам. Это облегчает выявление и исправление любых потенциальных ошибок или недочетов. Такая проверка особенно эффективна для выявления сложных или незаметных проблем, которые трудно обнаружить при ручной проверке.

Ручной аудит подразумевает проверку кода, дизайна и развертывания контракта экспертом. Аудитор использует свой опыт и знания для выявления рисков и оценки общего уровня безопасности контракта. Помимо этого, он может подтвердить, что процесс формальной верификации был выполнен корректно, и выявить проблемы, которую автоматические инструменты могли упустить. 

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

В заключение

Для обеспечения безопасности смарт-контрактов необходимо использовать как формальную верификацию, так и ручной аудит — их сочетание позволяет проводить всестороннюю и тщательную оценку безопасности смарт-контракта.

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

Рекомендуемая литература

Предупреждение о рисках и отказ от ответственности: следующие материалы предоставляются на условиях «как есть» без каких-либо гарантий исключительно для общих справочных и образовательных целей. Эта информация не должна рассматриваться как финансовая консультация или рекомендация по приобретению какого-либо конкретного продукта или услуги. Стоимость цифровых активов может быть волатильной, в результате чего повышается риск потери инвестиций. Вы несете полную ответственность за свои инвестиционные решения. Binance не несет ответственность за ваши возможные убытки. Эта информация не должна рассматриваться в качестве финансовой рекомендации.

Получайте БЕСПЛАТНУЮ криптовалюту за изучение блокчейна
Binance Sensei
I am powered by ChatGPT and trained with 1,000+ articles and glossary entries from Binance Academy. My responses are provided on an “as is” basis for general information only, without any representation, warranty or guarantee of completeness or accuracy. See full terms and conditions here