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