Перейти к основному контенту
Change page

Формальная верификация смарт-контрактов

Смарт-контракты позволяют создавать децентрализованные, не требующие доверия и надежные приложения, которые открывают новые варианты использования и приносят пользу пользователям. Поскольку смарт-контракты управляют большими объемами средств, безопасность является критически важным аспектом для разработчиков.

Формальная верификация — один из рекомендуемых методов повышения безопасности смарт-контрактов. Формальная верификация, использующая формальные методы (opens in a new tab) для спецификации, проектирования и проверки программ, уже много лет применяется для обеспечения корректности критически важных аппаратных и программных систем.

При применении к смарт-контрактам формальная верификация может доказать, что бизнес-логика контракта соответствует заранее определенной спецификации. По сравнению с другими методами оценки корректности кода контракта, такими как тестирование, формальная верификация дает более надежные гарантии того, что смарт-контракт функционально корректен.

Что такое формальная верификация?

Формальная верификация — это процесс оценки корректности системы по отношению к формальной спецификации. Проще говоря, формальная верификация позволяет нам проверить, удовлетворяет ли поведение системы определенным требованиям (т. е. делает ли она то, что мы хотим).

Ожидаемое поведение системы (в данном случае смарт-контракта) описывается с помощью формального моделирования, а языки спецификаций позволяют создавать формальные свойства. Затем методы формальной верификации могут проверить, соответствует ли реализация контракта его спецификации, и получить математическое доказательство корректности реализации. Когда контракт удовлетворяет своей спецификации, он описывается как «функционально корректный», «корректный по проекту» (correct by design) или «корректный по построению» (correct by construction).

Что такое формальная модель?

В информатике формальная модель (opens in a new tab) — это математическое описание вычислительного процесса. Программы абстрагируются в математические функции (уравнения), при этом модель описывает, как вычисляются выходные данные функций на основе входных данных.

Формальные модели обеспечивают уровень абстракции, на котором можно оценивать анализ поведения программы. Существование формальных моделей позволяет создать формальную спецификацию, которая описывает желаемые свойства рассматриваемой модели.

Для моделирования смарт-контрактов в целях формальной верификации используются различные методы. Например, некоторые модели используются для рассуждений о высокоуровневом поведении смарт-контракта. Эти методы моделирования применяют к смарт-контрактам подход «черного ящика», рассматривая их как системы, которые принимают входные данные и выполняют вычисления на их основе.

Высокоуровневые модели фокусируются на взаимосвязи между смарт-контрактами и внешними агентами, такими как внешне принадлежащие аккаунты (EOA), аккаунты контрактов и среда блокчейна. Такие модели полезны для определения свойств, которые указывают, как контракт должен вести себя в ответ на определенные взаимодействия с пользователем.

И наоборот, другие формальные модели фокусируются на низкоуровневом поведении смарт-контракта. Хотя высокоуровневые модели могут помочь в рассуждениях о функциональности контракта, они могут не уловить детали внутреннего устройства реализации. Низкоуровневые модели применяют подход «белого ящика» к анализу программ и опираются на низкоуровневые представления приложений смарт-контрактов, такие как трассы программ и графы потока управления (opens in a new tab), для рассуждений о свойствах, относящихся к выполнению контракта.

Низкоуровневые модели считаются идеальными, поскольку они представляют фактическое выполнение смарт-контракта в среде выполнения Эфириума (т. е. в EVM). Методы низкоуровневого моделирования особенно полезны для установления критических свойств безопасности в смарт-контрактах и обнаружения потенциальных уязвимостей.

Что такое формальная спецификация?

Спецификация — это просто техническое требование, которому должна удовлетворять конкретная система. В программировании спецификации представляют собой общие идеи о выполнении программы (т. е. о том, что программа должна делать).

В контексте смарт-контрактов формальные спецификации относятся к свойствам — формальным описаниям требований, которым должен удовлетворять контракт. Такие свойства описываются как «инварианты» и представляют собой логические утверждения о выполнении контракта, которые должны оставаться истинными при любых возможных обстоятельствах, без каких-либо исключений.

Таким образом, мы можем рассматривать формальную спецификацию как набор утверждений, написанных на формальном языке, которые описывают предполагаемое выполнение смарт-контракта. Спецификации охватывают свойства контракта и определяют, как контракт должен вести себя в различных обстоятельствах. Цель формальной верификации — определить, обладает ли смарт-контракт этими свойствами (инвариантами) и не нарушаются ли эти свойства во время выполнения.

