Como Otimizar seu Consumo de Gás Sem se Dar Mal - Parte 2

Nesta publicação (a sequência de "Como otimizar seu consumo de gás sem se dar mal"), focamos nossa atenção nas bibliotecas Solidity/Yul que realizam os cálculos matemáticos e econômicos que estão no coração do mundo DeFi, e explicamos por que a verificação de equivalência é uma ferramenta poderosa nas mãos de desenvolvedores e auditores que desejam trabalhar com esse tipo de código.

Nosso plano é:

1. Discutir vulnerabilidades aritméticas e os respectivos exploits econômicos contra protocolos DeFi, usando a classe de Constant Function Market Maker (CFMM) como exemplo motivador.

2. Examinar alguns casos recentes em detalhe e explicar o erro de arredondamento encontrado na biblioteca PRBMath pela Certora.

3. Mostrar como podemos detectar o bug usando uma fácil "especificação de equivalência" de 3 linhas e provar que sua correção está livre de bugs.

Nota: Como esta é a segunda parte desta série, usaremos livremente os termos: verificação de equivalência, verificação formal, Provador Certora (Certora Prover), e Linguagem de Verificação Certora (Certora Verification Language, ou CVL), que foram discutidos na postagem anterior do blog. Você pode relembrar lendo a primeira parte aqui: Parte 1.

Um curso rápido em Formadores de Mercado Automatizado (AMMs)

Uma aplicação de finanças distribuídas (ou DeFi) é um sistema financeiro baseado em regras que opera de acordo com protocolos implementados por contratos inteligentes em uma (ou várias) blockchains. Uma categoria importante de aplicações DeFi são as exchanges descentralizadas (ou DEXs). Estas são definidas como um mercado onde os usuários (chamados de traders) podem trocar criptomoedas de maneira não custodial (ou seja, sem a necessidade de um ator intermediário para facilitar a transferência e custódia de fundos, mas possivelmente com a ajuda de um contrato inteligente intermediário). Ao contrário das exchanges tradicionais (ou até mesmo criptomoedas centralizadas), que muitas vezes dependem do modelo de livro de ordens ou de formadores de mercado designados para a provisão de liquidez, a maioria das DEXs depende de uma classe de protocolos conhecidos como formadores de mercado automatizados (AMMs).

No coração de cada AMM está uma coleção de pools de liquidez. Cada pool corresponde a um par de ativos cripto fungíveis (ou tokens), que denominamos como token A e token B no diagrama abaixo.

Usuários que depositam uma certa quantidade de cada token no pool são chamados de provedores de liquidez (ou LPs, para abreviar). Em troca de seu investimento, eles recebem um token de liquidez que essencialmente funciona como um 'recibo de depósito, e registra o valor de seu investimento em relação ao saldo atual de token A e token B depositado no pool.

Ao contrário dos livros de ordens (um protocolo peer-to-peer para combinar compradores e vendedores), um AMM implementa um método peer-to-pool onde cada usuário que deseja trocar uma certa quantidade de token A por token B interage com o próprio pool. Dessa forma, os traders têm acesso imediato à liquidez sem a necessidade de esperar por uma contraparte, enquanto os LPs lucram com o investimento devido às taxas de câmbio acumuladas pelo pool.

Os Formadores de Mercado de Função Constante (CFMMs) e o invariante de negociação

Como você deve ter notado até este ponto, há um detalhe muito importante que nossa descrição acima deixou de lado.

Pergunta: Suponha que um trader deseje trocar 1000 Tokens A. Como o AMM sabe exatamente quantos Tokens B enviar de volta?

O ponto chave é que o AMM não requer acesso a uma fonte externa de informações de preços (ou seja, um oráculo de preços) já que todo mercado é, em sua essência, um mecanismo de descoberta de preços.

Do ponto de vista matemático, quase todos os AMMs existentes hoje pertencem a uma classe conhecida como formadores de mercado de função constante (CFMMs). Isso significa que seu comportamento de negociação (ou “troca”) é governado por uma única função

