ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ СМАРТ-КОНТРАКТОВ
Умные контрактыделают возможным создание децентрализованных, недоверительных и надежных приложений, которые представляют новые случаи использования и разблокируют ценность для пользователей. Поскольку смарт-контракты обрабатывают большие суммы ценности, безопасность является критическим соображением для разработчиков.
Формальная верификация - одна из рекомендуемых техник для улучшениябезопасность смарт-контрактов. Формальная верификация, которая используетформальные методы
для спецификации, проектирования и верификации программ используется на протяжении многих лет для обеспечения корректности критически важных аппаратных и программных систем.
При реализации в смарт-контрактах формальная верификация может доказать, что бизнес-логика контракта соответствует заранее определенной спецификации. По сравнению с другими методами оценки правильности кода контракта, такими как тестирование, формальная верификация обеспечивает более надежные гарантии того, что смарт-контракт функционально корректен.
ЧТО ТАКОЕ ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ?
Формальная верификация относится к процессу оценки корректности системы относительно формальной спецификации. Проще говоря, формальная верификация позволяет нам проверить, удовлетворяет ли поведение системы определенным требованиям (т.е. делает то, что мы хотим).
Ожидаемые поведенческие характеристики системы (в данном случае - смарт-контракта) описываются с использованием формального моделирования, тогда как языки спецификации позволяют создавать формальные свойства. Техники формальной верификации могут затем проверить, что реализация контракта соответствует его спецификации и извлечь математическое доказательство корректности последнего. Когда контракт удовлетворяет своей спецификации, его описывают как "функционально корректный", "корректный по дизайну" или "корректный по построению".
Что такое формальная модель?
В области информатики, формальная модель
это математическое описание вычислительного процесса. Программы абстрагируются в математические функции (уравнения), причем модель описывает, как вычисляются выходы функций при заданном входе.
Формальные модели обеспечивают уровень абстракции, над которым можно оценить поведение программы. Наличие формальных моделей позволяет создать формальную спецификацию, которая описывает желаемые свойства модели вопроса.
Для моделирования смарт-контрактов с целью формальной верификации применяются различные техники. Например, некоторые модели используются для анализа высокоуровневого поведения смарт-контракта. Эти техники моделирования применяют черный ящик для смарт-контрактов, рассматривая их как системы, принимающие входные данные и выполняющие вычисления на основе этих входных данных.
Модели высокого уровня сосредотачиваются на взаимоотношениях между смарт-контрактами и внешними агентами, такими как внешние управляемые учетные записи (EOA), контрактные учетные записи и среда блокчейна. Такие модели полезны для определения свойств, которые указывают, как должен вести себя контракт в ответ на определенные пользовательские взаимодействия.
Наоборот, другие формальные модели сосредотачиваются на низкоуровневом поведении смарт-контракта. В то время как высокоуровневые модели могут помочь в рассуждениях о функциональности контракта, они могут не учитывать детали внутренней работы реализации. Низкоуровневые модели применяют вид белого ящика к анализу программ и полагаются на более низкоуровневые представления приложений смарт-контрактов, такие как следы программы и графики потока управления
, чтобы рассуждать о свойствах, важных для выполнения контракта.
Низкоуровневые модели считаются идеальными, так как они представляют фактическое выполнение смарт-контракта в среде выполнения Ethereum (т. е. EVM). Техники низкоуровневого моделирования особенно полезны для установления критически важных свойств безопасности в смарт-контрактах и выявления потенциальных уязвимостей.
Что такое формальная спецификация?
Спецификация - это просто техническое требование, которому должна удовлетворять определенная система. В программировании спецификации представляют общие идеи о выполнении программы (т. е. что программа должна делать).
В контексте смарт-контрактов формальные спецификации относятся к свойствам - формальным описаниям требований, которым должен удовлетворять контракт. Такие свойства описываются как «инварианты» и представляют собой логические утверждения о выполнении контракта, которые должны оставаться верными в любом возможном случае, без исключений.
Таким образом, мы можем рассматривать формальную спецификацию как совокупность утверждений, написанных на формальном языке, которые описывают предполагаемое выполнение смарт-контракта. Спецификации охватывают свойства контракта и определяют, как контракт должен вести себя в различных обстоятельствах. Цель формальной верификации - определить, обладает ли смарт-контракт этими свойствами (инвариантами) и не нарушаются ли эти свойства во время выполнения.
Формальные спецификации критичны для разработки безопасных реализаций смарт-контрактов. Контракты, которые не реализуют инварианты или нарушают свои свойства во время выполнения, подвержены уязвимостям, которые могут повредить функциональность или вызвать злонамеренные эксплойты.
ТИПЫ ФОРМАЛЬНЫХ СПЕЦИФИКАЦИЙ ДЛЯ СМАРТ-КОНТРАКТОВ
Формальные спецификации позволяют математически рассуждать о правильности выполнения программы. Как и с формальными моделями, формальные спецификации могут захватывать как высокоуровневые свойства, так и низкоуровневое поведение реализации контракта.
Формальные спецификации разрабатываются с использованием элементов логика программы
, которые позволяют формальное рассуждение о свойствах программы. Логика программы имеет формальные правила, которые выражают (на математическом языке) ожидаемое поведение программы. Для создания формальных спецификаций используются различные логики программ, включая логика достижимости
Формальные спецификации для смарт-контрактов можно классифицировать широко как высокоуровневые, так и низкоуровневые спецификации. Независимо от того, к какой категории относится спецификация, она должна должным образом и однозначно описывать свойство системы под анализом.
Спецификации высокого уровня
Как следует из названия, спецификация высокого уровня (также называемая "спецификацией, ориентированной на модель") описывает высокоуровневое поведение программы. Высокоуровневые спецификации моделируют смарт-контракт как конечный автомат
(FSM), который может переходить между состояниями, выполняя операции, с использованием временной логики для определения формальных свойств модели FSM.
Это «правила рассуждения о высказываниях, квалифицированных в терминах времени (например, «Я всегда голоден» или «Я в конечном итоге буду голоден»)». Применительно к формальной верификации временные логики используются для формулирования утверждений о правильном поведении систем, моделируемых как конечные автоматы. Конкретно, временная логика описывает будущие состояния, в которых может находиться смарт-контракт, и то, как он переходит между состояниями.
Общие спецификации обычно охватывают два критических временных свойства для смарт-контрактов: безопасность и живучесть. Свойства безопасности представляют собой идею того, что "никогда не происходит ничего плохого" и обычно выражают неизменность. Свойство безопасности может определять общие требования программного обеспечения, такие как свобода от тупик
, или выражать доменно-специфические свойства для контрактов (например, инварианты на контроль доступа к функциям, допустимые значения переменных состояния или условия для передачи токенов).
Возьмем, к примеру, такое требование безопасности, которое охватывает условия использования transfer() или transferFrom() в контрактах токенов ERC-20: «Баланс отправителя никогда не ниже запрошенного количества токенов для отправки». Это естественноязычное описание инварианта контракта может быть переведено в формальную (математическую) спецификацию, которая затем может быть тщательно проверена на допустимость.
Свойства живучести утверждают, что "в конечном итоге происходит что-то хорошее" и касаются способности контракта продвигаться через различные состояния. Примером свойства живучести является "ликвидность", которая относится к способности контракта переводить свои балансы пользователям по запросу. Если это свойство нарушается, пользователи не смогут вывести активы, хранящиеся в контракте, как произошло с Инцидент кошелька Parity
.
Низкоуровневые спецификации
Спецификации высокого уровня берут за отправную точку конечно-состоянийную модель контракта и определяют желаемые свойства этой модели. В отличие от этого, спецификации низкого уровня (также называемые «ориентированные на свойства спецификации») часто моделируют программы (смарт-контракты) как системы, включающие в себя набор математических функций и описывают правильное поведение таких систем.
Проще говоря, низкоуровневые спецификации анализируют следы программы и пытаются определить свойства смарт-контракта по этим следам. Следы относятся к последовательностям выполнения функций, которые изменяют состояние смарт-контракта; следовательно, низкоуровневые спецификации помогают определить требования к внутреннему выполнению контракта.
Низкоуровневые формальные спецификации могут быть представлены как свойства в стиле Хоара, так и инварианты на путях выполнения.
Свойства стиля Хоара
предоставляет набор формальных правил для рассуждения о корректности программ, включая смарт-контракты. Свойство в стиле Хоара представлено тройкой Хоара {P}c{Q}, где c - это программа, а P и Q - предикаты для состояния c (т.е. программы), формально описанные как предусловия и постусловия соответственно.
Предусловие - это предикат, описывающий условия, необходимые для правильного выполнения функции; пользователи, вызывающие контракт, должны удовлетворять этому требованию. Постусловие - это предикат, описывающий условие, которое функция устанавливает при правильном выполнении; пользователи могут ожидать, что это условие будет верным после вызова функции. Инвариант в логике Хоара - это предикат, который сохраняется выполнением функции (т.е. он не изменяется).
Спецификации в стиле Хоара могут гарантировать как частичную корректность, так и полную корректность. Реализация функции контракта является "частично корректной", если предусловие истинно перед выполнением функции, и если выполнение завершается, постусловие также истинно. Доказательство полной корректности достигается, если предусловие истинно перед выполнением функции, выполнение гарантировано завершится и, когда это произойдет, постусловие также истинно.
Получение доказательства общей правильности сложно, поскольку некоторые исполнения могут задерживаться перед завершением или вообще не завершаться. Тем не менее, вопрос о том, завершается ли исполнение, можно считать спорным, поскольку механизм газа Ethereum предотвращает бесконечные циклы программы (исполнение завершается либо успешно, либо из-за ошибки 'out-of-gas').
Спецификации смарт-контрактов, созданные с использованием логики Хоара, будут иметь предусловия, постусловия и инварианты, определенные для выполнения функций и циклов в контракте. Предусловия часто включают возможность ошибочных входных данных в функцию, с постусловиями, описывающими ожидаемый ответ на такие входы (например, генерация определенного исключения). Таким образом, свойства стиля Хоара эффективны для обеспечения правильности реализации контракта.
Многие формальные верификационные фреймворки используют спецификации в стиле Хоара для доказательства семантической корректности функций. Также можно добавить свойства в стиле Хоара (как утверждения) непосредственно в код контракта, используя операторы require и assert в Solidity.
операторы require выражают предусловие или инвариант и часто используются для проверки ввода пользователя, в то время как assert захватывает постусловие, необходимое для безопасности. Например, правильный контроль доступа к функциям (пример свойства безопасности) можно достичь, используя require в качестве проверки предусловия на идентичность вызывающего аккаунта. Аналогично, инвариант на допустимые значения переменных состояния в контракте (например, общее количество токенов в обращении) можно защитить от нарушений, используя assert для подтверждения состояния контракта после выполнения функции.
Свойства трассировки уровня
Спецификации на основе трассировки описывают операции, которые передают контракт между различными состояниями и связи между этими операциями. Как объяснялось ранее, трассировки — это последовательности операций, которые определенным образом изменяют состояние контракта.
Данный подход основан на модели смарт-контрактов как систем состояний с некоторыми предопределенными состояниями (описываемыми переменными состояния) вместе с набором предопределенных переходов (описываемых функциями контракта). Кроме того, граф потока управления
(CFG), который является графическим представлением потока выполнения программы, часто используется для описания операционной семантики контракта. Здесь каждый след представлен как путь на графе управления потоком.
В основном спецификации на уровне трассировки используются для рассмотрения шаблонов внутреннего выполнения в смарт-контрактах. Создавая спецификации на уровне трассировки, мы утверждаем допустимые пути выполнения (т. е. переходы состояний) для смарт-контракта. Используя такие техники, как символьное выполнение, мы можем формально проверить, что выполнение никогда не следует по пути, не определенному в формальной модели.
Давайте воспользуемся примером DAOконтракт, который имеет некоторые публично доступные функции для описания свойств на уровне трассировки. Здесь мы предполагаем, что контракт DAO позволяет пользователям выполнять следующие операции:
- Пополнить средства
- Проголосуйте за предложение после внесения средств
- Получите возврат средств, если они не проголосуют по предложению
Примером свойств уровня трассировки могут быть «пользователи, не вносящие средства, не могут голосовать за предложение» или «пользователи, не голосующие за предложение, всегда должны иметь возможность требовать возврата». Оба свойства утверждают предпочтительные последовательности выполнения (голосование не может произойти до внесения средств, а возвраты не могут произойти после голосования за предложение).
МЕТОДЫ ФОРМАЛЬНОЙ ПРОВЕРКИ СМАРТ-КОНТРАКТОВ
Проверка модели
Проверка модели - это формальный метод верификации, при котором алгоритм проверяет формальную модель смарт-контракта на соответствие его спецификации. При проверке модели смарт-контракты часто представлены в виде систем перехода состояний, в то время как свойства допустимых состояний контракта определяются с использованием временной логики.
Для модельной проверки требуется создание абстрактного математического представления системы (т. е. контракта) и выражение свойств этой системы с использованием формул, основанных на Пропозициональная логика
. Это упрощает задачу алгоритма проверки модели, а именно доказательство того, что математическая модель удовлетворяет заданной логической формуле.
Модельная проверка в формальной верификации в основном используется для оценки временных свойств, описывающих поведение контракта со временем. Временные свойства для смарт-контрактов включают в себя безопасность и живость, о которых мы ранее объясняли.
Например, свойство безопасности, относящееся к управлению доступом (например, Только владелец контракта может вызывать самоуничтожение), может быть записано в формальной логике. После этого алгоритм проверки модели может проверить, удовлетворяет ли контракт этой формальной спецификации.
Model checking использует исследование пространства состояний, которое включает в себя построение всех возможных состояний смарт-контракта и попытки найти достижимые состояния, приводящие к нарушению свойств. Однако это может привести к бесконечному количеству состояний (известному как "проблема взрыва состояний"), поэтому модельные проверяющие полагаются на техники абстракции, чтобы обеспечить эффективный анализ смарт-контрактов.
Доказательство теоремы
Доказательство теорем - это метод математического рассуждения о корректности программ, включая смарт-контракты. Он включает в себя преобразование модели системы контракта и его спецификаций в математические формулы (логические выражения).
Целью доказательства теоремы является проверка логического эквивалентности между этими утверждениями. «Логическое эквивалентность» (также называемое «логической двусторонней импликацией») - это тип отношения между двумя утверждениями, таким образом, что первое утверждение истинно тогда и только тогда, когда второе утверждение истинно.
Необходимое отношение (логическое эквивалентное) между высказываниями о модели контракта и его свойстве формулируется как доказуемое высказывание (называемое теоремой). С использованием формальной системы вывода автоматизированный доказатель теорем может проверить правильность теоремы. Другими словами, доказатель теоремы может окончательно доказать, что модель смарт-контракта точно соответствует его спецификациям.
При проверке моделей моделируют контракты как конечные системы состояний, теоремы могут обрабатывать анализ систем с бесконечным числом состояний. Однако это означает, что автоматизированный доказатель не всегда может знать, является ли логическая проблема "разрешимой" или нет.
В результате часто требуется человеческая помощь для направления доказательства теоремы в выводе доказательств о корректности. Использование человеческих усилий в доказательстве теорем делает его более дорогостоящим в использовании, чем проверка модели, которая полностью автоматизирована.
Символическое выполнение
Символическое выполнение - это метод анализа смарт-контракта путем выполнения функций с использованием символьных значений (например, x > 5) вместо конкретных значений (например, x == 5). Как техника формальной верификации, символическое выполнение используется для формального рассмотрения свойств на уровне трассировки в коде контракта.
Символическое выполнение представляет собой след выполнения в виде математической формулы над символическими входными значениями, иначе называемой предикатом пути. SMT решатель
используется для проверки того, является ли предикат пути "удовлетворимым" (т. е. существует значение, которое может удовлетворить формулу). Если уязвимый путь удовлетворим, решатель SMT сгенерирует конкретное значение, которое запускает выполнение в направлении этого пути.
Предположим, что функция смарт-контракта принимает в качестве входных данных значение uint (x) и отменяется, когда x больше 5, а также меньше 10. Чтобы найти значение x, которое вызывает ошибку, с помощью обычной процедуры тестирования потребовалось бы пройти десятки тестовых случаев (или больше) без уверенности в том, что вы действительно найдете входные данные, вызывающие ошибку.
С другой стороны, инструмент символьного выполнения выполнял бы функцию с символьным значением: X > 5 ∧ X < 10 (т. Е. x больше 5 И x меньше 10). Связанный с путевым предикатом x = X > 5 ∧ X < 10 затем будет передан решателю SMT для решения. Если определенное значение удовлетворяет формуле x = X > 5 ∧ X < 10, решатель SMT его вычислит, например, решатель может получить 7 в качестве значения для x.
Поскольку символьное выполнение зависит от входных данных программы, и набор входных данных для исследования всех достижимых состояний потенциально бесконечен, это по-прежнему является формой тестирования. Однако, как показано в примере, символьное выполнение эффективнее обычного тестирования при поиске входных данных, вызывающих нарушения свойств.
Кроме того, символьное выполнение создает меньше ложных срабатываний, чем другие техники, основанные на свойствах (например, fuzzing), которые случайным образом генерируют входные данные для функции. Если во время символьного выполнения возникает состояние ошибки, то возможно сгенерировать конкретное значение, вызывающее ошибку, и воспроизвести проблему.
Символическое выполнение также может обеспечить определенную степень математического доказательства корректности. Рассмотрим следующий пример функции контракта с защитой от переполнения:
Трассировка выполнения, которая приводит к переполнению целого числа, должна удовлетворять формуле: z = x + y И (z >= x) И (z=>y) И (z < x ИЛИ z < y) Такая формула вряд ли будет решена, поэтому она служит математическим доказательством того, что функция safe_add никогда не приводит к переполнению.
Зачем использовать формальную верификацию для смарт-контрактов?
Необходимость надежности
Формальная верификация используется для оценки правильности систем, критически важных для безопасности, отказ которых может иметь разрушительные последствия, такие как смерть, травмы или финансовая разруха. Смарт-контракты - это приложения высокой ценности, контролирующие огромные суммы ценности, и простые ошибки в проектировании могут привести к невозместимые потери для пользователей
Формальная верификация контракта перед развертыванием, однако, может увеличить гарантии того, что он будет работать ожидаемым образом после запуска на блокчейне.
Надежность - это очень желаемое качество в любом смарт-контракте, особенно потому, что код, развернутый в виртуальной машине Ethereum (EVM), как правило, является неизменяемым. С учетом того, что обновления после запуска не доступны, необходимость гарантировать надежность контрактов делает формальную верификацию необходимой. Формальная верификация способна обнаруживать сложные проблемы, такие как недостаток и переполнение целых чисел, рекурсию и плохую оптимизацию газа, которые могут ускользнуть от аудиторов и тестировщиков.
Доказать функциональную правильность
Тестирование программ - самый распространенный метод подтверждения того, что смарт-контракт удовлетворяет определенным требованиям. Это включает выполнение контракта с образцом данных, которые от него ожидаются, и анализ его поведения. Если контракт возвращает ожидаемые результаты для образцовых данных, то разработчики имеют объективное доказательство его корректности.
Однако такой подход не может доказать правильность выполнения входных значений, которые не являются частью выборки. Таким образом, тестирование контракта может помочь обнаружить ошибки (например, если некоторые пути кода не возвращают желаемые результаты во время выполнения), но оно не может окончательно доказать отсутствие ошибок.
И наоборот, формальная проверка может формально доказать, что смарт-контракт удовлетворяет требованиям для бесконечного диапазона исполнений вообще без запуска контракта. Для этого необходимо создать формальную спецификацию, которая точно описывает правильное поведение контракта, и разработать формальную (математическую) модель контрактной системы. Затем мы можем следовать формальной процедуре доказательства, чтобы проверить согласованность между моделью контракта и его спецификацией.
С формальной верификацией вопрос о проверке того, удовлетворяет ли бизнес-логика контракта требования, является математическим предложением, которое можно доказать или опровергнуть. Формально доказывая предложение, мы можем проверить бесконечное количество тестовых случаев с конечным числом шагов. Таким образом, формальная верификация имеет более хорошие перспективы доказать, что контракт функционально корректен относительно спецификации.
Целевые объекты верификации идеальны
Целевая верификация описывает систему, которая должна быть формально проверена. Формальная верификация наилучшим образом применяется в «встроенных системах» (небольшие, простые программные компоненты, являющиеся частью более крупной системы). Они также идеально подходят для специализированных областей, в которых мало правил, что упрощает модификацию инструментов для проверки свойств, специфичных для области.
Смарт-контракты, по крайней мере, частично, удовлетворяют оба требования. Например, небольшой размер контрактов Ethereum делает их пригодными для формальной верификации. Точно так же EVM следует простым правилам, что упрощает указание и проверку семантических свойств для программ, запускаемых в EVM.
Быстрый цикл разработки
Техники формальной верификации, такие как проверка модели и символьное выполнение, обычно более эффективны, чем обычный анализ кода смарт-контракта (проводимый во время тестирования или аудита). Это потому, что формальная верификация полагается на символьные значения для проверки утверждений («что, если пользователь попытается вывести n эфиров?»), в отличие от тестирования, которое использует конкретные значения («что, если пользователь попытается вывести 5 эфиров?»).
Символические входные переменные могут охватывать несколько классов конкретных значений, поэтому методы формальной верификации обещают больший охват кода за более короткий промежуток времени. При эффективном использовании формальная верификация может ускорить цикл разработки для разработчиков.
Формальная верификация также улучшает процесс создания децентрализованных приложений (dapps), уменьшая дорогостоящие ошибки проектирования. Обновление контрактов (где это возможно) для исправления уязвимостей требует обширного переписывания кодовых баз и большего усилия, затраченного на разработку. Формальная верификация может обнаружить множество ошибок в реализации контрактов, которые могут ускользнуть от тестировщиков и аудиторов, и предоставляет достаточно возможностей для устранения этих проблем перед развертыванием контракта.
НЕДОСТАТКИ ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ
Стоимость ручного труда
Формальная верификация, особенно полуавтоматизированная верификация, при которой человек направляет доказательство для вывода доказательств правильности, требует значительного количества ручного труда. Более того, создание формальной спецификации - это сложная деятельность, требующая высокого уровня навыков.
Эти факторы (усилие и навык) делают формальную верификацию более требовательной и дорогостоящей по сравнению с обычными методами оценки правильности в контрактах, такими как тестирование и проверки. Тем не менее, оплата стоимости полного аудита верификации практична, учитывая стоимость ошибок в реализации смарт-контрактов.
Ложноотрицательные
Формальная верификация может проверить только соответствие выполнения смарт-контракта формальной спецификации. Поэтому важно убедиться, что спецификация правильно описывает ожидаемое поведение смарт-контракта.
Если спецификации написаны плохо, нарушения свойств, указывающие на уязвимые исполнения, не могут быть обнаружены при формальной проверке аудита. В этом случае разработчик может ошибочно предположить, что контракт свободен от ошибок.
Проблемы производительности
При формальной верификации возникает ряд проблем производительности. Например, проблемы взрыва состояний и путей, возникающие при проверке моделей и символьной проверке соответственно, могут повлиять на процедуры верификации. Кроме того, инструменты формальной верификации часто используют SMT-решатели и другие решатели ограничений на своем нижнем уровне, и эти решатели полагаются на вычислительно интенсивные процедуры.
Кроме того, не всегда возможно для верификаторов программ определить, может ли свойство (описанное как логическая формула) быть удовлетворено или нет ("проблема разрешимости
потому что программа может никогда не завершиться. Таким образом, некоторые свойства контракта могут быть невозможно доказать, даже если он хорошо специфицирован.
Инструменты формальной верификации для смарт-контрактов Ethereum
Языки спецификации для создания формальных спецификаций
Act: Act позволяет указывать обновления хранилища, предусловия/постусловия и инварианты контракта. Его инструментальный набор также имеет поддержку доказательств, способных доказать множество свойств с помощью Coq, SMT-солверов или hevm.
Scribble - Scribble преобразует аннотации кода на языке спецификации Scribble в конкретные утверждения, которые проверяют спецификацию.
Dafny - Dafny - это язык программирования, готовый к верификации, который полагается на высокоуровневые аннотации для рассуждения о правильности кода и его доказательства.
Проверщики программ для проверки корректности
Certora Prover - Certora Prover - это автоматический инструмент формальной верификации для проверки правильности кода в смарт-контрактах. Спецификации написаны на CVL (Certora Verification Language), а нарушения свойств обнаруживаются с использованием комбинации статического анализа и решения ограничений.
Solidity SMTChecker - SMTChecker от Solidity - это встроенная программа проверки моделей, основанная на SMT (теориях выполнимости по модулю) и решении по Хорну. Он подтверждает, соответствует ли исходный код контракта спецификациям во время компиляции, и статически проверяет на наличие нарушений свойств безопасности.
solc-verify - solc-verify - это расширенная версия компилятора Solidity, которая может выполнять автоматизированную формальную верификацию кода Solidity с использованием аннотаций и модульной верификации программы.
KEVM - KEVM - это формальная семантика виртуальной машины Ethereum (EVM), написанная на платформе K. KEVM является исполняемым и может доказать определенные утверждения, связанные с свойствами, с использованием логики достижимости.
Логические фреймворки для доказательства теорем
Изабель - Изабель/HOL - это помощник по доказательствам, который позволяет выражать математические формулы формальным языком и предоставляет инструменты для доказательства этих формул. Основное применение - формализация математических доказательств, в частности формальная верификация, которая включает в себя доказательство правильности компьютерного оборудования или программного обеспечения и доказательство свойств компьютерных языков и протоколов.
Coq - Coq - это интерактивный доказательственный механизм, который позволяет вам определять программы с использованием теорем и интерактивно генерировать машинно-проверенные доказательства корректности.
Инструменты на основе символьного выполнения для обнаружения уязвимых шаблонов в смарт-контрактах
Manticore - инструмент для анализа байткода EVM на основе символьного выполнения.
hevm - hevm - это механизм символьного выполнения и проверка эквивалентности байт-кода EVM.
Mythril - инструмент символьного выполнения для обнаружения уязвимостей в умных контрактах Ethereum
Отказ от ответственности:
- Эта статья перепечатана с [ ]. Все авторские права принадлежат оригинальному автору [**]. Если есть возражения по поводу этого перепечатывания, пожалуйста, свяжитесь с Gate Learnкоманда, и они незамедлительно справятся с этим.
- Ответственность за отказ: Взгляды и мнения, высказанные в этой статье, являются исключительно точкой зрения автора и не являются инвестиционными советами.
- Переводы статьи на другие языки выполняются командой Gate Learn. Если не указано иное, копирование, распространение или плагиат переведенных статей запрещены.
Bài viết liên quan
Что такое Neiro? Все, что вам нужно знать о NEIROETH
Лучшие криптовалютные лотерейные платформы на 2024 год
Что такое обернутый Ethereum (WETH)？
ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ СМАРТ-КОНТРАКТОВ
ЧТО ТАКОЕ ФОРМАЛЬНАЯ ПРОВЕРКА?
ТИПЫ ФОРМАЛЬНЫХ СПЕЦИФИКАЦИЙ ДЛЯ СМАРТ-КОНТРАКТОВ
ТЕХНИКИ ФОРМАЛЬНОЙ ПРОВЕРКИ СМАРТ-КОНТРАКТОВ
НЕДОСТАТКИ ФОРМАЛЬНОЙ ПРОВЕРКИ
ИНСТРУМЕНТЫ ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ ДЛЯ СМАРТ-КОНТРАКТОВ ETHEREUM
Умные контрактыделают возможным создание децентрализованных, недоверительных и надежных приложений, которые представляют новые случаи использования и разблокируют ценность для пользователей. Поскольку смарт-контракты обрабатывают большие суммы ценности, безопасность является критическим соображением для разработчиков.
Формальная верификация - одна из рекомендуемых техник для улучшениябезопасность смарт-контрактов. Формальная верификация, которая используетформальные методы
для спецификации, проектирования и верификации программ используется на протяжении многих лет для обеспечения корректности критически важных аппаратных и программных систем.
При реализации в смарт-контрактах формальная верификация может доказать, что бизнес-логика контракта соответствует заранее определенной спецификации. По сравнению с другими методами оценки правильности кода контракта, такими как тестирование, формальная верификация обеспечивает более надежные гарантии того, что смарт-контракт функционально корректен.
ЧТО ТАКОЕ ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ?
Формальная верификация относится к процессу оценки корректности системы относительно формальной спецификации. Проще говоря, формальная верификация позволяет нам проверить, удовлетворяет ли поведение системы определенным требованиям (т.е. делает то, что мы хотим).
Ожидаемые поведенческие характеристики системы (в данном случае - смарт-контракта) описываются с использованием формального моделирования, тогда как языки спецификации позволяют создавать формальные свойства. Техники формальной верификации могут затем проверить, что реализация контракта соответствует его спецификации и извлечь математическое доказательство корректности последнего. Когда контракт удовлетворяет своей спецификации, его описывают как "функционально корректный", "корректный по дизайну" или "корректный по построению".
Что такое формальная модель?
В области информатики, формальная модель
это математическое описание вычислительного процесса. Программы абстрагируются в математические функции (уравнения), причем модель описывает, как вычисляются выходы функций при заданном входе.
Формальные модели обеспечивают уровень абстракции, над которым можно оценить поведение программы. Наличие формальных моделей позволяет создать формальную спецификацию, которая описывает желаемые свойства модели вопроса.
Для моделирования смарт-контрактов с целью формальной верификации применяются различные техники. Например, некоторые модели используются для анализа высокоуровневого поведения смарт-контракта. Эти техники моделирования применяют черный ящик для смарт-контрактов, рассматривая их как системы, принимающие входные данные и выполняющие вычисления на основе этих входных данных.
Модели высокого уровня сосредотачиваются на взаимоотношениях между смарт-контрактами и внешними агентами, такими как внешние управляемые учетные записи (EOA), контрактные учетные записи и среда блокчейна. Такие модели полезны для определения свойств, которые указывают, как должен вести себя контракт в ответ на определенные пользовательские взаимодействия.
Наоборот, другие формальные модели сосредотачиваются на низкоуровневом поведении смарт-контракта. В то время как высокоуровневые модели могут помочь в рассуждениях о функциональности контракта, они могут не учитывать детали внутренней работы реализации. Низкоуровневые модели применяют вид белого ящика к анализу программ и полагаются на более низкоуровневые представления приложений смарт-контрактов, такие как следы программы и графики потока управления
, чтобы рассуждать о свойствах, важных для выполнения контракта.
Низкоуровневые модели считаются идеальными, так как они представляют фактическое выполнение смарт-контракта в среде выполнения Ethereum (т. е. EVM). Техники низкоуровневого моделирования особенно полезны для установления критически важных свойств безопасности в смарт-контрактах и выявления потенциальных уязвимостей.
Что такое формальная спецификация?
Спецификация - это просто техническое требование, которому должна удовлетворять определенная система. В программировании спецификации представляют общие идеи о выполнении программы (т. е. что программа должна делать).
В контексте смарт-контрактов формальные спецификации относятся к свойствам - формальным описаниям требований, которым должен удовлетворять контракт. Такие свойства описываются как «инварианты» и представляют собой логические утверждения о выполнении контракта, которые должны оставаться верными в любом возможном случае, без исключений.
Таким образом, мы можем рассматривать формальную спецификацию как совокупность утверждений, написанных на формальном языке, которые описывают предполагаемое выполнение смарт-контракта. Спецификации охватывают свойства контракта и определяют, как контракт должен вести себя в различных обстоятельствах. Цель формальной верификации - определить, обладает ли смарт-контракт этими свойствами (инвариантами) и не нарушаются ли эти свойства во время выполнения.
Формальные спецификации критичны для разработки безопасных реализаций смарт-контрактов. Контракты, которые не реализуют инварианты или нарушают свои свойства во время выполнения, подвержены уязвимостям, которые могут повредить функциональность или вызвать злонамеренные эксплойты.
ТИПЫ ФОРМАЛЬНЫХ СПЕЦИФИКАЦИЙ ДЛЯ СМАРТ-КОНТРАКТОВ
Формальные спецификации позволяют математически рассуждать о правильности выполнения программы. Как и с формальными моделями, формальные спецификации могут захватывать как высокоуровневые свойства, так и низкоуровневое поведение реализации контракта.
Формальные спецификации разрабатываются с использованием элементов логика программы
, которые позволяют формальное рассуждение о свойствах программы. Логика программы имеет формальные правила, которые выражают (на математическом языке) ожидаемое поведение программы. Для создания формальных спецификаций используются различные логики программ, включая логика достижимости
Формальные спецификации для смарт-контрактов можно классифицировать широко как высокоуровневые, так и низкоуровневые спецификации. Независимо от того, к какой категории относится спецификация, она должна должным образом и однозначно описывать свойство системы под анализом.
Спецификации высокого уровня
Как следует из названия, спецификация высокого уровня (также называемая "спецификацией, ориентированной на модель") описывает высокоуровневое поведение программы. Высокоуровневые спецификации моделируют смарт-контракт как конечный автомат
(FSM), который может переходить между состояниями, выполняя операции, с использованием временной логики для определения формальных свойств модели FSM.
Это «правила рассуждения о высказываниях, квалифицированных в терминах времени (например, «Я всегда голоден» или «Я в конечном итоге буду голоден»)». Применительно к формальной верификации временные логики используются для формулирования утверждений о правильном поведении систем, моделируемых как конечные автоматы. Конкретно, временная логика описывает будущие состояния, в которых может находиться смарт-контракт, и то, как он переходит между состояниями.
Общие спецификации обычно охватывают два критических временных свойства для смарт-контрактов: безопасность и живучесть. Свойства безопасности представляют собой идею того, что "никогда не происходит ничего плохого" и обычно выражают неизменность. Свойство безопасности может определять общие требования программного обеспечения, такие как свобода от тупик
, или выражать доменно-специфические свойства для контрактов (например, инварианты на контроль доступа к функциям, допустимые значения переменных состояния или условия для передачи токенов).
Возьмем, к примеру, такое требование безопасности, которое охватывает условия использования transfer() или transferFrom() в контрактах токенов ERC-20: «Баланс отправителя никогда не ниже запрошенного количества токенов для отправки». Это естественноязычное описание инварианта контракта может быть переведено в формальную (математическую) спецификацию, которая затем может быть тщательно проверена на допустимость.
Свойства живучести утверждают, что "в конечном итоге происходит что-то хорошее" и касаются способности контракта продвигаться через различные состояния. Примером свойства живучести является "ликвидность", которая относится к способности контракта переводить свои балансы пользователям по запросу. Если это свойство нарушается, пользователи не смогут вывести активы, хранящиеся в контракте, как произошло с Инцидент кошелька Parity
.
Низкоуровневые спецификации
Спецификации высокого уровня берут за отправную точку конечно-состоянийную модель контракта и определяют желаемые свойства этой модели. В отличие от этого, спецификации низкого уровня (также называемые «ориентированные на свойства спецификации») часто моделируют программы (смарт-контракты) как системы, включающие в себя набор математических функций и описывают правильное поведение таких систем.
Проще говоря, низкоуровневые спецификации анализируют следы программы и пытаются определить свойства смарт-контракта по этим следам. Следы относятся к последовательностям выполнения функций, которые изменяют состояние смарт-контракта; следовательно, низкоуровневые спецификации помогают определить требования к внутреннему выполнению контракта.
Низкоуровневые формальные спецификации могут быть представлены как свойства в стиле Хоара, так и инварианты на путях выполнения.
Свойства стиля Хоара
предоставляет набор формальных правил для рассуждения о корректности программ, включая смарт-контракты. Свойство в стиле Хоара представлено тройкой Хоара {P}c{Q}, где c - это программа, а P и Q - предикаты для состояния c (т.е. программы), формально описанные как предусловия и постусловия соответственно.
Предусловие - это предикат, описывающий условия, необходимые для правильного выполнения функции; пользователи, вызывающие контракт, должны удовлетворять этому требованию. Постусловие - это предикат, описывающий условие, которое функция устанавливает при правильном выполнении; пользователи могут ожидать, что это условие будет верным после вызова функции. Инвариант в логике Хоара - это предикат, который сохраняется выполнением функции (т.е. он не изменяется).
Спецификации в стиле Хоара могут гарантировать как частичную корректность, так и полную корректность. Реализация функции контракта является "частично корректной", если предусловие истинно перед выполнением функции, и если выполнение завершается, постусловие также истинно. Доказательство полной корректности достигается, если предусловие истинно перед выполнением функции, выполнение гарантировано завершится и, когда это произойдет, постусловие также истинно.
Получение доказательства общей правильности сложно, поскольку некоторые исполнения могут задерживаться перед завершением или вообще не завершаться. Тем не менее, вопрос о том, завершается ли исполнение, можно считать спорным, поскольку механизм газа Ethereum предотвращает бесконечные циклы программы (исполнение завершается либо успешно, либо из-за ошибки 'out-of-gas').
Спецификации смарт-контрактов, созданные с использованием логики Хоара, будут иметь предусловия, постусловия и инварианты, определенные для выполнения функций и циклов в контракте. Предусловия часто включают возможность ошибочных входных данных в функцию, с постусловиями, описывающими ожидаемый ответ на такие входы (например, генерация определенного исключения). Таким образом, свойства стиля Хоара эффективны для обеспечения правильности реализации контракта.
Многие формальные верификационные фреймворки используют спецификации в стиле Хоара для доказательства семантической корректности функций. Также можно добавить свойства в стиле Хоара (как утверждения) непосредственно в код контракта, используя операторы require и assert в Solidity.
операторы require выражают предусловие или инвариант и часто используются для проверки ввода пользователя, в то время как assert захватывает постусловие, необходимое для безопасности. Например, правильный контроль доступа к функциям (пример свойства безопасности) можно достичь, используя require в качестве проверки предусловия на идентичность вызывающего аккаунта. Аналогично, инвариант на допустимые значения переменных состояния в контракте (например, общее количество токенов в обращении) можно защитить от нарушений, используя assert для подтверждения состояния контракта после выполнения функции.
Свойства трассировки уровня
Спецификации на основе трассировки описывают операции, которые передают контракт между различными состояниями и связи между этими операциями. Как объяснялось ранее, трассировки — это последовательности операций, которые определенным образом изменяют состояние контракта.
Данный подход основан на модели смарт-контрактов как систем состояний с некоторыми предопределенными состояниями (описываемыми переменными состояния) вместе с набором предопределенных переходов (описываемых функциями контракта). Кроме того, граф потока управления
(CFG), который является графическим представлением потока выполнения программы, часто используется для описания операционной семантики контракта. Здесь каждый след представлен как путь на графе управления потоком.
В основном спецификации на уровне трассировки используются для рассмотрения шаблонов внутреннего выполнения в смарт-контрактах. Создавая спецификации на уровне трассировки, мы утверждаем допустимые пути выполнения (т. е. переходы состояний) для смарт-контракта. Используя такие техники, как символьное выполнение, мы можем формально проверить, что выполнение никогда не следует по пути, не определенному в формальной модели.
Давайте воспользуемся примером DAOконтракт, который имеет некоторые публично доступные функции для описания свойств на уровне трассировки. Здесь мы предполагаем, что контракт DAO позволяет пользователям выполнять следующие операции:
- Пополнить средства
- Проголосуйте за предложение после внесения средств
- Получите возврат средств, если они не проголосуют по предложению
Примером свойств уровня трассировки могут быть «пользователи, не вносящие средства, не могут голосовать за предложение» или «пользователи, не голосующие за предложение, всегда должны иметь возможность требовать возврата». Оба свойства утверждают предпочтительные последовательности выполнения (голосование не может произойти до внесения средств, а возвраты не могут произойти после голосования за предложение).
МЕТОДЫ ФОРМАЛЬНОЙ ПРОВЕРКИ СМАРТ-КОНТРАКТОВ
Проверка модели
Проверка модели - это формальный метод верификации, при котором алгоритм проверяет формальную модель смарт-контракта на соответствие его спецификации. При проверке модели смарт-контракты часто представлены в виде систем перехода состояний, в то время как свойства допустимых состояний контракта определяются с использованием временной логики.
Для модельной проверки требуется создание абстрактного математического представления системы (т. е. контракта) и выражение свойств этой системы с использованием формул, основанных на Пропозициональная логика
. Это упрощает задачу алгоритма проверки модели, а именно доказательство того, что математическая модель удовлетворяет заданной логической формуле.
Модельная проверка в формальной верификации в основном используется для оценки временных свойств, описывающих поведение контракта со временем. Временные свойства для смарт-контрактов включают в себя безопасность и живость, о которых мы ранее объясняли.
Например, свойство безопасности, относящееся к управлению доступом (например, Только владелец контракта может вызывать самоуничтожение), может быть записано в формальной логике. После этого алгоритм проверки модели может проверить, удовлетворяет ли контракт этой формальной спецификации.
Model checking использует исследование пространства состояний, которое включает в себя построение всех возможных состояний смарт-контракта и попытки найти достижимые состояния, приводящие к нарушению свойств. Однако это может привести к бесконечному количеству состояний (известному как "проблема взрыва состояний"), поэтому модельные проверяющие полагаются на техники абстракции, чтобы обеспечить эффективный анализ смарт-контрактов.
Доказательство теоремы
Доказательство теорем - это метод математического рассуждения о корректности программ, включая смарт-контракты. Он включает в себя преобразование модели системы контракта и его спецификаций в математические формулы (логические выражения).
Целью доказательства теоремы является проверка логического эквивалентности между этими утверждениями. «Логическое эквивалентность» (также называемое «логической двусторонней импликацией») - это тип отношения между двумя утверждениями, таким образом, что первое утверждение истинно тогда и только тогда, когда второе утверждение истинно.
Необходимое отношение (логическое эквивалентное) между высказываниями о модели контракта и его свойстве формулируется как доказуемое высказывание (называемое теоремой). С использованием формальной системы вывода автоматизированный доказатель теорем может проверить правильность теоремы. Другими словами, доказатель теоремы может окончательно доказать, что модель смарт-контракта точно соответствует его спецификациям.
При проверке моделей моделируют контракты как конечные системы состояний, теоремы могут обрабатывать анализ систем с бесконечным числом состояний. Однако это означает, что автоматизированный доказатель не всегда может знать, является ли логическая проблема "разрешимой" или нет.
В результате часто требуется человеческая помощь для направления доказательства теоремы в выводе доказательств о корректности. Использование человеческих усилий в доказательстве теорем делает его более дорогостоящим в использовании, чем проверка модели, которая полностью автоматизирована.
Символическое выполнение
Символическое выполнение - это метод анализа смарт-контракта путем выполнения функций с использованием символьных значений (например, x > 5) вместо конкретных значений (например, x == 5). Как техника формальной верификации, символическое выполнение используется для формального рассмотрения свойств на уровне трассировки в коде контракта.
Символическое выполнение представляет собой след выполнения в виде математической формулы над символическими входными значениями, иначе называемой предикатом пути. SMT решатель
используется для проверки того, является ли предикат пути "удовлетворимым" (т. е. существует значение, которое может удовлетворить формулу). Если уязвимый путь удовлетворим, решатель SMT сгенерирует конкретное значение, которое запускает выполнение в направлении этого пути.
Предположим, что функция смарт-контракта принимает в качестве входных данных значение uint (x) и отменяется, когда x больше 5, а также меньше 10. Чтобы найти значение x, которое вызывает ошибку, с помощью обычной процедуры тестирования потребовалось бы пройти десятки тестовых случаев (или больше) без уверенности в том, что вы действительно найдете входные данные, вызывающие ошибку.
С другой стороны, инструмент символьного выполнения выполнял бы функцию с символьным значением: X > 5 ∧ X < 10 (т. Е. x больше 5 И x меньше 10). Связанный с путевым предикатом x = X > 5 ∧ X < 10 затем будет передан решателю SMT для решения. Если определенное значение удовлетворяет формуле x = X > 5 ∧ X < 10, решатель SMT его вычислит, например, решатель может получить 7 в качестве значения для x.
Поскольку символьное выполнение зависит от входных данных программы, и набор входных данных для исследования всех достижимых состояний потенциально бесконечен, это по-прежнему является формой тестирования. Однако, как показано в примере, символьное выполнение эффективнее обычного тестирования при поиске входных данных, вызывающих нарушения свойств.
Кроме того, символьное выполнение создает меньше ложных срабатываний, чем другие техники, основанные на свойствах (например, fuzzing), которые случайным образом генерируют входные данные для функции. Если во время символьного выполнения возникает состояние ошибки, то возможно сгенерировать конкретное значение, вызывающее ошибку, и воспроизвести проблему.
Символическое выполнение также может обеспечить определенную степень математического доказательства корректности. Рассмотрим следующий пример функции контракта с защитой от переполнения:
Трассировка выполнения, которая приводит к переполнению целого числа, должна удовлетворять формуле: z = x + y И (z >= x) И (z=>y) И (z < x ИЛИ z < y) Такая формула вряд ли будет решена, поэтому она служит математическим доказательством того, что функция safe_add никогда не приводит к переполнению.
Зачем использовать формальную верификацию для смарт-контрактов?
Необходимость надежности
Формальная верификация используется для оценки правильности систем, критически важных для безопасности, отказ которых может иметь разрушительные последствия, такие как смерть, травмы или финансовая разруха. Смарт-контракты - это приложения высокой ценности, контролирующие огромные суммы ценности, и простые ошибки в проектировании могут привести к невозместимые потери для пользователей
Формальная верификация контракта перед развертыванием, однако, может увеличить гарантии того, что он будет работать ожидаемым образом после запуска на блокчейне.
Надежность - это очень желаемое качество в любом смарт-контракте, особенно потому, что код, развернутый в виртуальной машине Ethereum (EVM), как правило, является неизменяемым. С учетом того, что обновления после запуска не доступны, необходимость гарантировать надежность контрактов делает формальную верификацию необходимой. Формальная верификация способна обнаруживать сложные проблемы, такие как недостаток и переполнение целых чисел, рекурсию и плохую оптимизацию газа, которые могут ускользнуть от аудиторов и тестировщиков.
Доказать функциональную правильность
Тестирование программ - самый распространенный метод подтверждения того, что смарт-контракт удовлетворяет определенным требованиям. Это включает выполнение контракта с образцом данных, которые от него ожидаются, и анализ его поведения. Если контракт возвращает ожидаемые результаты для образцовых данных, то разработчики имеют объективное доказательство его корректности.
Однако такой подход не может доказать правильность выполнения входных значений, которые не являются частью выборки. Таким образом, тестирование контракта может помочь обнаружить ошибки (например, если некоторые пути кода не возвращают желаемые результаты во время выполнения), но оно не может окончательно доказать отсутствие ошибок.
И наоборот, формальная проверка может формально доказать, что смарт-контракт удовлетворяет требованиям для бесконечного диапазона исполнений вообще без запуска контракта. Для этого необходимо создать формальную спецификацию, которая точно описывает правильное поведение контракта, и разработать формальную (математическую) модель контрактной системы. Затем мы можем следовать формальной процедуре доказательства, чтобы проверить согласованность между моделью контракта и его спецификацией.
С формальной верификацией вопрос о проверке того, удовлетворяет ли бизнес-логика контракта требования, является математическим предложением, которое можно доказать или опровергнуть. Формально доказывая предложение, мы можем проверить бесконечное количество тестовых случаев с конечным числом шагов. Таким образом, формальная верификация имеет более хорошие перспективы доказать, что контракт функционально корректен относительно спецификации.
Целевые объекты верификации идеальны
Целевая верификация описывает систему, которая должна быть формально проверена. Формальная верификация наилучшим образом применяется в «встроенных системах» (небольшие, простые программные компоненты, являющиеся частью более крупной системы). Они также идеально подходят для специализированных областей, в которых мало правил, что упрощает модификацию инструментов для проверки свойств, специфичных для области.
Смарт-контракты, по крайней мере, частично, удовлетворяют оба требования. Например, небольшой размер контрактов Ethereum делает их пригодными для формальной верификации. Точно так же EVM следует простым правилам, что упрощает указание и проверку семантических свойств для программ, запускаемых в EVM.
Быстрый цикл разработки
Техники формальной верификации, такие как проверка модели и символьное выполнение, обычно более эффективны, чем обычный анализ кода смарт-контракта (проводимый во время тестирования или аудита). Это потому, что формальная верификация полагается на символьные значения для проверки утверждений («что, если пользователь попытается вывести n эфиров?»), в отличие от тестирования, которое использует конкретные значения («что, если пользователь попытается вывести 5 эфиров?»).
Символические входные переменные могут охватывать несколько классов конкретных значений, поэтому методы формальной верификации обещают больший охват кода за более короткий промежуток времени. При эффективном использовании формальная верификация может ускорить цикл разработки для разработчиков.
Формальная верификация также улучшает процесс создания децентрализованных приложений (dapps), уменьшая дорогостоящие ошибки проектирования. Обновление контрактов (где это возможно) для исправления уязвимостей требует обширного переписывания кодовых баз и большего усилия, затраченного на разработку. Формальная верификация может обнаружить множество ошибок в реализации контрактов, которые могут ускользнуть от тестировщиков и аудиторов, и предоставляет достаточно возможностей для устранения этих проблем перед развертыванием контракта.
НЕДОСТАТКИ ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ
Стоимость ручного труда
Формальная верификация, особенно полуавтоматизированная верификация, при которой человек направляет доказательство для вывода доказательств правильности, требует значительного количества ручного труда. Более того, создание формальной спецификации - это сложная деятельность, требующая высокого уровня навыков.
Эти факторы (усилие и навык) делают формальную верификацию более требовательной и дорогостоящей по сравнению с обычными методами оценки правильности в контрактах, такими как тестирование и проверки. Тем не менее, оплата стоимости полного аудита верификации практична, учитывая стоимость ошибок в реализации смарт-контрактов.
Ложноотрицательные
Формальная верификация может проверить только соответствие выполнения смарт-контракта формальной спецификации. Поэтому важно убедиться, что спецификация правильно описывает ожидаемое поведение смарт-контракта.
Если спецификации написаны плохо, нарушения свойств, указывающие на уязвимые исполнения, не могут быть обнаружены при формальной проверке аудита. В этом случае разработчик может ошибочно предположить, что контракт свободен от ошибок.
Проблемы производительности
При формальной верификации возникает ряд проблем производительности. Например, проблемы взрыва состояний и путей, возникающие при проверке моделей и символьной проверке соответственно, могут повлиять на процедуры верификации. Кроме того, инструменты формальной верификации часто используют SMT-решатели и другие решатели ограничений на своем нижнем уровне, и эти решатели полагаются на вычислительно интенсивные процедуры.
Кроме того, не всегда возможно для верификаторов программ определить, может ли свойство (описанное как логическая формула) быть удовлетворено или нет ("проблема разрешимости
потому что программа может никогда не завершиться. Таким образом, некоторые свойства контракта могут быть невозможно доказать, даже если он хорошо специфицирован.
Инструменты формальной верификации для смарт-контрактов Ethereum
Языки спецификации для создания формальных спецификаций
Act: Act позволяет указывать обновления хранилища, предусловия/постусловия и инварианты контракта. Его инструментальный набор также имеет поддержку доказательств, способных доказать множество свойств с помощью Coq, SMT-солверов или hevm.
Scribble - Scribble преобразует аннотации кода на языке спецификации Scribble в конкретные утверждения, которые проверяют спецификацию.
Dafny - Dafny - это язык программирования, готовый к верификации, который полагается на высокоуровневые аннотации для рассуждения о правильности кода и его доказательства.
Проверщики программ для проверки корректности
Certora Prover - Certora Prover - это автоматический инструмент формальной верификации для проверки правильности кода в смарт-контрактах. Спецификации написаны на CVL (Certora Verification Language), а нарушения свойств обнаруживаются с использованием комбинации статического анализа и решения ограничений.
Solidity SMTChecker - SMTChecker от Solidity - это встроенная программа проверки моделей, основанная на SMT (теориях выполнимости по модулю) и решении по Хорну. Он подтверждает, соответствует ли исходный код контракта спецификациям во время компиляции, и статически проверяет на наличие нарушений свойств безопасности.
solc-verify - solc-verify - это расширенная версия компилятора Solidity, которая может выполнять автоматизированную формальную верификацию кода Solidity с использованием аннотаций и модульной верификации программы.
KEVM - KEVM - это формальная семантика виртуальной машины Ethereum (EVM), написанная на платформе K. KEVM является исполняемым и может доказать определенные утверждения, связанные с свойствами, с использованием логики достижимости.
Логические фреймворки для доказательства теорем
Изабель - Изабель/HOL - это помощник по доказательствам, который позволяет выражать математические формулы формальным языком и предоставляет инструменты для доказательства этих формул. Основное применение - формализация математических доказательств, в частности формальная верификация, которая включает в себя доказательство правильности компьютерного оборудования или программного обеспечения и доказательство свойств компьютерных языков и протоколов.
Coq - Coq - это интерактивный доказательственный механизм, который позволяет вам определять программы с использованием теорем и интерактивно генерировать машинно-проверенные доказательства корректности.
Инструменты на основе символьного выполнения для обнаружения уязвимых шаблонов в смарт-контрактах
Manticore - инструмент для анализа байткода EVM на основе символьного выполнения.
hevm - hevm - это механизм символьного выполнения и проверка эквивалентности байт-кода EVM.
Mythril - инструмент символьного выполнения для обнаружения уязвимостей в умных контрактах Ethereum
Отказ от ответственности:
- Эта статья перепечатана с [ ]. Все авторские права принадлежат оригинальному автору [**]. Если есть возражения по поводу этого перепечатывания, пожалуйста, свяжитесь с Gate Learnкоманда, и они незамедлительно справятся с этим.
- Ответственность за отказ: Взгляды и мнения, высказанные в этой статье, являются исключительно точкой зрения автора и не являются инвестиционными советами.
- Переводы статьи на другие языки выполняются командой Gate Learn. Если не указано иное, копирование, распространение или плагиат переведенных статей запрещены.
Bài viết liên quan
Что такое Neiro? Все, что вам нужно знать о NEIROETH
Лучшие криптовалютные лотерейные платформы на 2024 год