Ir para o conteúdo
Buscar

WEB3DEV

Cover image for SMTChecker: (quase) Superpotência Prática
Panegali
Panegali

Posted on

SMTChecker: (quase) Superpotência Prática

#smtchecker #solidity

Teoria: o que é SMTChecker?

Você apostaria seu primogênito que o contrato que você acabou de implantar não tem vulnerabilidades críticas? Se você é como eu, a resposta é um sonoro 'não'.

Já vi hacks suficientes na engenharia de software tradicional para saber que você nunca pode ter 100% de certeza. Isso é assustador, mas uma combinação de diferentes técnicas pode nos levar bem perto do nível de confiança desejado. SMTChecker é um delas.

É uma ferramenta que realiza a verificação formal do seu contrato: você define uma especificação (o que você acha que seu contrato deve fazer) e o SMTChecker prova formalmente que o contrato está de acordo com a especificação. Se isso não acontecer, o SMTChecker geralmente fornece um contra exemplo concreto: uma sequência de transações que quebram a especificação.

E a melhor parte? Se você usa o Solidity, já tem o SMTChecker — ele faz parte do compilador do Solidity.

Não é uma solução à prova de balas - existem bugs, a verificação é lenta. Acima de tudo, é muito difícil definir uma especificação completa. Mas mesmo sabendo disso, ainda vale a pena tentar.

Exemplo: damas

O contrato implementa um contador — uma peça do jogo de damas (ou esboços) jogada em um tabuleiro de 8x8.

Vamos implementar um 'contador preguiçoso' (inventado): ele não pode se mover, mas pode capturar peças em células diagonalmente adjacentes 'pulando' sobre elas: se eu estiver em (0, 0) e quiser capturar um peça em (1, 1), vou terminar em (2, 2). Fácil.

// SPDX-License-Identifier: MIT
pragma solidity >=0.8.7;

contract LazyCounter {
    int8 private x;
    int8 private y;

    constructor(int8 _x, int8 _y) {
        // verificar se estamos dentro dos limites da diretoria
        require(_x >= 0 && _x < 8 && _y >= 0 && _y < 8);

        x = _x;
        y = _y;
    }

    /// @dev captura um pedaço em (_x, _y)
    function capture(int8 _x, int8 _y) public {
        require(_x >= 0 && _x < 8 && _y >= 0 && _y < 8);

        int8 deltaX = _x - x;
        int8 deltaY = _y - y;
        // verificar se estamos capturando uma peça diagonalmente adjacente
        require((deltaX == 1 || deltaX == -1) && (deltaY == 1 || deltaY == -1));

        // pular sobre
        x = _x + deltaX;
        y = _y + deltaY;
    }

    /// @dev não pode deixar a diretoria sob nenhuma condição
    function invariant() public view {
        assert(x >= 0 && x < 8 && y >= 0 && y < 8);
    }
}
Enter fullscreen mode Exit fullscreen mode

O código é simples: criamos um contador em uma determinada posição. Ele então pode capturar outras peças.

A parte interessante é a última função — ela define uma invariante que deve ser mantida o tempo todo. A invariante é simples — o contador não pode sair do tabuleiro. Vamos compilar o contrato e ver se nossA invariante já foi quebradA (observe os argumentos extras solc - eles ativam o SMTChecker em modo agressivo, mas preciso):

~/src/smtchecker_demo ❯❯❯ solc 1.sol --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0
Advertência: CHC: A violação da asserção acontece aqui.
Counterexample:
x = 0, y = 8
Transaction trace:
LazyCounter.constructor(2, 6)
State: x = 2, y = 6
LazyCounter.capture(1, 7)
State: x = 0, y = 8
LazyCounter.invariant()
 --> 1.sol:32:9:
  |
32 |         assert(x >= 0 && x < 8 && y >= 0 && y < 8);
  |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Enter fullscreen mode Exit fullscreen mode

Ops, nossa invariante está quebrada. O SMTChecker ainda nos dá um contra-exemplo! Se nossa peça está em (2, 6) e captura a peça em (1, 7), ela acaba em (0, 8) que está fora do tabuleiro. Esquecemos de verificar a validade da posição do contador após a captura.

