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