cuja entrada é:

O AMM aceitará uma oferta de negociação se e somente se acreditar que a oferta é favorável a ele. Em termos concretos, isso significa que o AMM deve aceitar uma negociação se e somente se a desigualdade

for mantida.

Exemplo:

O formador de mercado de produto constante: Este é o caso mais clássico, introduzido por Martin Koppelmann e Vitalik Buterin em 2018 e implementado pela primeira vez pela Uniswap em 2018. A função de negociação deste CFMM (★) é de forma

Descompactando a fórmula, vemos que se denotamos o produto das duas reservas pela notação familiar k := x*y, então a desigualdade (★★) afirma precisamente que k deve ser não decrescente com cada negociação, que é um invariante bem conhecido dos AMMs de produto constante.

O que gostaríamos de enfatizar aqui é que não há nada mágico sobre a fórmula x*y = k! Existem muitos outros tipos de funções de negociação, algumas delas bastante matematicamente envolvidas.

Isso não deve ser surpresa: quando os casos de uso pretendidos são diferentes (por exemplo, moedas estáveis, derivativos, certos tipos de ativos sintéticos), o design do invariante CFMM deve refletir isso porque diferentes funções de negociação otimizam diferentes propriedades dos pares de tokens subjacentes.

Explorando a função de negociação

Pergunta: O que aconteceria se, devido a um bug aritmético ou erro de implementação, fosse possível para um usuário interagir com os contratos inteligentes do AMM de uma maneira que violasse a desigualdade (★★)?

Nesse caso, seria possível para um atacante forçar o AMM a executar consistentemente negociações desfavoráveis, drenando assim os fundos depositados no pool pelos provedores de liquidez (LPs).

Este tipo de transação de ataque é sutil: a quantidade de Tokens LP mantida por cada provedor de liquidez permanece a mesma antes e depois de cada ataque. No entanto, explorar tal falha permite a um atacante diminuir o valor deles. Uma analogia útil, embora aproximada, para o que acontece aqui é a inflação: os LPs ficam com a mesma quantidade de dinheiro (Tokens LP), mas a mesma quantidade de dinheiro agora compra muito menos bens (Tokens A ou B).

Exemplos recentes de tais ataques incluem:

• O exploit do Alpha Homora (fevereiro de 2021)
• O bug do sistema de empréstimos de tokens spl na Biblioteca de Programas Solana (dezembro de 2021)
• O exploit do pool de distribuição Yieldly HDL (março de 2022)
• O exploit do Hundred Finance (abril de 2023)
• O exploit do Midas Capital (junho de 2023)

Talvez o tipo mais comum de tal bug aritmético seja um erro de off-by-one que ocorre ao calcular a função de negociação e arredondar o resultado na direção errada¹.

Descrição do Bug

Observação: Como mencionamos na divulgação, o erro de arredondamento que encontramos está presente em várias versões da biblioteca PRBMath. Para simplificação, sempre nos referimos ao commit e2fc29127c (v4.0) nesta seção.

Falando de forma simplificada, a função Common.sol da biblioteca PRBMath

function mulDiv(uint256 x, uint256 y, uint256 denominator) pure returns (uint256 result)
/// @notice Calcula floor(x*y÷denominator) com precisão total.
/// Requisitos:
/// - O denominador não pode ser zero.
/// - O resultado deve caber em uint256.

implementa o seguinte algoritmo (crédito: Remco Bloeman) para cálculo eficiente de multiplicação-e-divisão sem sinal:

1. Use o Teorema Chinês do Resto (CRT) para obter uma representação de 512 bits do numerador como um par ordenado (prod1,prod0) de duas variáveis uint256 (para explicação, veja os posts de Remco sobre o teorema chinês do resto e multiplicação completa):

