Teste de Invariantes - Entrando na Matrix

A suíte de testes de invariantes que criamos para a auditoria de segurança mencionada neste artigo está disponível no GitHub. Para saber mais sobre segurança e auditorias de contratos inteligentes, visite Cyfrin.io. Uma lista de nossos relatórios públicos de auditoria pode ser encontrada aqui.

Imagem por Markus Spiske, no Unsplash

O Neo nos ensinou que existem duas realidades:

1. Realidade Base - onde vivemos, e;
2. A Matrix - uma simulação da Realidade Base.

Considere a rede principal (Mainnet) da Ethereum como a Realidade Base: o mundo real. Ninguém tem acesso root aqui e as coisas que acontecem têm consequências. Seria loucura implantar contratos nesse ambiente sem considerar as consequências. Portanto, devemos testá-los em uma simulação antes de liberá-los mundo afora.

Aqui entra a Suíte de Testes de Invariantes. O simulador da Matrix/realidade base.

Ninguém tem acesso root à Realidade Base. No entanto, temos acesso root à Matrix. Podemos definir tudo o que pode acontecer e tudo o que deve permanecer verdadeiro, não importa o quê. Ao classificar essas coisas, podemos começar a raciocinar melhor sobre elas:

• Ações - um conjunto de tudo o que pode acontecer durante uma simulação.
• Invariantes - um conjunto de verdades que devem sempre ser mantidas, não importa qual Ação ou sequência de Ações seja executada.

Ao aplicar conjuntos de Ações e Invariantes, criamos um mundo simulado que utiliza o Foundry para detectar casos extremos e bugs difíceis de encontrar antes de chegarmos perto da Realidade Base.

A Solução Definitiva?

Repetindo o que já foi dito: as auditorias não são uma solução definitiva, e nenhuma ferramenta é. Embora a inteligência artificial provavelmente chegará lá um dia, as ferramentas não podem substituir completamente o processo de auditoria, mas certamente podem ajudar. Nós usamos diversas ferramentas para auxiliar na realização de auditorias de segurança. Recentemente, a mais produtiva delas tem sido o uso do Foundry para criar Suítes de Testes de Invariantes que simulam condições do mundo real.

Pensamos nas Suítes de Testes de Invariantes começando com algumas suposições superficiais. Assumimos que os problemas mais básicos (controle de acesso, modificadores corretos, reentrância, erros de digitação, etc.) estão cobertos em testes unitários (estamos assumindo um nível básico de cobertura de testes, o que significa que 100% dos caminhos de código são cobertos por testes unitários). Fazemos isso porque queremos que nossa suíte de testes tente quebrar Invariantes do contrato usando apenas Ações válidas. Se pudermos demonstrar que a verdade de um sistema não é verdadeira em todos os cenários válidos possíveis, temos que assumir que alguém tirará proveito disso na rede principal, especialmente se puder lucrar com isso.

Escrevendo Testes de Invariantes Efetivos

Os fuzzers são limitados, assim como sua capacidade computacional é limitada. Se definirmos um conjunto de Ações, o fuzzer escolherá e executará aleatoriamente uma delas. E se ele escolher uma Ação errada no momento errado ou for enganado por um endereço incorreto, e o contrato reverter como esperado? Isso é algo básico. Sabemos que ele deve reverter e que os testes unitários devem cobrir isso. Portanto, idealmente, queremos que nossos testes de invariantes evitem chamar essas Ações, pois isso desperdiça chamadas de fuzz valiosas que poderiam ser melhor utilizadas em Ações válidas.

Portanto, um dos desafios ao escrever testes de Invariantes é obter o máximo valor deles, mesmo que o fuzzer do Foundry escolha uma Ação inválida. Vamos considerar um exemplo de teste de Invariantes dos contratos de Staking v0.1 da Chainlink.

Nos contratos de Staking v0.1 da Chainlink, diferentes estados permitem um conjunto específico de ações. O fluxo de estados é o seguinte: Fechado → Aberto → Fechado. Antes que o pool possa aceitar LINK para ser colocado em stake, o pool tem que ser aberto pelo endereço do administrador. Se tornarmos a Ação stake() disponível para o fuzzer antes que o pool tenha sido aberto, essa Ação provavelmente será chamada pelo fuzzer e reverterá. Isso é esperado, mas, até onde sabemos, é uma chamada de fuzz desperdiçada. Isso reduziu o valor geral da simulação, já que o fuzzer não irá tão fundo quanto poderia.

O mesmo vale para funções onlyOwner. Se um endereço aleatório chamar uma delas, ela reverterá, desperdiçando outra chamada. Se uma Suíte de Testes de Invariantes tiver muitos desses casos, a maioria das chamadas será desperdiçada por reversões desnecessárias que já conhecemos, tornando a suíte praticamente inútil. Portanto, algumas decisões arquiteturais devem ser tomadas para garantir que esses casos não ocorram e que a suíte seja a mais valiosa possível.

