В этой статье мы:
сделаем поверхностный обзор подходов, обеспечивающих безопасность смарт‑контрактов;
разберем устройство и принцип работы инструмента формальной верификации SMTChecker — он интегрирован в компилятор solc;
практика: верифицируем несколько учебных контрактов на Solidity с помощью SMTChecker.
Обзор подходов к безопасности и надежности смарт-контрактов
Формальная верификация - это подход, позволяющий с помощью математических методов доказать, что код смарт-контракта не содержит ошибок определенного вида. Формальная верификация стоит наряду с другими инструментами анализа безопасности и надежности смарт-контрактов, такими как:
инструменты статического анализа, линтеры (Slither, Solhint)
верификация (сверка) исходного кода и байткода, развернутого на блокчейне (Sourcify, EtherScan)
фреймворки для Unit-тестирования, динамического анализа (Foundry, HardHat)
инструменты для Fuzzing-тестирования (Echidna)
инструменты для оптимизации расхода газа и DeFi — тестирования (Chainlink VRF)
аудит, краудсорсинговое обнаружение уязвимостей (OpenZeppelin, Immunefi)
мониторинг контракта после развертывания (OpenZeppelin Defender, EtherScan, The Graph)
Формальная верификация отличается от вышеперечисленных методов сложностью логики, глубиной анализа, а от некоторых и назначением в целом, а главное — она дает возможность доказать с математической точностью, что код не содержит определенного вида ошибок.
Формальная верификация на практике — это:
написание спецификаций (или описание модели поведения/модели безопасности программы);
математическое доказательство того, что код соответствует спецификации.
Верификация смарт-контракта начинается с выбора инструмента — готовых существует несколько:
Certora Prover
Фреймворк ConCert
KEVM (K Framework)
Solidity SMTChecker
Устройство и принцип работы SMT-Checker
В этой статье мы рассмотрим инструмент, интегрированный в компилятор solc: Solidity SMTChecker.
Для начала необходимо установить компилятор, я использовала PPAs для Ubuntu:
sudo add-apt-repository ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install solcЕсли говорить простыми словами, SMTChecker строит модель кода смарт-контракта в виде формул, которые проверяются на SMT-солвере и Horn-солвере. Формулы отправляются солверу, солвер возвращает ответ. Если солвер нашел ошибку — он может вернуть контр-пример, демонстрирующий, на каких именно значениях входных параметров функция ведет себя не так как ожидается.
SMTChecker включает в себя две модели автоматической проверки спецификаций — это Bounded Model Checker (BMC) и Constrained Horn Clauses (CHC).
CHC (в основе лежит логика Хорна) — более мощная, и, по умолчанию запускается первой. Модель строит CFG (Граф управления потоком) смарт-контркта в виде системы хорновских дизъюнктов. Анализируется поведение контракта в целом, количество транзакций, каждая функция. Эта модель умеет анализировать циклы (BMC пока не умеет).
Если CHC не удалось доказать какое-то утверждение — это утверждение передается в BMC. Каждое сообщение об ошибке сопровождается пометкой, от какой модели это сообщение пришло. По умолчанию SMTChecker выключен. Включить его можно в консоли, указав, какую модель использовать:
CLI option --model-checker-engine {all,bmc,chc,none}
Или в настройках JSON:
JSON option settings.modelChecker.engine={all,bmc,chc,none}.
Я рекомендую включать все модели {all}, т. к. принципы работы моделей отличаются, и ошибки, которые не смогла найти CHC может выявить BMC.
SMTChecker в Solidity работает со следующими солверами: Z3 (по-умолчанию), CVC4 / CVC5, Eldarica.
Пользователь может выбрать какой из солверов следует использовать, передав опцию CLI
--model-checker-solvers {all,cvc5,eld,smtlib2,z3}
или определить это в файле JSON
option settings.modelChecker.solvers=[smtlib2,z3]
Все опции ModelChecker можно посмотреть через solc —help, вот они:
Исходный код чекера лежит на GitHub, написан он на языке C++, как и сам компилятор solc. Проект являетя open source, и, если очень хочется, можно поучаствовать в его разработке, взяв на себя одну из открытых задач.
Практика: формальная верификация смарт-контрактов
Приступим к верификации кода на Solidity, чтобы продемонстрировать возможности SMTChecker.
Исходный код примеров, разработанных для этой статьи можно посмотреть также на GitHub.
По умолчанию, если включить обе модели, SMTChecker проверит следующее:
Арифметическое переполнение и исчерпание разрядности (underflow и overflow)
Деление на ноль
Тривиальные условия и недостижимый код
Извлечение элемента из пустого массива
Выход за границы индекса
Недостаточность средств для перевода
Можно также в строке запроса указать, какие именно цели проверить отдельно, например
--model-checker-targets divByZero
Чтобы получить больше — нужно написать собственную спецификацию. В целом процесс верификации можно разделить на два больших шага:
разработка модели безопасности, или спецификаций, описывающих ожидаемое поведение смарт-контракта. Этот шаг выполняет человек.
доказательство, что код соответствует спецификации. Этот шаг помогает выполнить солвер
Спецификации состоят (как и во многих других подобных инструментах) из require и assert утверждений. Где require — это ограничения, которые солвер будет учитывать во время проверки, то есть они будут частью формулы, отправляемой солверу. А assert — само утверждение.
Встроенная в Solidity функция require помогает исправить ошибки, которые нашел SMTChecker — она накладывает требуемые ограничения, и уточнения.
Алгоритмы проверки, лежащие в основе используют разные подходы — символьное исполнение, проверка пограничных значений и другие.
Можно включить опцию «показать все доказанные свойства безопасности контракта»
--model-checker-show-proved-safe
и мы увидим целый список ошибок, отсутствие которых было доказано.
Давайте рассмотрим контракт, приведенный ниже - Arithmetic.sol. Это код контракта до верификации, в нем есть ошибки, если точнее, три ошибки разных видов.
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Overflow {
uint immutable x;
uint immutable y;
modifier req() {
require(x >= 0);
require(y >= 0);
_;
}
function add(uint x_, uint y_) internal view req returns (uint) {
return x_ + y_;
}
function mul(uint x_, uint y_) internal view req returns (uint) {
return x_ * y_;
return x_+ y_;
}
constructor(uint x_, uint y_) {
(x, y) = (x_, y_);
}
function stateAdd() public view {
uint res_add = add(x, y);
assert(x <= res_add && y <= res_add);
}
function stateMul() public view {
uint res_mul = mul(x, y);
assert(x <= res_mul && y <= res_mul);
}
}А теперь приведем этот же контракт, но после верификации. В коде ниже я устранила все ошибки, допущенные в контракте. Это было сделано с помощью SMTChecker:
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
// Since Solidity 0.8.0, arithmetic operations automatically revert on overflow/underflow
contract Overflow {
uint immutable x;
uint immutable y;
modifier req() {
require(x >= 0);
require(y >= 0);
require(x < type(uint128).max); // comment to detect overflow error
require(y < type(uint128).max); // comment to detect overflow error
_;
}
function add(uint x_, uint y_) internal view req returns (uint) {
return x_ + y_;
}
function mul(uint x_, uint y_) internal view req returns (uint) {
return x_ * y_;
// return x_+ y_; // uncomment to detect unrecheable code error
}
constructor(uint x_, uint y_) {
(x, y) = (x_, y_);
}
function stateAdd() public view {
uint res_add = add(x, y);
assert(x <= res_add && y <= res_add);
}
function stateMul() public view {
require (x != 0); // comment to detect assertion violation
require (y != 0); // comment to detect assertion violation
uint res_mul = mul(x, y);
assert(x <= res_mul && y <= res_mul);
}
}Места, где ошибки были обнаружены снабжены комментариями.
Всего с помощью SMTChecker было выявлено 3 вида ошибок:
unrecheable code (но это легко находит и простой IDE, не говоря уж о линтерах и проч.)
arithmetic overflow — проверяется SMTCheker по умолчанию
assertion violation — невыполнение спецификации, заданной assert
Для overflow ошибок, солвер привел контр-пример. Для ошибки Assertion violation солвер мне не привел контр-примера (а хотелось бы). Так тоже бывает. Это зависит от многих факторов: от солвера, установленного пользователем, от сложности задачи. Попробуйте запустить код на вашей машине — вернул ли вам солвер контр-пример для assertion violation?
Рассмотрим найденную солвером ошибку Assert violation (нарушение спецификации assert). Заметим, что для функции stateAdd assert выполняется, а для функции stateMul — уже нет. Почему? Если x или y будут равные нулю, то assert для stateMul уже не выполнится. Добавление дополнительных ограничений для функции stateMul решает проблему:
require (x != 0); // comment to detect assertion violation
require (y != 0); // comment to detect assertion violation
После того, как мы исправили все найденные солвером ошибки, SMTCheker возвращает такой ответ:
Info: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
CHC — говорит нам о том, что проверка выполнялась на модели Constrained Horn Clauses
А если мы включим опцию —model-checker-show-proved-safe, то солвер покажет нам полный список доказанных свойств:
Ошибки были исправлены — можно раскомментировать или закомментировать строчки кода, чтобы посмотреть как солвер отмечает найденные ошибки.
Итак, утверждение (assertion) представляет собой инвариант в вашем коде: это свойство, которое должно быть истинным для всех транзакций, включая все входные значения и значения storage, в противном случае это означает наличие ошибки.
Функции stateMul() и stateAdd() задают спецификации, а SMTChecker подтверждает, что свойство корректно.
Рассмотрим еще один пример: контракт Max, из листинга Loops.sol (все примеры конрактов для этой статьи можно посмотреть на GitHub)
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Max {
function max(uint[] memory a) public pure returns (uint) {
uint m = 0;
for (uint i = 0; i < a.length; ++i)
if (a[i] > m)
m = a[i];
for (uint i = 0; i < a.length; ++i)
assert(m >= a[i]);
return m;
}
}В этом примере assert (инвариант) встроен в тело цикла. Для этого примера солвер также проверит overflow для ++i, и выполнение assert на каждом шаге цикла. Для солвера циклы могут быть проблемой (так же как и для расхода газа), тут нужно помнить, что в общем случае SMT-проблемы являются NP-полными (как и SAT):
В худшем случае время работы экспоненциально (
O(2^n)) от размера задачи.На практике решатели, с которыми работает SMTChecker (Z3, cvc5, Eldarica) используют эвристики и оптимизации, поэтому часто справляются за разумное время.
В заключение приведем тезисно преимущества и недостатки инструментов формальной верификации, встроенных в компилятор Solidity - SMTChecker
Преимущества:
выразительность спецификаций, возможность описать модель поведения кода
возможность автоматизации и большой объем покрытия диапазонов анализируемых значений
демонстрация контр-примеров
автоматическая проверка целого ряда ошибок
Недостатки:
инструментарий находится в стадии разработки и набор разновидностей ошибок, которые можно верифицировать — ограничен
SMTChecker не может анализировать некоторые возможности Solidity, такие как
keccak256,ecrecover, address.call, delegatecall,а также динамическое хранилище: массивы без ограничения длины, маппинги с произвольными ключами.плохо работает с нелинейной арифметикой
при работе с Horn логикой инварианты (например, в циклах) должны описываться вручную
ВMC (Bounded Model Checker) проверяет конечное число путей выполнения (до определённой глубины циклов) на нарушения условий
assertиrequire, и может не отловить баги, находящиеся за пределами проверкитут идет речь о выдаче ложных положительных результатов: невозможно доказать отсутствие багов, можно только показать их наличие и только в рамках указанных границ. Например BMC может пропустить ошибку overflow внутри цикла, который работает вне пределах ограничений, наложенных моделью.
Высокая вычислительная сложность:
SMT-решатели (например, Z3) могут не уложиться в допустимое время проверки для больших контрактов или сложной логики.
не решает вопросы учета расхода газа
Для максимальной безопасности смарт-контракта необходимо реализовать комплексный подход, использовать разные инструменты и формальная верификация — один из них.