uint256 prod0; // 256 bits menos significativos
uint256 prod1; // 256 bits mais significativos
assembly ("memory-safe") {
 let mm := mulmod(x, y, not(0))
 prod0 := mul(x, y)
 prod1 := sub(sub(mm, prod0), lt(mm, prod0))
} // produto = prod1 * 2^256 + prod0.

1. Torne a divisão exata subtraindo o resto de (prod1, prod0):

    uint256 remainder;
    assembly ("memory-safe") {
        // Calcula o resto usando a instrução mulmod do Yul.
        remainder := mulmod(x, y, denominator)
        // Subtrai número de 256 bits de número de 512 bits.
        prod1 := sub(prod1, gt(remainder, prod0))
        prod0 := sub(prod0, remainder)
    }

1. Calcule o maior divisor de potência de dois (LPOTD) do denominador e divida por ele (veja os posts de Remco e a pergunta do Stack Exchange para explicação):

        uint256 lpotdod = denominator & (~denominator + 1);
        uint256 flippedLpotdod;

        assembly ("memory-safe") {
            // Fatora potências de dois do denominador.
            denominator := div(denominator, lpotdod)

            // Divide [prod1 prod0] por lpotdod.
            prod0 := div(prod0, lpotdod)
            flippedLpotdod := add(div(sub(0, lpotdod), lpotdod), 1)
        }

        // Desloca bits de prod1 para prod0.
        prod0 |= prod1 * flippedLpotdod;

1. Inverta o denominador mod 2²⁵⁶ usando o método de iteração de Newton-Raphson. (Veja o post e o artigo para o palpite inicial; Nota: Isso funciona em um campo finito por causa do lema de elevação de Hensel):

uint256 inverse = (3 * denominator) ^ 2; // inverso mod 2^4
inverse *= 2 - denominator * inverse; // inverso mod 2^8
inverse *= 2 - denominator * inverse; // inverso mod 2^16
inverse *= 2 - denominator * inverse; // inverso mod 2^32
inverse *= 2 - denominator * inverse; // inverso mod 2^64
inverse *= 2 - denominator * inverse; // inverso mod 2^128
inverse *= 2 - denominator * inverse; // inverso mod 2^256

1. Agora podemos dividir multiplicando prod0 pelo inverso modular do denominador:

result = prod0 * inverse;

produzindo o resultado necessário.

Sabendo disso, agora podemos revisar como a computação de multiplicação-e-divisão com sinal é realizada pela função Common.sol:

function mulDivSigned(int256 x, int256 y, int256 denominator) pure returns (int256 result)
/// @notice Calcula floor(x*y÷denominator) com precisão total.
/// Requisitos:
/// - Consulte os requisitos em {mulDiv}.
/// - Nenhuma das entradas pode ser `type(int256).min`.
/// - O resultado deve caber em int256.
///
/// @param x O multiplicando como um int256.
/// @param y O multiplicador como um int256.
/// @param denominator O divisor como um int256.
/// @return result O resultado como um int256.

que se baseia no cálculo mencionado anteriormente, implementando o seguinte algoritmo:

1. Extraia o valor absoluto das entradas:

uint256 xAbs;
uint256 yAbs;
uint256 dAbs;
unchecked {
  xAbs = x < 0 ? uint256(-x) : uint256(x);
  yAbs = y < 0 ? uint256(-y) : uint256(y);
  dAbs = denominator < 0 ? uint256(-denominator) : uint256(denominator);
}

1. Calcule o valor absoluto do resultado reduzindo ao caso sem sinal (ou seja, invocando a função de multiplicação-e-divisão sem sinal mencionada anteriormente nos valores absolutos das entradas):

uint256 resultAbs = mulDiv(xAbs, yAbs, dAbs);

1. Reverta com um erro personalizado se o valor absoluto do resultado não couber em uma variável int256:

if (resultAbs > uint256(type(int256).max)) {
  revert PRBMath_MulDivSigned_Overflow(x, y);
}