Felizmente, nosso espaço está cheio de lendas pseudônimas que se empenham em contribuir com ideias e evoluir o espaço. Recentemente, horsefacts escreveu um artigo usando o WETH9 como alvo de teste, descrevendo como estruturar uma suíte de testes de invariantes usando um padrão Handler (desde então adotado na documentação oficial do Foundry). Ele introduz o conceito de "variáveis fantasmas" para acompanhar o estado assumido dentro de um contrato alvo.

É aqui que os Invariantes _e as _Ações que definimos anteriormente podem ser descritos de forma mais concreta. Ele define dois contratos, o Handler e o Invariants.

Handler - define as Ações.

Invariants - define os Invariantes.

Escrevendo Invariantes em uma Auditoria de Segurança

Durante uma auditoria do protocolo Wells da Beanstalk Farms, escrevemos uma Suíte de Testes de Invariantes. O protocolo Wells é um framework para implantar pools de liquidez de mercado automatizado de função constante, que podem ser configurados para usar qualquer número de tokens e qualquer função (sendo o caso base a função de produto constante). O pool e a função são separados em contratos diferentes, com o objetivo de serem peças que podem ser compostas em um ecossistema maior.

Felizmente, o protocolo Wells já usava o Foundry para seus testes, então pudemos aproveitar as funções auxiliares que eles já haviam escrito (setupWell() e várias versões sobrecarregadas para configurações mais granulares) para implantar um conjunto de contratos que poderíamos testar.

O Primeiro Invariante

O Well (pool) usa a função terceirizada (ConstantProduct2 neste caso) para calcular o fornecimento e as reservas totais quando ocorre uma mudança nas reservas, seja fornecendo ou removendo liquidez ou trocando de um token para outro. O primeiro Invariante que identificamos foi este:

well.totalSupply() == wellFunction.calcTotalLpSupply()

Este Invariante testa se o fornecimento total de tokens LP deve sempre ser igual ao fornecimento total calculado da função wellFunction. Bem simples. O primeiro passo está completo, mas ainda não definimos nenhuma Ação, então nossa Suíte de Testes de Invariantes faz apenas o deploy do Well até agora.

A Primeira Ação - Adicionando Liquidez

Em seguida, começamos a adicionar Ações ao nosso Handler. Primeiro, vamos adicionar liquidez. Seguindo o exemplo do WETH9 do horsefacts, temos que fazer algumas coisas aqui:

1. Gerar um endereço aleatório, uma quantidade de token0 e uma quantidade de token1.
2. Fingir ser o endereço gerado.
3. Limitar as quantidades a valores razoáveis e cunhar tokens para o endereço gerado.
4. Aprovar para que o Well possa gastar nossos tokens.
5. Adicionar a liquidez.
6. Adicionar o endereço à nossa lista de LPs da "variável fantasma".

A função (arquivo completo aqui) se parece com isso:

/// @dev addLiquidity
function addLiquidity(uint addressSeed, uint token0AmountIn, uint token1AmountIn) public {
   // Limitar a semente de endereço
   address msgSender = _seedToAddress(addressSeed);
   changePrank(msgSender);
   // Limitar a quantidade de tokens
   token0AmountIn = bound(token0AmountIn, 1, type(uint96).max);
   token1AmountIn = bound(token1AmountIn, 1, type(uint96).max);

   uint[] memory tokenAmountsIn = new uint[](2);
   tokenAmountsIn[0] = token0AmountIn;
   tokenAmountsIn[1] = token1AmountIn;
   // Cunhar tokens para o remetente
   IERC20[] memory mockTokens = s_well.tokens();
   for (uint i = 0; i < mockTokens.length; i++) {
       MockToken(address(mockTokens[i])).mint(msgSender, tokenAmountsIn[i]);
       // Aprovar o Well
       mockTokens[i].approve(address(s_well), tokenAmountsIn[i]);
   }

   // Adicionar liquidez
   uint minLpAmountOut = s_well.getAddLiquidityOut(tokenAmountsIn);
   uint lpAmountOut = s_well.addLiquidity(tokenAmountsIn, minLpAmountOut, msgSender, block.timestamp);
   assertGe(lpAmountOut, minLpAmountOut);
   // Adicionar o LP à lista
   s_LPs.add(msgSender);
}

Por que "Passo 6: Adicionar o endereço à nossa lista de LPs da "variável fantasma"? Este é o primeiro exemplo de preparação para evitar aquelas reversões temidas que desperdiçam chamadas de fuzz. Essa variável fantasma ainda não é necessária, mas será quando a Ação removeLiquidity for implementada. Isso ocorre porque, para um endereço remover a liquidez, ele deve possuir tokens LP. Caso contrário, ele reverterá, desperdiçando a chamada. Mais sobre isso depois…

