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