Формальные спецификации имеют решающее значение при разработке безопасных реализаций смарт-контрактов. Контракты, которые не реализуют инварианты или свойства которых нарушаются во время выполнения, подвержены уязвимостям, которые могут нанести ущерб функциональности или стать причиной злонамеренных эксплойтов.

Типы формальных спецификаций для смарт-контрактов

Формальные спецификации позволяют математически рассуждать о корректности выполнения программы. Как и в случае с формальными моделями, формальные спецификации могут фиксировать либо высокоуровневые свойства, либо низкоуровневое поведение реализации контракта.

Формальные спецификации выводятся с использованием элементов логики программ (opens in a new tab), которые позволяют формально рассуждать о свойствах программы. Логика программ имеет формальные правила, которые выражают (на математическом языке) ожидаемое поведение программы. При создании формальных спецификаций используются различные логики программ, включая логику достижимости (opens in a new tab), темпоральную логику (opens in a new tab) и логику Хоара (opens in a new tab).

Формальные спецификации для смарт-контрактов можно в общих чертах классифицировать как высокоуровневые или низкоуровневые спецификации. Независимо от того, к какой категории относится спецификация, она должна адекватно и недвусмысленно описывать свойство анализируемой системы.

Высокоуровневые спецификации

Как следует из названия, высокоуровневая спецификация (также называемая «модельно-ориентированной спецификацией») описывает высокоуровневое поведение программы. Высокоуровневые спецификации моделируют смарт-контракт как конечный автомат (opens in a new tab) (FSM), который может переходить между состояниями путем выполнения операций, при этом темпоральная логика используется для определения формальных свойств модели FSM.

Темпоральные логики (opens in a new tab) — это «правила для рассуждений об утверждениях, квалифицируемых с точки зрения времени (например, "я всегда голоден" или "в конечном итоге я проголодаюсь")». Применительно к формальной верификации темпоральные логики используются для формулирования утверждений о правильном поведении систем, смоделированных как конечные автоматы. В частности, темпоральная логика описывает будущие состояния, в которых может находиться смарт-контракт, и то, как он переходит между состояниями.

Высокоуровневые спецификации обычно фиксируют два критических темпоральных свойства для смарт-контрактов: безопасность (safety) и живучесть (liveness). Свойства безопасности представляют собой идею о том, что «ничего плохого никогда не происходит», и обычно выражают инвариантность. Свойство безопасности может определять общие требования к программному обеспечению, такие как отсутствие взаимных блокировок (opens in a new tab) (deadlocks), или выражать специфичные для предметной области свойства контрактов (например, инварианты контроля доступа для функций, допустимые значения переменных состояния или условия для переводов токенов).

Возьмем, к примеру, это требование безопасности, которое охватывает условия использования transfer() или transferFrom() в контрактах токенов ERC-20: «Баланс отправителя никогда не бывает ниже запрошенного количества токенов для отправки». Это описание инварианта контракта на естественном языке может быть переведено в формальную (математическую) спецификацию, которая затем может быть строго проверена на достоверность.

Свойства живучести утверждают, что «в конечном итоге происходит что-то хорошее», и касаются способности контракта продвигаться через различные состояния. Примером свойства живучести является «ликвидность», которая относится к способности контракта переводить свои балансы пользователям по запросу. Если это свойство нарушено, пользователи не смогут вывести активы, хранящиеся в контракте, как это произошло в случае с инцидентом с кошельком Parity (opens in a new tab).

Низкоуровневые спецификации

Высокоуровневые спецификации берут за отправную точку конечно-автоматную модель контракта и определяют желаемые свойства этой модели. В отличие от них, низкоуровневые спецификации (также называемые «свойство-ориентированными спецификациями») часто моделируют программы (смарт-контракты) как системы, состоящие из набора математических функций, и описывают правильное поведение таких систем.

Проще говоря, низкоуровневые спецификации анализируют трассы программы и пытаются определить свойства смарт-контракта на основе этих трасс. Трассы относятся к последовательностям выполнений функций, которые изменяют состояние смарт-контракта; следовательно, низкоуровневые спецификации помогают определить требования к внутреннему выполнению контракта.

Низкоуровневые формальные спецификации могут быть заданы либо как свойства в стиле Хоара, либо как инварианты на путях выполнения.

Свойства в стиле Хоара

Логика Хоара (opens in a new tab) предоставляет набор формальных правил для рассуждений о корректности программ, включая смарт-контракты. Свойство в стиле Хоара представлено тройкой Хоара {P}c{Q}, где c — это программа, а P и Q — предикаты состояния c (т. е. программы), формально описываемые как предусловия и постусловия соответственно.