Ao executar o comando forge test - match-contract Invariants, vemos que até agora tudo está ok; temos um diagnóstico limpo. Nesta etapa, isto é o que a nossa simulação faz:

1. Implanta um Well e uma WellFunction.
2. Adiciona liquidez de centenas de endereços gerados aleatoriamente.

O primeiro Invariante é válido.

A Segunda Ação - Removendo Liquidez

Em seguida, adicionamos a Ação para remover liquidez:

1. Verifique se nossa lista de LPs da variável fantasma não tem comprimento zero.
2. Obtenha um índice de endereço LP gerado e uma quantidade de token LP.
3. Limite esses valores a valores razoáveis.
4. Finja ser o endereço LP obtido da lista da variável ​​fantasma s_LPs.
5. Remova a liquidez.
6. Remova o endereço da lista da variável fantasma se ela não tiver nenhum token LP (se toda a sua liquidez for removida).

Vai ficar assim:

/// @dev removeLiquidity
function removeLiquidity(uint addressIndex, uint lpAmountIn) public {
   if (s_LPs.length() == 0) {
       return;
   }
   // Limitar o índice de endereço
   address msgSender = _indexToLpAddress(addressIndex);
   changePrank(msgSender);
   // Limitar quantidade de LP
   lpAmountIn = bound(lpAmountIn, 0, s_well.balanceOf(msgSender));

   // Remover liquidez
   uint[] memory minTokenAmountsOut = s_well.getRemoveLiquidityOut(lpAmountIn);
   uint[] memory tokenAmountsOut =
       s_well.removeLiquidity(lpAmountIn, minTokenAmountsOut, msgSender, block.timestamp);

   assertGe(tokenAmountsOut[0], minTokenAmountsOut[0]);
   assertGe(tokenAmountsOut[1], minTokenAmountsOut[1]);

   // Remover o LP da lista se ela não tiver mais LP
   if (s_well.balanceOf(msgSender) == 0) {
       s_LPs.remove(msgSender);
   }
}

Observe que esta função retorna se a lista de LPs da variável fantasma estiver vazia. Se verdadeiro, esta é uma chamada de fuzz desperdiçada para esta ação. Isso pode ser mitigado de várias maneiras:

1. Adicionando liquidez de vários endereços durante a função setUp(), reduzindo a probabilidade de que o fuzzer remova toda a liquidez antes de adicionar mais.
2. Redirecionando a chamada para a Ação addLiquidity() no caso de uma lista de LPs com comprimento zero.

Neste estágio, isto é o que a nossa simulação faz:

1. Implanta um Well e um WellFunction.
2. Adiciona liquidez de centenas de endereços gerados aleatoriamente.
3. Remove aleatoriamente a liquidez de endereços com tokens LP.

Ao executar os testes desta vez, nos deparamos com erros.

Uh oh

Nosso Invariante inicial falhou... Ao executar o comando de teste acima com -vvv, o Foundry nos dá um rastreamento completo de cada Ação realizada, os valores que essas Ações usaram e o Invariante que falhou. Muito útil.

Usamos isso para criar um teste unitário que recriou o Invariante quebrado para incluir no relatório final da auditoria e encontrar maneiras de mitigá-lo.

A Cebola da Segurança

Este Invariante quebrado nos deixou presos no problema por vários dias, resultando em uma descoberta de alta gravidade que abordou a matemática subjacente, direções de arredondamento e peculiaridades arquitetônicas. À medida que construímos a Suíte de Testes de Invariantes em paralelo com nossa auditoria manual, descobrimos vários problemas adicionais que disponibilizamos à Beanstalk Farms em nosso relatório. Também tornamos a Suíte de Testes de Invariantes de código aberto, para que qualquer mudança futura no protocolo Wells possa ser testada contra essa camada extra de defesa.

Afinal, a segurança não é binária; é fuzzy (com trocadilho). Compreende camadas de técnicas, estratégias, melhores práticas, testes, revisões e muito mais, que nunca serão uma solução definitiva, mas podem ser como uma cebola. Quanto mais camadas de segurança ela tiver, mais provável será a proteção do núcleo.

Na Cyfrin, acreditamos em elevar a segurança do espaço Web3. Continuaremos a fornecer Suítes de Testes de Invariantes juntamente com nossas auditorias para que os desenvolvedores possam aprender e aplicá-las a todos os sistemas de contratos inteligentes que criam.

A Suíte de Teste de Invariantes que criamos para a auditoria de segurança mencionada neste artigo está disponível no GitHub. Para saber mais sobre segurança de contratos inteligentes e auditorias de contratos inteligentes, visite Cyfrin.io. Uma lista de nossos relatórios públicos de auditoria pode ser encontrada aqui.

Artigo original publicado por Alex Roan. Traduzido por Paulinho Giovannini.