1. Calcule eficientemente o sinal de cada entrada:

uint256 sx;
uint256 sy;
uint256 sd;
assembly ("memory-safe") {
  // "sgt" é a instrução de montagem "maior que assinado" e "sub(0,1)" é -1 em complemento de dois.
  sx := sgt(x, sub(0, 1))
  sy := sgt(y, sub(0, 1))
  sd := sgt(denominator, sub(0, 1))
}

1. Compute o sinal geral tomando XOR e retorne o resultado:

// XOR sobre sx, sy e sd. Isso verifica se há 1 ou 3 sinais negativos nas entradas. Se houver, o resultado deve ser negativo. Caso contrário, deve ser positivo.
unchecked {
  result = sx ^ sy ^ sd == 0 ? -int256(resultAbs) : int256(resultAbs);
}

O problema é que o Passo 2 no algoritmo de mulDivSigned está errado, pois

Portanto, sempre que o resultado for negativo, na verdade estamos arredondando em direção a zero e não para menos infinito, levando a um erro de arredondamento.

Exemplo: Tome

(x,y,denominator) = (-180,1,14)

então:

(xAbs,yAbs,dAbs) = (180,1,14)
(sx,sy,sd) = (1,0,0)

e, portanto:

resultAbs = mulDiv(180, 1, 14) = floor(12.857...) = 12
resultado = -12

mas:

floor(-12.857) = -13 ≠ resultado

Verificação de Equivalência e Especificações Fáceis

Em geral, escrever especificações formais é um trabalho árduo. No entanto, para bibliotecas computacionais, o comportamento necessário é fácil de descrever matematicamente, de modo que a especificação quase se escreve sozinha. Considere as duas funções PRBMath que discutimos na seção anterior.

Olhando apenas para os comentários NatSpec da função, podemos produzir uma especificação para mulDivSigned:

Executar esta especificação² através o Provador Certora produz o contraexemplo que mostra que mulDivSigned tem um erro de arredondamento:

E é isso! Esse é o segredo todo. Nem precisamos ler o código ou entender como mulDivSigned (ou mulDiv) é implementado.

Conclusão

Bibliotecas matemáticas são os blocos de construção básicos do ecossistema DeFi. No entanto, elas são surpreendentemente difíceis de acertar (especialmente quando se tenta otimizar agressivamente seu consumo de gás), e auditá-las pode ser cansativo e difícil.

O bug acima demonstra a importância do verificador de equivalência da Certora e a expressividade da Linguagem CVL: uma especificação CVL elementar (uma "especificação de equivalência") pode detectar bugs no código Solidity de uma biblioteca matemática que envolve extensos segmentos Yul, inúmeros truques de manipulação de bits, e até um pouco de teoria dos números na mistura — tudo isso sem a necessidade de entender nada sobre os detalhes da implementação!

¹ Embora toda a nossa discussão até agora tenha sido no contexto de DEXs baseadas em AMMs, devemos pelo menos mencionar que esse problema ocorre em outras aplicações DeFi também. Por exemplo, no caso de plataformas de empréstimo, já foi notado no ERC-4626 (sob "considerações de segurança") que "... os implementadores do Vault devem estar cientes da necessidade de direções de arredondamento opostas e específicas nos métodos de visualização...". No entanto, para fins de simplificação, escolhemos nos concentrar em uma classe de aplicações DeFi em vez de tentar categorizar esse tipo de vulnerabilidade em toda a sua generalidade.

² Na terminologia usada na parte 1, produzir esta especificação é o "segundo modo" do verificador de equivalência, que compara código Solidity ou Yul contra expressões lógicas escritas na CVL. Para ser preciso, estamos produzindo apenas metade da especificação de equivalência aqui, já que não precisamos nos preocupar com as condições de reversão.

Autor: Netanel Rubin-Blaier

Editores: Uri Kirstein, Yura Sherman, David Mwihuri.

Traduzido por Paulinho Giovannini.