Noobing Security Research: “Formal Verification, часть 3.1 Что содержит .spec файл Здесь мы на язы…”

Formal Verification, часть 3.1

Что содержит .spec файл

Здесь мы на языке CVL (Certora Verification Language) пишем спецификацию

Что может быть указано в .spec файле:

👨‍💻 Import statements: файлы CVL могут импортировать содержимое других файлов CVL
Пример

import "base.spec";

Такое объявление импортирует все элементы из base.spec за исключением правил и инвариантов

👨‍💻 Use statements: оператор use позволяет использовать правила и инварианты из других файлов/встроенных правил
Пример

use rule ruleInBase;

Импортирует правило ruleInBase из base.spec. Может использоваться в связке с фильтрами (о них как-нибудь позже), может переписывать импортированные фильтры

👨‍💻 Using statements: Позволяет получить ссылки на различные контракты
Пример

using Asset as underlying;

Если дальше по файлу писать что-то вроде "underlying.someFunc()", то это равносильно вызову функции на экземпляр контракта

👨‍💻Methods blocks: methods блок содержит информацию о том, как должны вести себя методы, какие из них мы подвергаем суммаризации (summarization). Это вообще один из интересных концептов формальной верификации, про него будет отдельный пост, возможно не один

В блоке методов не надо указывать все проверяемые методы, там необходимы лишь те, про которые мы хотим внести дополнительную информацию
Пример

methods {
    function _.balanceOf(address) external => DISPATCHER(true);
    function _.totalSupply() external => DISPATCHER(true);
    function _.transfer(address, uint256) external => DISPATCHER(true);
    function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
}

👨‍💻 Rules: Правила описывают желаемое поведение методов и контрактов. Корневое понятие, именно правила проверяет prover. Если правило нарушается, то это называется контрпример - counterexample
Пример

/// `deposit` must increase the pool's underlying asset balance
rule integrityOfDeposit {

    mathint balance_before = underlyingBalance();

    env e; 
    uint256 amount;
    safeAssumptions(_, e);

    deposit(e, amount);

    mathint balance_after = underlyingBalance();

    assert balance_after == balance_before + amount,
        "deposit must increase the underlying balance of the pool";
}

Простое правило, которое проверяет, что баланс после всегда равен балансу до плюс вносимая сумма

👨‍💻 Invariants: Инвариант описывает свойство системы, которое всегда должно выполняться. В CVL инвариант может быть сильным или слабым. Первый должен выполняться в "момент покоя", то есть пока контракт не исполняется. Сильный инвариант держится не только между транзакциями, но и до/после вызова unresolved external calls, например call или delegatecall
Пример

/// The ball should never get to player 2 - strenghened invariant
invariant playerTwoNeverReceivesBall() 
    ballPosition() == 1 || ballPosition() == 3;

мяч должен всегда быть у первого или третьего игрока

👨‍💻 Functions: CVL функции. Могут использоваться для вычислений, могут переопределять функции из блока methods
Пример

function abs_value_difference(uint256 x, uint256 y) returns uint256 {
    if (x < y) {
      return y - x;
    } else {
      return x - y;
    }
}

👨‍💻 Definitions: CVL определения - это типизированные макросы, предназначаются для упрощения спецификации.
Пример

definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffff;
definition is_even(uint256 x) returns bool = exists uint256 y . 2 * y == x;

https://t.me/web3securityresearch