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