Предусловие — это предикат, описывающий условия, необходимые для правильного выполнения функции; пользователи, вызывающие контракт, должны удовлетворять этому требованию. Постусловие — это предикат, описывающий условие, которое функция устанавливает при правильном выполнении; пользователи могут ожидать, что это условие будет истинным после вызова функции. Инвариант в логике Хоара — это предикат, который сохраняется при выполнении функции (т. е. он не изменяется).

Спецификации в стиле Хоара могут гарантировать либо частичную корректность, либо полную корректность. Реализация функции контракта «частично корректна», если предусловие истинно до выполнения функции, и если выполнение завершается, постусловие также истинно. Доказательство полной корректности получается, если предусловие истинно до выполнения функции, выполнение гарантированно завершается, и когда это происходит, постусловие истинно.

Получить доказательство полной корректности сложно, поскольку некоторые выполнения могут задерживаться перед завершением или вообще никогда не завершаться. Тем не менее, вопрос о том, завершается ли выполнение, возможно, является спорным, поскольку механизм газа Эфириума предотвращает бесконечные циклы программы (выполнение завершается либо успешно, либо заканчивается из-за ошибки «нехватки газа»).

Спецификации смарт-контрактов, созданные с использованием логики Хоара, будут иметь предусловия, постусловия и инварианты, определенные для выполнения функций и циклов в контракте. Предусловия часто включают возможность ошибочных входных данных для функции, а постусловия описывают ожидаемую реакцию на такие входные данные (например, выдачу определенного исключения). Таким образом, свойства в стиле Хоара эффективны для обеспечения корректности реализаций контрактов.

Многие фреймворки формальной верификации используют спецификации в стиле Хоара для доказательства семантической корректности функций. Также возможно добавлять свойства в стиле Хоара (в качестве утверждений) непосредственно в код контракта, используя операторы require и assert в Solidity.

Операторы require выражают предусловие или инвариант и часто используются для проверки пользовательского ввода, в то время как assert фиксирует постусловие, необходимое для безопасности. Например, надлежащий контроль доступа для функций (пример свойства безопасности) может быть достигнут с использованием require в качестве проверки предусловия личности вызывающего аккаунта. Аналогичным образом, инвариант допустимых значений переменных состояния в контракте (например, общее количество токенов в обращении) может быть защищен от нарушения с помощью assert для подтверждения состояния контракта после выполнения функции.

Свойства на уровне трасс

Спецификации на основе трасс описывают операции, которые переводят контракт между различными состояниями, и взаимосвязи между этими операциями. Как объяснялось ранее, трассы — это последовательности операций, которые определенным образом изменяют состояние контракта.

Этот подход опирается на модель смарт-контрактов как систем переходов состояний с некоторыми предопределенными состояниями (описываемыми переменными состояния) вместе с набором предопределенных переходов (описываемых функциями контракта). Кроме того, для описания операционной семантики контракта часто используется граф потока управления (opens in a new tab) (CFG), который представляет собой графическое представление потока выполнения программы. Здесь каждая трасса представлена как путь на графе потока управления.

В первую очередь спецификации на уровне трасс используются для рассуждений о шаблонах внутреннего выполнения в смарт-контрактах. Создавая спецификации на уровне трасс, мы утверждаем допустимые пути выполнения (т. е. переходы состояний) для смарт-контракта. Используя такие методы, как символьное выполнение, мы можем формально проверить, что выполнение никогда не следует по пути, не определенному в формальной модели.

Давайте используем пример контракта DAO, который имеет некоторые общедоступные функции, чтобы описать свойства на уровне трасс. Здесь мы предполагаем, что контракт DAO позволяет пользователям выполнять следующие операции:

  • Вносить средства

  • Голосовать за предложение после внесения средств

  • Востребовать возврат средств, если они не голосуют за предложение

Примерами свойств на уровне трасс могут быть «пользователи, которые не вносят средства, не могут голосовать за предложение» или «пользователи, которые не голосуют за предложение, всегда должны иметь возможность востребовать возврат средств». Оба свойства утверждают предпочтительные последовательности выполнения (голосование не может произойти до внесения средств, а востребование возврата средств не может произойти после голосования за предложение).

Методы формальной верификации смарт-контрактов

Проверка моделей

