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

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

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

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

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

Чтобы понять, каким образом Certora Prover выполняет такую проверку, необходимо рассмотреть общий принцип его работы.

Как упомянуто ранее, процесс верификации начинается с двух входных компонентов - кода и спецификации. На первом этапе Solidity-код компилируется в байткод Ethereum Virtual Machine. В следующем шаге байткод декомпилируется в трехадресный код (Three-Address Code, TAC), который представляет собой упрощенное, но более объемное представление логики программы. TAC упрощает отдельные вычислительные шаги, что важно для дальнейшего анализа.

На этапе статического анализа TAC-код оптимизируется. К примеру, некоторые участки программы, не влияющие на проверяемое свойство, могут быть исключены. Далее оптимизированный код комбинируется со спецификацией CVL, в результате чего формируются логические формулы. Они передаются в constraint solver (например, Z3 или CVC5), который уже либо доказывает корректность свойства, либо находит контрпример.

Далее разберем формальные основы, лежащие в архитектуре Prover. Они помогут нам понять, какие свойства проверяются и как они формализуются.

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

Также используется тройка Хоара, которая записывается в виде {P} C {Q}, где P - предусловие, C - команда, а Q - постусловие. Предусловие описывает состояние системы до вызова команды, а постусловие - ожидаемое состояние после его выполнения. Если первое выполняется, то корректная реализация команды должна обеспечивать выполнение второго.

В CVL эти идеи выражаются через правила (rule) и инварианты (invariant), которые используются для описания проверяемых свойств. Правила применяются для описания конкретных сценариев при вызове функций. В них четко задается последовательность действий и проверяется, что после их выполнения соблюдается нужное свойство. Инварианты же описывают свойства, которые должны сохраняться в любом случае, на любом этапе жизни системы.

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

Примеры далее позволят увидеть разницу между правилами и инвариантами.

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

rule contractOwnerNeverChange(env e) {

address owner = contractOwner();

method f;

calldataarg args;

f(e, args);

assert owner == contractOwner();

}

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

invariant totalSupplyIsSumOfBalances() {

totalSupply() == sumOfBalances;

}

Однако правило contractOwnerNeverChange нельзя выразить в форме инварианта, поскольку в Certora Prover инварианты не позволяют фиксировать значения переменных до вызова функции.:

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

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

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

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

Certora Prover может использоваться на разных этапах жизненного цикла проекта. Например, он может применяться во время аудитов, после исправления багов для подтверждения их устранения, а также в публичных аудитах и bug bounty-программах (программах, в рамках которых компании вознаграждают сторонних пользователей за найденные уязвимости в их продуктах).

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

Наконец, мы рассмотрим, как применение Certora Prover выглядит на конкретном примере.

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

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

Скриншот показывает контрпример, найденный Certora Prover, указывающий на нарушение правила в реализации permit.

Таким образом, Certora Prover позволяет проверять корректность смарт-контрактов относительно заданных свойств и выявлять ошибки, пропущенные аудитами и тестами. На практике он используется как один из инструментов безопасности и наиболее эффективен в комплексе.