É importante entender o que o SMTChecker acabou de fazer: demos a ele um contrato com um conjunto de limites operacionais (require instruções que definem o conjunto de entradas válidas) e uma invariante. O SMTChecker fez uma análise exaustiva: chamou todas as funções públicas em um loop com todas as entradas possíveis, em todas as combinações possíveis. Na realidade, ele não faz uma abordagem de força bruta (isso seria muito caro), mas depende da matemática para fazê-lo funcionar (não vou fingir entender isso completamente, há alguns detalhes aqui).

Aqui está outro exemplo que mostra que o SMTChecker tenta longas sequências de transações para testar invariantes: um contrato que implementa um cavalo de xadrez. Adicionaremos uma invariante que sabemos que não é válida, apenas para dar ao SMTChecker algo para encontrar: o cavalo não pode alcançar a posição (7, 7). O SMTChecker também nos dará um contra-exemplo.

// SPDX-License-Identifier: MIT
pragma solidity >=0.8.7;

contract Knight {
    int8 private x;
    int8 private y;

    function isValidPosition() internal view returns (bool) {
        return x >= 0 && x < 8 && y >= 0 && y < 8;
    }

    function move1() public {
        x += 1;
        y += 2;
        require(isValidPosition());
    }

    function move2() public {
        x += 2;
        y += 1;
        require(isValidPosition());
    }

    function move3() public {
        x += 2;
        y -= 1;
        require(isValidPosition());
    }

    function move4() public {
        x -= 1;
        y -= 2;
        require(isValidPosition());
    }

    function move5() public {
        x -= 1;
        y += 2;
        require(isValidPosition());
    }

    function move6() public {
        x -= 2;
        y += 1;
        require(isValidPosition());
    }

    function move7() public {
        x -= 2;
        y -= 1;
        require(isValidPosition());
    }

    function move8() public {
        x -= 1;
        y -= 2;
        require(isValidPosition());
    }

    function get_to_7_7() public view {
        assert(!(x == 7 && y == 7));
    }
}
Enter fullscreen mode Exit fullscreen mode 
~/src/smtchecker_demo ❯❯❯ solc 2.sol --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0
Advertência: CHC: A violação da asserção acontece aqui.
Counterexample:
x = 7, y = 7
Transaction trace:
Knight.constructor()
State: x = 0, y = 0
Knight.move2()
    Knight.isValidPosition() -- internal call
State: x = 2, y = 1
Knight.move2()
    Knight.isValidPosition() -- internal call
State: x = 4, y = 2
Knight.move5()
    Knight.isValidPosition() -- internal call
State: x = 3, y = 4
Knight.move1()
    Knight.isValidPosition() -- internal call
State: x = 4, y = 6
Knight.move3()
    Knight.isValidPosition() -- internal call
State: x = 6, y = 5
Knight.move1()
    Knight.isValidPosition() -- internal call
State: x = 7, y = 7
Knight.get_to_7_7()
  --> 2.sol:61:9:
   |
61 |         assert(!(x == 7 && y == 7));
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Enter fullscreen mode Exit fullscreen mode

Organizado! Deu-nos a sequência de passos que move o cavalo de (0, 0) para (7, 7).

Prática

Isenção de responsabilidade: Todo o resto é um grande experimento para ver como torná-lo útil em 'configurações de produção'. Pode haver outros caminhos, não afirmo ter encontrado O CAMINHO.

Vamos fazer algo um pouco mais prático: parte de um AMM: provedores de liquidez adicionam liquidez a um par de negociação, mas ninguém pode realmente negociar.

  • Após a construção, o proprietário deposita alguns (x) tokens X e alguns (y) tokens Y. AMM gera x * y tokens LP
  • Qualquer pessoa pode depositar tokens x1 X e y1 Y, desde que isso não altere a proporção dos saldos X/Y (x1/y1 == xReserves / yReserves). AMM gera totalSupply(LP) * (x1 / xReserves) tokens LP
  • Suportamos apenas tokens ERC20 de ponto fixo com decimais() == 18

