Про Formal Verification, часть 1

Упоминал про этот метод анализа кода здесь

Рассказывать буду на примере Certora, так как сам пользуюсь их сервисом. Это будет серией постов неопределенной длины, поскольку нюансов работы множество.

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

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

Certora (произносится как «сертора») как система состоит из двух частей:
- Certora Verification Language
- Certora Prover

Certora Verification Language - CVL
Это специальный язык, который используется для написания спецификаций для смарт контрактов

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

В спецификациях определяются правила анализируемого контракта, которые несут в себе некоторые предположения о его поведении. Эти правила компилируются в логические формулы, которые называются verification condition. Обычно их создается некоторое множество, которое затем отправляется на анализ в SMT Solver

SMT Solver - Satisfiability Modulo Theories Solver. Проверяет могут ли быть удовлетворены условия выражения

Для написания теста формальной верификации по стандарту создается в корне проекта папка certora с двумя подпасками: conf и spec и в них соответственно два файла с расширениями .spec и .conf

На этом сегодня закончу, хороших выходных!

https://t.me/web3securityresearch

Formal Verification, часть 2
.conf файл

Конфигурационный файл и этим все сказано. Хранит в себе пути к исследуемым контрактам, к файлу спецификации, содержит настройки прувера

Имеет расширение .conf, пишется как JSON

Типичный файл выглядит так

{
    "files": [
        "./src/OurContract.sol:OurContract",
        "./src/AnotherContract.sol:AnotherContract"
    ],
    "verify": "OurContract:certora/spec/OurContractInvariant.spec",
    "wait_for_results": "all",
    "rule_sanity": "basic",
    "optimistic_loop": true,
    "msg":"Verification of OurContractInvariant"
}

После разделов files и verify находятся настройки анализа, альтернативно их можно писать в CLI при вызове команды certoraRun, которая запускает верификацию

То есть можно было бы написать

 certoraRun ./certora/conf/OurContract.conf --verify OurContract:certora/spec/OurContractInvariant.spec --wait_for_results all --rule_sanity basic --optimistic_loop true --msg Verification of OurContractInvariant

Кроме прочего таким образом могут быть заданы настройки самого прувера

После запуска команды certoraRun компилируются контракты, затем проверяется корректность локально, если все ок, то задача уходит в работу на сервер, когда будет готово - вам пришлют ссылку на отчет

Потому что Certora работает по freemium модели и вам доступны 2000 минут работы сервиса в месяц

https://t.me/web3securityresearch

Интересный пост в Сиолошной, про то как AI модели могут находить и эксплуатировать уязвимости в смарт-контрактах уже сейчас

оригинал статьи на английском от Антропик

В статье указаны две уязвимости в коде:
- в первом случае в контракте все пользователи имели доступ к функции калькулятора, меняющей storage переменные и модель смогла провести inflation attack, про которые я писал
- во втором случае в контракте, выпускающем токены в один клик, можно было задеплоить токен без указания адреса для приема комиссий. Зато его можно было добавить позже

Круто, что атакующие скрипты в исходной статье тоже показаны

https://t.me/web3securityresearch

Formal Verification, часть 4

Правило для проверки transfer в ERC-20

Сегодня разбираем как написать правило на примере стандартной реализации ERC-20

Проверяемое правило:
Баланс бенефициара увеличивается соответствующим образом

Правило простое, в общих чертах похожее на то, что стоило бы написать в обычном тесте

/** @title Transfer must move `amount` tokens from the caller's
 *  account to `recipient`
 */
rule transferSpec(address recipient, uint amount) {

    env e;
    
    // `mathint` is a type that represents an integer of any size
    mathint balance_sender_before = balanceOf(e.msg.sender);
    mathint balance_recip_before = balanceOf(recipient);

    transfer(e, recipient, amount);

    mathint balance_sender_after = balanceOf(e.msg.sender);
    mathint balance_recip_after = balanceOf(recipient);

    // Operations on mathints can never overflow nor underflow
    assert balance_sender_after == balance_sender_before - amount,
        "transfer must decrease sender's balance by amount";

    assert balance_recip_after == balance_recip_before + amount,
        "transfer must increase recipient's balance by amount";
}