Проверка моделей (model checking) — это метод формальной верификации, при котором алгоритм проверяет формальную модель смарт-контракта на соответствие ее спецификации. При проверке моделей смарт-контракты часто представляются как системы переходов состояний, в то время как свойства допустимых состояний контракта определяются с использованием темпоральной логики.

Проверка моделей требует создания абстрактного математического представления системы (т. е. контракта) и выражения свойств этой системы с использованием формул, основанных на пропозициональной логике (opens in a new tab). Это упрощает задачу алгоритма проверки моделей, а именно доказательство того, что математическая модель удовлетворяет заданной логической формуле.

Проверка моделей в формальной верификации в первую очередь используется для оценки темпоральных свойств, которые описывают поведение контракта с течением времени. Темпоральные свойства для смарт-контрактов включают безопасность и живучесть, которые мы объяснили ранее.

Например, свойство безопасности, связанное с контролем доступа (например, Только владелец контракта может вызывать selfdestruct), может быть записано в формальной логике. После этого алгоритм проверки моделей может проверить, удовлетворяет ли контракт этой формальной спецификации.

Проверка моделей использует исследование пространства состояний, которое включает в себя построение всех возможных состояний смарт-контракта и попытку найти достижимые состояния, которые приводят к нарушениям свойств. Однако это может привести к бесконечному количеству состояний (известному как «проблема взрыва состояний»), поэтому средства проверки моделей полагаются на методы абстракции, чтобы сделать возможным эффективный анализ смарт-контрактов.

Доказательство теорем

Доказательство теорем — это метод математического рассуждения о корректности программ, включая смарт-контракты. Он включает в себя преобразование модели системы контракта и ее спецификаций в математические формулы (логические утверждения).

Цель доказательства теорем — проверить логическую эквивалентность между этими утверждениями. «Логическая эквивалентность» (также называемая «логической биимпликацией») — это тип отношения между двумя утверждениями, при котором первое утверждение истинно тогда и только тогда, когда истинно второе утверждение.

Требуемое отношение (логическая эквивалентность) между утверждениями о модели контракта и его свойстве формулируется как доказуемое утверждение (называемое теоремой). Используя формальную систему вывода, автоматизированный прувер теорем может проверить достоверность теоремы. Другими словами, прувер теорем может убедительно доказать, что модель смарт-контракта точно соответствует его спецификациям.

В то время как проверка моделей моделирует контракты как системы переходов с конечными состояниями, доказательство теорем может справляться с анализом систем с бесконечным числом состояний. Однако это означает, что автоматизированный прувер теорем не всегда может знать, является ли логическая проблема «разрешимой» или нет.

В результате часто требуется помощь человека, чтобы направлять прувер теорем в получении доказательств корректности. Использование человеческих усилий в доказательстве теорем делает его более дорогим в использовании, чем проверка моделей, которая полностью автоматизирована.

Символьное выполнение

Символьное выполнение — это метод анализа смарт-контракта путем выполнения функций с использованием символьных значений (например, x > 5) вместо конкретных значений (например, x == 5). В качестве метода формальной верификации символьное выполнение используется для формального рассуждения о свойствах на уровне трасс в коде контракта.

Символьное выполнение представляет трассу выполнения как математическую формулу над символьными входными значениями, иначе называемую предикатом пути. SMT-солвер (opens in a new tab) используется для проверки того, является ли предикат пути «выполнимым» (т. е. существует ли значение, которое может удовлетворить формуле). Если уязвимый путь выполним, 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.

Поскольку символьное выполнение опирается на входные данные программы, а набор входных данных для исследования всех достижимых состояний потенциально бесконечен, это все еще форма тестирования. Однако, как показано в примере, символьное выполнение более эффективно, чем обычное тестирование, для поиска входных данных, которые вызывают нарушения свойств.

Более того, символьное выполнение дает меньше ложных срабатываний, чем другие методы на основе свойств (например, фаззинг), которые случайным образом генерируют входные данные для функции. Если во время символьного выполнения запускается состояние ошибки, то можно сгенерировать конкретное значение, которое вызывает ошибку, и воспроизвести проблему.

Символьное выполнение также может обеспечить некоторую степень математического доказательства корректности. Рассмотрим следующий пример функции контракта с защитой от переполнения:

function safe_add(uint x, uint y) returns(uint z){

  z = x + y;
  require(z>=x);
  require(z>=y);

  return z;
}

Трасса выполнения, которая приводит к целочисленному переполнению, должна была бы удовлетворять формуле: z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y) Такая формула вряд ли будет решена, следовательно, она служит математическим доказательством того, что функция safe_add никогда не вызывает переполнения.