É isso. Não estamos nem distribuindo tokens LP, apenas gerando-os.

// SPDX-License-Identifier: MIT
pragma solidity >=0.8.7;

/// @dev mínimo necessário de IERC20 e IERC20Metadata que usaremos
interface IERC20Metadata {
    function decimals() external view returns (uint8);

    function transferFrom(address sender, address recipient, uint256 amount) external returns (bool);
}


contract AMMPair {
    IERC20Metadata x;
    IERC20Metadata y;

    uint256 xReserves;
    uint256 yReserves;

    uint256 totalSupply;

    constructor(IERC20Metadata _x, IERC20Metadata _y, uint256 depositX, uint256 depositY) {
        require(_x.decimals() == 18);
        require(_y.decimals() == 18);
        require(depositX != 0);
        require(depositY != 0);

        x = _x;
        y = _y;

        xReserves = depositX;
        yReserves = depositY;
        totalSupply = depositX * depositY / 1e18;

        x.transferFrom(msg.sender, address(this), depositX);
        y.transferFrom(msg.sender, address(this), depositY);
    }

    function addLiquidity(uint256 depositX, uint256 depositY) public returns (uint256) {
        require(depositX != 0, "depositX != 0");
        require(depositY != 0, "depositY != 0");
        require(depositX * 1e18 / depositY == xReserves * 1e18 / yReserves, "unbalancing");

        uint256 extraSupply = depositX * totalSupply / xReserves;

        xReserves += depositX;
        yReserves += depositY;
        totalSupply += extraSupply;

        x.transferFrom(msg.sender, address(this), depositX);
        y.transferFrom(msg.sender, address(this), depositY);

        return extraSupply;
    }
}
Enter fullscreen mode Exit fullscreen mode

Que invariantes podemos adicionar? Não muitas — talvez as reservas não estejam vazias (xReserves != 0 && yReserves != 0), mas é isso.

Vamos virar a definição de uma invariante de lado e chamá-la de 'invariante dinâmica': conhecendo o estado antes e depois de executar addLiquidity, o que podemos afirmar?

contract AMMPair {
    // ...
    function invariantAddLiquidity(uint256 depositX, uint256 depositY) public {
        uint256 oldSupply = totalSupply;
        uint256 oldXReserves = xReserves;

        uint256 supplyAdded = addLiquidity(depositX, depositY);
        assert(depositX / oldXReserves == supplyAdded / oldSupply);
        revert("all done");
    }
}
Enter fullscreen mode Exit fullscreen mode

Observe o revert() no final - ele garante que a função invariante não tenha efeitos colaterais (pense nisso como uma função view). Vamos experimentá-lo!

~/src/smtchecker_demo ❯❯❯ solc --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0 --model-checker-contracts 3.sol
...
Enter fullscreen mode Exit fullscreen mode

Isso vai demorar um pouco (algumas horas na melhor das hipóteses). Não é prático o suficiente para uma invariante simples.

O que poderia torná-lo lento? Meu palpite é de endereços e chamadas externas (transferFrom) — o SMTChecker os modela como funções desconhecidas que podem fazer qualquer coisa, inclusive chamar seu contrato de volta. Isso é bom e útil (eles podem encontrar problemas de reentrância), mas não é prático para o nosso cenário.

Reestruturaremos o contrato: retire todas as comunicações externas para um contrato separado. Nosso contrato 'principal' manterá um estado mínimo e será apenas um triturador de números. Bônus adicionado - torna o acompanhamento de CEI (checks-effects-interactions) quase automático.