Необычных вещей здесь несколько:
1) env e. Главное отличие ФВ от тестов в том, что она учитывает все возможные входные данные и все возможные контексты вызова. Как раз контекст передается через переменную env. Достаточно объявить одну, но можно использовать больше. Соответственно, она содержит/предоставляет такую информацию как: e.msg.sender, e.block.number и так далее. Передавать e следует первой из аргументов
2) mathint. Это собственный тип CVL для целых чисел произвольного размера. Позволяет не беспокоиться о переполнении и знаке
3) в CVL можно использовать только assert, а вот assertEq не поддерживается

Выполнение проверки этого правила завершится с ошибкой, отчет об этом на прикрепленном изображении

...
Finished verification request
ERROR: Prover found violations:

[rule] transferSpec: FAIL
report url: https://prover.certora.com/output/...

Violations were found

Ошибка возникает в случае, когда пользователь отправляет токены сам себе, так что assert'ы неверны

На экране отчета мы видим 4 столбца:
- слева мы видим проверяемые правила
- второй столбец содержит проверяемый код
- в третьем call trace вызова, в котором обнаружено нарушение
- в четвертом значения переменных и параметров

Для того, чтобы обрабатывать этот случай следует добавить следующий assert

    assert recipient == sender => balance_sender_after == balance_sender_before,
        "transfer must not change sender's balancer when transferring to self";

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

Ссылки:
- Туториал, взятый за основу
- Исследуемая реализация ERC-20, код
- Исходная спецификация
- Исправленная спецификация

https://t.me/web3securityresearch

Вышел Solidity 0.8.31

Команда Solidity объявила о выходе компилятора Solidity версии 0.8.31. Обновление приносит поддержку новых возможностей EVM, представленных в сетевом апгрейде Fusaka, расширяет функциональность спецификаторов раскладки хранилища и запускает первый этап отказа от устаревших возможностей, которые будут окончательно удалены в версии 0.9.0. Кроме того, теперь официально публикуются сборки компилятора для Linux на архитектуре ARM.

Одним из ключевых изменений стало то, что версия EVM с кодовым названием osaka теперь используется по умолчанию. При необходимости разработчики по-прежнему могут указать более старую версию виртуальной машины через настройки компилятора. В новой версии также добавлена поддержка опкода CLZ, реализующего стандарт EIP-7939. Эта инструкция позволяет считать количество ведущих нулей в 256-битном слове и открывает новые возможности для оптимизаций, битовых операций, алгоритмов сжатия и работы со структурами данных на уровне приложений.

В ближайшее время этот опкод найдет активное применение в популярных библиотеках, включая solady и OpenZeppelin, где сможет заменить существующие реализации вроде Math.clz(). Пока в самом компиляторе область применения CLZ ограничена, но команда изучает способы использовать его для будущих оптимизаций генерации байткода.

С точки зрения инфраструктуры релиза произошло важное обновление: начиная с этой версии, Solidity официально выпускается в виде бинарных сборок для Linux на ARM. Ранее такие версии существовали либо в виде сборок под macOS, либо в виде самостоятельной компиляции из исходников. Теперь ARM-билды встроены в систему CI и проходят тот же цикл тестирования, что и остальные платформы, гарантируя идентичность байткода и метаданных на всех архитектурах.

Также введён формат предварительных релизов. Если раньше существовали только ночные сборки и полноценные релизы, то теперь появились pre-release версии, позволяющие получать доступ к новым фичам раньше официального релиза. Именно в pre-release впервые стала доступна поддержка CLZ, и эта практика будет использоваться дальше для постепенного внедрения экспериментальных возможностей.

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