Зачем использовать формальную верификацию для смарт-контрактов?

Потребность в надежности

Формальная верификация используется для оценки корректности критически важных для безопасности систем, отказ которых может иметь разрушительные последствия, такие как смерть, травмы или финансовый крах. Смарт-контракты — это ценные приложения, контролирующие огромные объемы средств, и простые ошибки в проектировании могут привести к безвозвратным потерям для пользователей (opens in a new tab). Однако формальная верификация контракта перед развертыванием может повысить гарантии того, что он будет работать так, как ожидается, после запуска в блокчейне.

Надежность — это весьма желательное качество любого смарт-контракта, особенно потому, что код, развернутый в виртуальной машине Эфириума (EVM), обычно является неизменяемым. Поскольку обновления после запуска не всегда легкодоступны, необходимость гарантировать надежность контрактов делает формальную верификацию необходимой. Формальная верификация способна обнаруживать сложные проблемы, такие как целочисленные недополнения и переполнения, повторный вход (re-entrancy) и плохая оптимизация газа, которые могут ускользнуть от внимания аудиторов и тестировщиков.

Доказательство функциональной корректности

Тестирование программы — наиболее распространенный метод доказательства того, что смарт-контракт удовлетворяет некоторым требованиям. Это включает в себя выполнение контракта с выборкой данных, которые он должен обрабатывать, и анализ его поведения. Если контракт возвращает ожидаемые результаты для выборочных данных, то у разработчиков есть объективное доказательство его корректности.

Однако этот подход не может доказать правильное выполнение для входных значений, которые не являются частью выборки. Поэтому тестирование контракта может помочь обнаружить ошибки (т. е. если некоторые пути кода не возвращают желаемых результатов во время выполнения), но оно не может убедительно доказать отсутствие ошибок.

И наоборот, формальная верификация может формально доказать, что смарт-контракт удовлетворяет требованиям для бесконечного диапазона выполнений без запуска контракта вообще. Это требует создания формальной спецификации, которая точно описывает правильное поведение контракта, и разработки формальной (математической) модели системы контракта. Затем мы можем следовать процедуре формального доказательства, чтобы проверить согласованность между моделью контракта и его спецификацией.

При формальной верификации вопрос проверки того, удовлетворяет ли бизнес-логика контракта требованиям, является математическим утверждением, которое можно доказать или опровергнуть. Формально доказывая утверждение, мы можем проверить бесконечное количество тестовых случаев за конечное число шагов. Таким образом, формальная верификация имеет лучшие перспективы для доказательства того, что контракт функционально корректен по отношению к спецификации.

Идеальные цели для верификации

Цель верификации описывает систему, которая должна быть формально верифицирована. Формальную верификацию лучше всего использовать во «встроенных системах» (небольших, простых частях программного обеспечения, которые являются частью более крупной системы). Они также идеально подходят для специализированных областей, в которых мало правил, поскольку это упрощает модификацию инструментов для проверки свойств, специфичных для предметной области.

Смарт-контракты — по крайней мере, в некоторой степени — удовлетворяют обоим требованиям. Например, небольшой размер контрактов Эфириума делает их поддающимися формальной верификации. Аналогичным образом, EVM следует простым правилам, что упрощает спецификацию и проверку семантических свойств для программ, работающих в EVM.

Ускоренный цикл разработки

Методы формальной верификации, такие как проверка моделей и символьное выполнение, как правило, более эффективны, чем обычный анализ кода смарт-контракта (выполняемый во время тестирования или аудита). Это связано с тем, что формальная верификация опирается на символьные значения для проверки утверждений («что, если пользователь попытается вывести n эфира?»), в отличие от тестирования, в котором используются конкретные значения («что, если пользователь попытается вывести 5 эфира?»).

Символьные входные переменные могут охватывать несколько классов конкретных значений, поэтому подходы формальной верификации обещают большее покрытие кода за более короткие сроки. При эффективном использовании формальная верификация может ускорить цикл разработки для разработчиков.

Формальная верификация также улучшает процесс создания децентрализованных приложений (dapp) за счет сокращения дорогостоящих ошибок проектирования. Обновление контрактов (где это возможно) для исправления уязвимостей требует обширного переписывания кодовых баз и больших усилий, затрачиваемых на разработку. Формальная верификация может обнаружить множество ошибок в реализациях контрактов, которые могут ускользнуть от тестировщиков и аудиторов, и предоставляет широкие возможности для исправления этих проблем перед развертыванием контракта.

