Эта статья написана сообществом. Автор: Дэвид Тардити, вице-президент по инженерным вопросам в компании CertiK, которая осуществляет аудит смарт-контрактов в Web3.
Осторожно! Много текста
Формальная верификация смарт-контрактов гарантирует, что в них нет ошибок, уязвимостей и других дефектов. В ходе верификации специалист-аудитор представляет логику смарт-контракта в виде математической теоремы, а затем запускает автоматический процесс по сверке фактической логики с моделями ожидаемой работы контракта. Сочетание формальной верификации и ручного аудита обеспечивает всестороннюю оценку безопасности смарт-контракта.
Введение
Смарт-контракты — это компьютерные программы, размещенные на блокчейне. Они запускаются автоматически при определенных условиях. Эти программы бывают простыми или сложными, и в них могут храниться активы стоимостью в миллионы и даже миллиарды долларов.
Наличие уязвимостей в коде контракта может иметь катастрофические последствия, включая потерю всех хранящихся в нем активов. Так, в 2021 году из автоматического маркет-мейкера (AMM) Uranium Finance было похищено $50 миллионов из-за одной ошибки в смарт-контракте.
Также в 2021 году компания Compound Finance потеряла $80 миллионов в виде незаработанных вознаграждений из-за одной опечатки в коде. А в 2022 году из Wormhole Bridge украли $320 миллионов из-за уязвимости в одном из смарт-контрактов.
Таким образом, крайне важно устранить все уязвимости в программе смарт-контракта до его запуска. Ведь смарт-контракты имеют открытый исходный код, который станет общедоступным после развертывания. Если злоумышленник обнаружит ошибку, он сможет немедленно ею воспользоваться. Кроме того, устранить какие-либо дефекты по истечении времени будет невозможно, поскольку код смарт-контракта обычно нельзя изменить после развертывания.
Как работает верификация смарт-контрактов
Формальная верификация смарт-контрактов осуществляется путем представления логики и действий смарт-контракта в виде математической теоремы. Затем аудиторы используют автоматические инструменты для проверки ее корректности.
Верификация проходит следующим образом:
Определение технических характеристик и важных свойств контракта на формальном языке.
Перевод кода контракта в формальный вид, такой как математическая теорема или уравнение.
Запуск автоматизированных средств доказательства теорем или валидации моделей для проверки технических характеристик и свойств контракта.
Повторение процесса верификации для поиска и устранения ошибок или отклонений от необходимых свойств.
Важность верификации смарт-контрактов
Использование математической проверки позволяет гарантировать, что смарт-контракты, прошедшие формальную верификацию, не содержат ошибок, уязвимостей и других дефектов. Оно также повышает доверие к контракту, поскольку его свойства и технические характеристики прошли строгую сверку.
Далее приведены примеры того, как верификация смарт-контрактов помогла предотвратить значительные финансовые потери и другие негативные последствия.
Uniswap
Uniswap — это широко известный AMM. После разработки смарт-контракта Uniswap V1 он прошел формальную верификацию, в результате чего были выявлены и исправлены ошибки округления, которые могли привести к потере средств в Uniswap V1.
Balancer
Balancer V2 — еще один AMM, прошедший формальную верификацию. В результате проверки в смарт-контракте была обнаружена и исправлена ошибка в расчете комиссий для флеш-кредитов, из-за которой средства на бирже могли быть украдены.
SafeMoon
После запуска SafeMoon V1 проект прошел формальную верификацию и выявил ошибку. Из-за нее владелец контракта мог отказаться от права собственности, осуществив перед этим определенные действия, а затем вновь приобрести его.
Эта ошибка осталась незамеченной в ходе большинства ручных аудитов форков SafeMoon V1, поскольку для ее обнаружения требовалось проанализировать определенные комбинации значений в программных переменных. Такая работа затруднительна для человека, но довольно проста для машины.
Сочетание формальной верификации и ручного аудита
Формальная верификация обеспечивает систематический и автоматический способ проверки логики и действий смарт-контракта на соответствие необходимым свойствам. Это облегчает выявление и исправление любых потенциальных ошибок или недочетов. Такая проверка особенно эффективна для выявления сложных или незаметных проблем, которые трудно обнаружить при ручной проверке.
Ручной аудит подразумевает проверку кода, дизайна и развертывания контракта экспертом. Аудитор использует свой опыт и знания для выявления рисков и оценки общего уровня безопасности контракта. Помимо этого, он может подтвердить, что процесс формальной верификации был выполнен корректно, и выявить проблемы, которую автоматические инструменты могли упустить.
Сочетание формальной верификации и ручного аудита обеспечивает всестороннюю оценку безопасности смарт-контракта. Она же повышает шансы на обнаружение и устранение всех уязвимостей. В результате мы получаем комплексный подход к обеспечению безопасности, который сочетает возможности людей и машин.
В заключение
Для обеспечения безопасности смарт-контрактов необходимо использовать как формальную верификацию, так и ручной аудит — их сочетание позволяет проводить всестороннюю и тщательную оценку безопасности смарт-контракта.
Хотя формальная верификация требует немало ресурсов, она крайне важна для контрактов с высокой стоимостью или факторами значительного риска. В конечном итоге безопасность должна быть главным приоритетом, поэтому устранение ошибок, уязвимостей и других изъянов в смарт-контрактов — неотъемлемая задача успешного проекта.
Рекомендуемая литература
Предупреждение о рисках и отказ от ответственности: следующие материалы предоставляются на условиях «как есть» без каких-либо гарантий исключительно для общих справочных и образовательных целей. Эта информация не должна рассматриваться как финансовая консультация или рекомендация по приобретению какого-либо конкретного продукта или услуги. Стоимость цифровых активов может быть волатильной, в результате чего повышается риск потери инвестиций. Вы несете полную ответственность за свои инвестиционные решения. Binance не несет ответственность за ваши возможные убытки. Эта информация не должна рассматриваться в качестве финансовой рекомендации.