Contexto
Na ciência da computação, a representação em ponto fixo é um método de representar números reais armazenando um número fixo de dígitos de sua parte fracionária (ou seja, os dígitos à direita de um ponto decimal). É evidente que a manipulação de números de ponto fixo é essencial para qualquer aplicativo DeFi, por exemplo, para calcular taxas de juros, índice de empréstimos, determinar a curva de preços da AMM etc.
O que talvez seja menos óbvio é que mesmo pequenos erros de arredondamento ou de implementação podem se acumular e se agravar, podendo levar a uma oportunidade de arbitragem ou até mesmo a uma vulnerabilidade de segurança. Exemplos recentes incluem:
- Exploração do Alpha Homora (fevereiro de 2021)
- O bug de empréstimo de spl-token na biblioteca do programa Solana (dezembro de 2021)
- Exploração do pool de distribuição de HDL da Yieldly (março de 2022)
- Exploração do Hundred Finance (abril de 2023)
- Exploração da Midas Capital (junho de 2023)
Consulte também a seção "Security Considerations" (Considerações de segurança) no ERC-4626 (Tokenized Vaults), que recomenda o uso de direções de arredondamento distintas e opostas ao calcular os compartilhamentos do cofre.
Dois excelentes recursos para a implementação de funções matemáticas avançadas no Solidity são a série de blogs Math in Solidity, de Mikhail Vladimirov, e o site de Remco Bloeman. Esse último inspirou uma das bibliotecas de ponto fixo mais populares, eficientes em termos de gás e sofisticadas do Solidity - a biblioteca PRBMath, escrita por Paul Razvan Berg. Em geral, a biblioteca é incrivelmente bem escrita e mantida, incluindo vários testes de unidade para suas diversas funções. No entanto, usando o Equivalence Checker, descobrimos recentemente uma falha de projeto até então desconhecida na biblioteca PRBMath que afeta a função:
function mulDivSigned(int256 x, int256 y, int256 denominator) pure
returns (int256 result)
///Calcula o piso(x*y÷denominador) com precisão total.
O problema é simples, mas, quando implementado no contexto do DeFi, pode levar a uma vulnerabilidade crítica e à perda de fundos. Ele está presente em todas as instâncias da biblioteca PRBMath com número de versão a partir da 1.1.0 e até a versão 4.0 (inclusive).
Até onde sabemos, essa é a primeira vez que uma ferramenta automática encontra um bug em uma biblioteca Solidity pública e de código aberto.
Descrição do bug
Em termos gerais, o algoritmo que o PRBMath está usando para calcular a multiplicação e a divisão assinadas pode ser dividido em três etapas
- Extrai os sinais e os valores absolutos das entradas:
- (abs_x,abs_y,abs_d) := valores absolutos de (x,y,d)
- (sign_x,sign_y,sign_d) := sinais de (x,y,d)
// Obtenha os valores absolutos de x, y e o denominador.
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);
}
// Obtenha os sinais de x, y e o denominador.
uint256 sx;
uint256 sy;
uint256 sd;
//"sgt" é a instrução de montagem "signed greater than" e "sub(0,1)" é -1 em complemento de dois.
assembly ("memory-safe") {
sx := sgt(x, sub(0, 1))
sy := sgt(y, sub(0, 1))
sd := sgt(denominator, sub(0, 1))
}
- Calcula o valor absoluto do resultado reduzindo-o para o caso sem sinal:
uint256 abs_result = mulDiv(abs_x, abs_y, abs_d);
onde
function mulDiv(uint256 x, uint256 y, uint256 denominator) pure
returns (uint256 result)
/// Calcula floor(x*y÷denominator) com precisão total.
- Calcula o sinal geral e retorna o resultado:
uint256 overall_sign = sign_x ^ sign_y ^ sign_d;
result = (overall_sign == 0) ? -int256(abs_result) : int256(abs_result);
O problema é que a etapa 2 está errada. Na verdade, temos:
Portanto, sempre que o resultado for negativo, na verdade estamos arredondando para zero e não para menos infinito, o que leva a um erro de um por um.
Impacto e procedimento adequado de revelação
Ao trabalhar em um projeto, os auditores geralmente classificam os bugs de contratos inteligentes de acordo com a gravidade (quanto dano o bug poderia causar: negação de serviço, perda de fundos, etc.) e a dificuldade (quão difícil é para um agente mal-intencionado transformar a vulnerabilidade em uma exploração real).
Encontramos esse bug pela primeira vez ao trabalhar com um dos principais protocolos DeFi em um código AMM¹ não lançado que usava mulDivSigned como parte de seu cálculo da função de negociação. Em determinadas circunstâncias, esse erro aritmético teria permitido que um invasor forçasse os pools de liquidez a aceitarem negociações desfavoráveis², drenando sistematicamente o valor dos LP-tokens.
Originalmente, classificamos essa vulnerabilidade como de gravidade crítica, mas também de alta dificuldade, e notificamos o cliente que corrigiu o problema em seu código. No entanto, nossa classificação inicial ficou complicada quando percebemos que esse erro aritmético ocorre em várias instâncias da biblioteca PRBMath e, portanto, poderia influenciar muitos outros sistemas, inclusive os ativos.
Isso representou uma espécie de enigma: mesmo no mundo da segurança "clássica" dos computadores, os bugs de biblioteca são notoriamente perigosos e é muito difícil estimar a gravidade e a dificuldade em todos os projetos. Essa dificuldade é agravada na Ethereum, que não tem suporte nativo para bibliotecas atualizáveis ou um mecanismo para distribuir hotfixes e onde (por motivos de gás) as pessoas preferem apenas copiar funções específicas do PRBMath e ajustá-las em vez de importar toda a biblioteca.
Depois de consultar os principais pesquisadores de segurança samczsun e Mudit Gupta, realizamos uma pesquisa minuciosa em repositórios públicos (fora e dentro da cadeia) e notificamos os possíveis projetos vulneráveis de forma privada. Também entramos em contato com Paul Razvan Berg (o autor do PRBMath), que imediatamente entrou em contato conosco e confirmou as descobertas.
Como resultado de nossas investigações, acreditamos que, neste momento, pouquíssimos contratos inteligentes usam a parte aritmética assinada do PRBMath de forma problemática. Assim, e dada a natureza imutável dos contratos inteligentes, parece melhor expô-la ao público.
Mitigação
Para resolver o problema rapidamente, Paul emitiu uma correção temporária (versão 4.1) que altera a definição de mulDivSigned para arredondar para zero:
function mulDiv(uint256 x, uint256 y, uint256 denominator) pure
returns (uint256 result)
/// Calcula x*y÷denominador com precisão de 512 bits.
/// Observações:
/// - O resultado é arredondado para zero.
Em longo prazo, esse problema receberá uma solução de longo prazo como parte de um plano contínuo para fornecer suporte extensivo a vários modos de arredondamento no PRBMath,veja as discussões aqui para saber mais.
Conclusão
As 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 o consumo de gás), e auditá-las pode ser cansativo e difícil.
O bug acima demonstra que, mesmo com testes unitários abrangentes, há uma grande vantagem metodológica no processo de escrever uma especificação formal para um sistema (nem que seja apenas para garantir que nada foi ignorado ou esquecido). Ele também serve como um bom exemplo da expressividade da linguagem CVL - uma especificação CVL elementar (uma "especificação de equivalência")
foi capaz de detectar um bug de dois anos no código Solidity de uma biblioteca matemática que envolve extensos segmentos Yul, vários truques de hacking de bits e até mesmo um pouco de teoria dos números, tudo isso sem a necessidade de entender nada sobre os detalhes da implementação.
¹ Veja, por exemplo, o documento de pesquisa "SoK: Decentralized Exchanges (DEX) with Automated Market Maker (AMM) Protocols" para uma rápida revisão de DEXs, AMMs e terminologia DeFi relacionada.
² também conhecido como AMM- ou CFMM-invariante.
Artigo escrito por Netanel. A versão original pode ser encontrada aqui. Traduzido e adaptado por Dimitris Calixto.
Top comments (0)