Недостатки формальной верификации

Затраты на ручной труд

Формальная верификация, особенно полуавтоматическая верификация, при которой человек направляет прувер для получения доказательств корректности, требует значительного ручного труда. Более того, создание формальной спецификации — это сложная деятельность, требующая высокого уровня квалификации.

Эти факторы (усилия и навыки) делают формальную верификацию более требовательной и дорогой по сравнению с обычными методами оценки корректности контрактов, такими как тестирование и аудит. Тем не менее, оплата полного аудита верификации практична, учитывая стоимость ошибок в реализациях смарт-контрактов.

Ложноотрицательные результаты

Формальная верификация может только проверить, соответствует ли выполнение смарт-контракта формальной спецификации. Поэтому важно убедиться, что спецификация должным образом описывает ожидаемое поведение смарт-контракта.

Если спецификации написаны плохо, нарушения свойств, которые указывают на уязвимые выполнения, не могут быть обнаружены аудитом формальной верификации. В этом случае разработчик может ошибочно предположить, что в контракте нет ошибок.

Проблемы с производительностью

Формальная верификация сталкивается с рядом проблем с производительностью. Например, проблемы взрыва состояний и путей, возникающие во время проверки моделей и символьной проверки соответственно, могут повлиять на процедуры верификации. Кроме того, инструменты формальной верификации часто используют SMT-солверы и другие солверы ограничений на своем базовом уровне, и эти солверы полагаются на вычислительно интенсивные процедуры.

Кроме того, верификаторы программ не всегда могут определить, может ли свойство (описанное как логическая формула) быть удовлетворено или нет («проблема разрешимости (opens in a new tab)»), поскольку программа может никогда не завершиться. Таким образом, может быть невозможно доказать некоторые свойства контракта, даже если он хорошо специфицирован.

Инструменты формальной верификации для смарт-контрактов Эфириума

Языки спецификаций для создания формальных спецификаций

Act: Act позволяет специфицировать обновления хранилища, пред/постусловия и инварианты контракта. Его набор инструментов также имеет бэкенды доказательств, способные доказывать многие свойства с помощью Coq, SMT-солверов или hevm.

Scribble — Scribble преобразует аннотации кода на языке спецификаций Scribble в конкретные утверждения, которые проверяют спецификацию.

Dafny — Dafny — это готовый к верификации язык программирования, который опирается на высокоуровневые аннотации для рассуждений и доказательства корректности кода.

Верификаторы программ для проверки корректности

Certora Prover — Certora Prover — это автоматический инструмент формальной верификации для проверки корректности кода в смарт-контрактах. Спецификации пишутся на CVL (Certora Verification Language), а нарушения свойств обнаруживаются с использованием комбинации статического анализа и решения ограничений.

Solidity SMTChecker — SMTChecker в Solidity — это встроенный инструмент проверки моделей, основанный на SMT (Satisfiability Modulo Theories) и решении предложений Хорна. Он подтверждает, соответствует ли исходный код контракта спецификациям во время компиляции, и статически проверяет нарушения свойств безопасности.

solc-verify — solc-verify — это расширенная версия компилятора Solidity, которая может выполнять автоматизированную формальную верификацию кода Solidity с использованием аннотаций и модульной верификации программ.

KEVM — KEVM — это формальная семантика виртуальной машины Эфириума (EVM), написанная в фреймворке K. KEVM является исполняемой и может доказывать определенные утверждения, связанные со свойствами, используя логику достижимости.

Логические фреймворки для доказательства теорем

Isabelle — Isabelle/HOL — это помощник по доказательствам, который позволяет выражать математические формулы на формальном языке и предоставляет инструменты для доказательства этих формул. Основным применением является формализация математических доказательств и, в частности, формальная верификация, которая включает доказательство корректности компьютерного оборудования или программного обеспечения и доказательство свойств компьютерных языков и протоколов.

Rocq — Rocq — это интерактивный прувер теорем, который позволяет определять программы с помощью теорем и интерактивно генерировать машинно-проверяемые доказательства корректности.

Инструменты на основе символьного выполнения для обнаружения уязвимых шаблонов в смарт-контрактах

Мантикора — Инструмент для анализа байт-кода EVM, основанный на символьном выполнении.

hevm — hevm — это движок символьного выполнения и средство проверки эквивалентности для байт-кода EVM.

Mythril — Инструмент символьного выполнения для обнаружения уязвимостей в смарт-контрактах Эфириума

Дополнительная литература