Верификация смарт-контрактов

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

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

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

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

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

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

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

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

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

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

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

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

Низкоуровневые модели считаются идеальными, поскольку они представляют фактическое выполнение смарт-контракта в среде выполнения Ethereum (т. е. 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) — это «правила для рассуждений о предложениях, квалифицированных с точки зрения времени (например, «Я всегда голоден» или «Я в конце концов проголодаюсь»)». Применительно к формальной верификации временные логики используются для формулирования утверждений о правильном поведении систем, смоделированных как конечные автоматы. В частности, временная логика описывает будущие состояния, в которых может находиться смарт-контракт, и как он переходит между состояниями.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Проверка моделей требует создания абстрактного математического представления системы (т. е. контракта) и выражения свойств этой системы с использованием формул, основанных на пропозициональной логике (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.

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

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

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

1function safe_add(uint x, uint y) returns(uint z){
2
3  z = x + y;
4  require(z>=x);
5  require(z>=y);
6
7  return z;
8}

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

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

Необходимость надежности

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Стоимость ручного труда

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

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

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

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

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

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

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

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

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

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

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

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

Документация (opens in a new tab)

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

GitHub (opens in a new tab)

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

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

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

GitHub (opens in a new tab)

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

GitHub (opens in a new tab)

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

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

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

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

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

Manticore - Инструмент для анализа байткода EVM на основе символического выполнения.

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

GitHub (opens in a new tab)

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