Наконец, версия 0.8.31 открывает фазу активной подготовки к релизу 0.9.0, который станет несовместимым с предыдущими версиями. В компилятор добавлены предупреждения об устаревании send() и transfer(), устаревшего ABI coder v1, виртуальных модификаторов, сравнений контрактов без явного приведения к адресу и специального комментария memory-safe-assembly. Всё это сигнализирует о переходе Solidity к более строгой типизации, более прозрачной семантике и сокращению исторически сложных и небезопасных конструкций, которые долгое время тянулись из ранних версий языка.

#solidity

Formal Verification, часть 4.1

Правило для проверки total supply в ERC-20

Проверяемое правило:
Total supply токена > баланс любого пользователя

Правило несложное, выглядит так. Сминтили токены на аккаунт, проверяем

/// @title Total supply after mint is at least the balance of the receiving account
rule totalSupplyAfterMint(address account, uint256 amount) {
    env e; 
    
    mint(e, account, amount);
    
    uint256 userBalanceAfter = balanceOf(account);
    uint256 totalAfter = totalSupply();
    
    // Verify that the total supply of the system is at least the current balance of the account.
    assert totalAfter >=  userBalanceAfter, "total supply is less than a user's balance";
}

Вот только по отчету certora это правило будет нарушено/violated

Потому что Certora работает так, что проверяет все возможные пути, даже те, которые невероятны/недостижимы. В данном случае один из таких путей это когда totalSuplly() вернет значение меньше, чем balanceOf()

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

Поэтому существуют

Preconditions - условия, которые мы задаем явно

В данном случае после строчки с env e следует добавить:

    // Assume that in the current state before calling mint, the total supply of the 
    // system is at least the user balance.
    uint256 userBalanceBefore =  balanceOf(account);
    uint256 totalBefore = totalSupply();
    require totalBefore >= userBalanceBefore; 

То есть обозначить, что total supply до операции был больше, чем user balance до операции

Про переменные надо еще сказать следующее:
- неинициализированная переменная может принимать любое значение
- require тем не менее может ограничить ее каким-либо образом
- переменные внутри правила immutable
- а вот ghost переменные могут меняться

Ссылки:
- Туториал, взятый за основу
- Спецификация

https://t.me/web3securityresearch

Formal Verification, часть 5

Parametric rules - Параметрические правила

Тот момент, где начинает раскрываться мощь инструмента

Многие свойства могут быть обобщены для всех функций контракта

Проверяемое правило:
Allowance может меняться только владельцем

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

К тому же подобных правил под проверку может быть несколько

Как выглядит параметрическое правило

rule someParametricRule(method f) {
    ...
    env e;  // The env for f
    calldataarg args;  // Any possible arguments for f
    f(e, args);  // Calling the contract method f
    ...
}

То есть мы в правило передаем некий method f в качестве параметра. Прувер будет передавать все возможные методы для исполнения в правило, а поскольку это имитация вызовов, то каждому вызову метода f положено передавать контекст вызова через env e и данные вызова через calldataarg args. При этом calldataarg автоматически подстроится под сигнатуры функций

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

Выглядит так:

f.selector == sig:approve(address, uint).selector

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

Полный пример кода:

/**
 * # ERC20 Parametric Example
 *
 * Another example specification for an ERC20 contract. This one using a parametric rule,
 * which is a rule that encompasses all the methods in the current contract. It is called
 * parametric since one of the rule's parameters is the current contract method.
 * To run enter:
 * 
 * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "Parametric rule"
 *
 * The `onlyHolderCanChangeAllowance` fails for one of the methods. Look at the Prover
 * results and understand the counter example - which discovers a weakness in the
 * current contract.
 */

// The methods block below gives various declarations regarding solidity methods.
methods
{
    // When a function is not using the environment (e.g., `msg.sender`), it can be
    // declared as `envfree`
    function balanceOf(address) external returns (uint) envfree;
    function allowance(address,address) external returns(uint) envfree;
    function totalSupply() external returns (uint) envfree;
}