contract AMMPairEngine {
    uint256 xReserves;
    uint256 yReserves;

    uint256 totalSupply;

    constructor(uint256 depositX, uint256 depositY) {
        require(depositX != 0, "depositX != 0");
        require(depositY != 0, "depositY != 0");

        xReserves = depositX;
        yReserves = depositY;
        totalSupply = depositX * depositY / 1e18;
    }

    function addLiquidityStateChange(uint256 depositX, uint256 depositY)
        internal
        returns (uint256)
    {
        require(depositX != 0, "depositX != 0");
        require(depositY != 0, "depositY != 0");
        require(
            (depositX * 1e18) / depositY == (xReserves * 1e18) / yReserves,
            "unbalancing"
        );

        uint256 extraSupply = (depositX * totalSupply) / xReserves;

        xReserves += depositX;
        yReserves += depositY;
        totalSupply += extraSupply;

        return extraSupply;
    }

    function invariant1() public view {
        assert(xReserves > 0);
        assert(yReserves > 0);
    }

    function invariantAddLiquidity(uint256 depositX, uint256 depositY) public {
        uint256 oldSupply = totalSupply;
        uint256 oldXReserves = xReserves;

        uint256 supplyAdded = addLiquidityStateChange(depositX, depositY);
        assert(depositX / oldXReserves == supplyAdded / oldSupply);
        revert("all done");
    }
}

contract AMMPair is AMMPairEngine {
    IERC20 x;
    IERC20 y;

    constructor(
        IERC20 _x,
        IERC20 _y,
        uint256 depositX,
        uint256 depositY
    ) AMMPairEngine(depositX, depositY) {
        require(_x.decimals() == 18);
        require(_y.decimals() == 18);

        x = _x;
        y = _y;

        x.transferFrom(msg.sender, address(this), depositX);
        y.transferFrom(msg.sender, address(this), depositY);
    }

    function addLiquidity(uint256 depositX, uint256 depositY)
        public
    {
        addLiquidityStateChange(depositX, depositY);

        x.transferFrom(msg.sender, address(this), depositX);
        y.transferFrom(msg.sender, address(this), depositY);
    }
}
Enter fullscreen mode Exit fullscreen mode

AMMPairEngine tem addLiquidityStateChange como função interna. Ele deve ser chamado por AMMPair (que herda de AMMPairEngine). As únicas funções públicas AMMPairEngine são as invariantes. Se não os quisermos no código implantado, eles podem ser movidos para o contrato AMMPairEngineTest is AMMPairEngine.

~/src/smtchecker_demo ❯❯❯ time solc --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0 --model-checker-contracts 3.sol:AMMPairEngine 3.sol
Advertência: CHC: A divisão por zero acontece aqui.
Counterexample:
xReserves = 2, yReserves = 2, totalSupply = 0
depositX = 1
depositY = 1
oldSupply = 0
oldXReserves = 1
supplyAdded = 0
Transaction trace:
AMMPairEngine.constructor(1, 1)
State: xReserves = 1, yReserves = 1, totalSupply = 0
AMMPairEngine.invariantAddLiquidity(1, 1)
    AMMPairEngine.addLiquidityStateChange(1, 1) -- internal call
   --> 3.sol:117:43:
    |
117 |         assert(depositX / oldXReserves == supplyAdded / oldSupply);
    |                                           ^^^^^^^^^^^^^^^^^^^^^^^
Advertência: CHC: A violação da asserção acontece aqui.
   --> 3.sol:117:9:
    |
117 |         assert(depositX / oldXReserves == supplyAdded / oldSupply);
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
solc --model-checker-engine chc --model-checker-show-unproved  0   3.sol  7.11s user 0.17s system 98% cpu 7.357 total
Enter fullscreen mode Exit fullscreen mode

Há uma divisão por zero que causa violação de asserção. O contra exemplo (depositX = 1; depositY = 1; oldSupply = 0) torna o problema óbvio: o criador do contrato depositou 1e-18 de X e 1e-18 de Y. Isso fez o contrato emitir 0 tokens LP (1e-36 é muito pequeno para ser representado com matemática de ponto fixo de 18 casas decimais). Vamos mudar para matemática de 36 decimais e isso deve cuidar disso:

contract AMMPairEngine {
    // ...
    constructor(uint256 depositX, uint256 depositY) {
        // ...
        totalSupply = depositX * depositY; // removido '/1e18'
    }
    // ...
}
Enter fullscreen mode Exit fullscreen mode 
~/src/smtchecker_demo ❯❯❯ time solc --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0 --model-checker-contracts 3.sol:AMMPairEngine 3.sol
Advertência: CHC: A violação da asserção pode acontecer aqui.
   --> 3.sol:117:9:
    |
117 |         assert(depositX / oldXReserves == supplyAdded / oldSupply);
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
solc --model-checker-engine chc --model-checker-show-unproved  0   3.sol  75.19s user 0.50s system 99% cpu 1:16.27 total
Enter fullscreen mode Exit fullscreen mode

Observe a mudança: não há divisão por zero e “Violação de asserção acontece aqui” agora é “Violação de asserção pode acontecer aqui”. Não acho seguro interpretar a incerteza como “definitivamente não há violações de asserção aqui”, mas é um sucesso parcial. Vou precisar fazer mais escavações para entender melhor o que está acontecendo aqui.

ATUALIZAÇÃO 09/05/2021: Leo Alt apontou que 'pode acontecer' não é bom o suficiente para chamar isso de 'sucesso parcial' - é muito difícil para o SMTChecker provar a afirmação, então não podemos confiar nisso:

q

y

FWIW, você pode provar a matemática do último exemplo manualmente, mas isso claramente não é dimensionado. Violação de asserção no código original com um contra-exemplo:

2

Prove que não há violação de asserção no novo código:

1

Conclusão

O SMTChecker pode ser sua superpotência pessoal - provavelmente precisa de algum trabalho e seus contratos precisam ser escritos com isto em mente. Mas se as estrelas se alinharem, todos poderão desfrutar dos benefícios da verificação formal automática.

Espero passar algum tempo analisando mais profundamente o SMTChecker, fique atento.

Alternativas

  1. Manticore é um mecanismo de execução simbólica que pode fazer coisas semelhantes ao SMTChecker. É altamente programável - por um lado, pode fazer menos coisas diferentes (invariantAddLiquidity tem 2 argumentos, SMTChecker explorou todas as entradas possíveis para eles; Manticore não pode fazer isto). Por outro lado, essas coisas são implementáveis, além de termos mais controle sobre o processo de verificação (talvez possamos fazer algumas suposições sobre contratos externos?)
  2. Echidna é uma ferramenta fuzzing — usa uma ideia semelhante de invariantes e tenta aleatoriamente encontrar entradas que as quebrem. Isso não prova que as invariantes são válidas (talvez tenha falhado em encontrar esse caso extremo), mas pode ser rápido e descobrir muitas falhas não extremas. Echidna usa a mesma sintaxe de Manticore, então ambos podem ser usados ​​em paralelo (pelo menos em teoria).
  3. Scribble tem uma abordagem diferente — você anota cada função com invariantes dinâmicas. Ele usa sua própria linguagem para as invariantes e pode instrumentar seu código com as invariantes materializadas.
  4. Inúmeras ferramentas de análise estática/outras fuzzing — elas são super úteis, mas estão fora do escopo deste artigo.

Agradecimentos

A Alberto Cuesta Cañada pela maioria das referências acima e a ideia do bebê AMM

Junte-se ao canal Coinmonks no Telegram e ao canal do Youtube para aprender sobre negociação e investimento em criptomoedas

Leia também

Agradecimentos a Alberto Cuesta Cañada.

Artigo escrito por Owleksiy e traduzido por Marcelo Panegali.

Top comments (0)


Leia o próximo

cavazinf profile image

CISNE NEGRO em criptoativos.

Tiago Ferreira Cavazin -

cavazinf profile image

A Fantástica Fábrica de Aplicações para Web3: Desbravando os Desafios de Iniciar no Ecossistema

Tiago Ferreira Cavazin -

s4mp41xao profile image

Falha crítica da Nethermind interrompe o processamento de blocos Ethereum.

Samuel Paixão -

s4mp41xao profile image

MetaMask: Desvendando o Staking com Validadores Ethereum

Samuel Paixão -