Noobing Security Research: “Formal Verification, часть 4 Правило для проверки transfer в ERC-20 Се…”

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