/// @title If `approve` changes a holder's allowance, then it was called by the holder
rule onlyHolderCanChangeAllowance(address holder, address spender, method f) {

    // The allowance before the method was called
    mathint allowance_before = allowance(holder, spender);

    env e;
    calldataarg args;  // Arguments for the method f
    f(e, args);                        

    // The allowance after the method was called
    mathint allowance_after = allowance(holder, spender);

    assert allowance_after > allowance_before => e.msg.sender == holder,
        "only the sender can change its own allowance";

    // Assert that if the allowance changed then `approve` or `increaseAllowance` was called.
    assert (
        allowance_after > allowance_before =>
        (
            f.selector == sig:approve(address, uint).selector ||
            f.selector == sig:increaseAllowance(address, uint).selector
        )
    ),
    "only approve and increaseAllowance can increase allowances";
}

К этому моменту может появиться ощущение, что все не так уж сложно, но это до тех пор, пока вы не запустите ФВ на своем коде

Ссылки:
- Туториал, взятый за основу
- Спецификация на github

https://t.me/web3securityresearch

Formal Verification, часть 6

Vacuity

Одна из ошибок, с которой я столкнулся (и многие до и после меня), гласит rule is vacuous

Что можно перевести как правило бездумное/бессодержательное

Такая ошибка возникает, когда не существует таких путей исполнения программы, при которых выполнялись бы заявленные требования

Например, наше бездумное требование выглядит так:

rule simpleVacuousRule(uint256 x, uint256 y) {
    // Contradictory requirement
    require (x > y) && (y > x);
    assert false;  // Should always fail
}

У Prover есть свойство rule_sanity, которое может быть задано в .conf файле. Если будет указано, что rule_sanity basic, то прувер пометит это правило как неисполнимое, потому что оно не прошло проверку на корректность. Но если задать rule_sanity none, то правило будет помечено как верифицированное, потому что контрпримера не существует в том плане, что assert недостижим и значит не завершается ошибкой

Происходит это потому, что прувер по умолчанию игнорирует пути, которые завершаются revert'ом симулируемой транзакции

Для включения таких путей в анализ используется оператор @withrevert, который добавляется после названия функции, например someFunction@withrevert(args)

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

CVL так же имеет встроенную bool lastReverted, которая изменяется в зависимости от того, была ли последняя вызываемая функция reverted

Зачем это вообще нужно? Чтобы проверять, что некоторые пути действительно всегда недостижимы

Если наша @withRevert функция была ревертнута, то lastReverted становится true и возможно проверить что assert lastReverted. Потому что он теперь во-первых достижим, во-вторых true

Ссылки:
- Туториал, взятый за основу
- Спецификация
- Конфигурация

https://t.me/web3securityresearch

Mastering Ethereum
https://masteringethereum.xyz/

Даже немного странно, что я только недавно наткнулся на эту книгу, в этом замечательном канале

Читаю её последние пару недель, очень цельный и последовательный источник, по сути полное описание того, что следует знать о сети эфира

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

Еще одно подтверждение того, что даже в эпоху доступных переводчиков, владеть английским - неоценимое благо

Пост-навигация, дополняется

- Начало

Обучение никогда не заканчивается
- Про курсы
- Про источники информации о взломах
- Базовый учебник по Ethereum
- Про тесты
- Formal Verification в серии постов 1, 2, 3, 4, 5, 6

Механики аудита
- Какой бывает
- Стадии аудита
- Рект тест
- Оценка уязвимостей

Уязвимости
- Reentrancy
- Price Oracle Manipulation
- Access Control Vulnerabilities
- Inflation Attack 1, 2

Обзор статей
- MEV, Flash Boys 2.0: Frontrunning, Transaction Reordering, and Consensus Instability in Decentralized Exchanges
- AI, Перевод статьи «Detecting Functional Bugs in Smart Contract through LLM-powered and Bug-Oriented Compose Analysis», 2025, в нескольких частях

Разборы взломов
- Взлом GMX, что это было?
- Неэффективность NFT Strategy, стоившая почти 1кк$

Безопасность окружения разработки
- Kipuka - контроль npm-пакетов