WEB3DEV Español

Cover image for Los Problemas de las Librerías de Punto Fijo en Solidity - Revelación del Bug Certora
Gabriella Alexandra Martinez Viloria
Gabriella Alexandra Martinez Viloria

Posted on

Los Problemas de las Librerías de Punto Fijo en Solidity - Revelación del Bug Certora

Image description

Autor: Netanel Rubin-Blaier.
Editores: Uri Kirstein, Yura Sherman.

Trasfondo

En la ciencia de la computación, la representación de punto fijo es un método para representar números reales, almacenando dígitos de números fijos en su parte fraccional (por ejemplo, los dígitos a la derecha del punto decimal). Está claro que la manipulación de números fijos, es esencial para cualquier aplicación DeFi, es decir, para calcular tasas de interés, prestar índices, determinar la curva de precio AMM, etc.

Lo que es menos obvio es que incluso un pequeño error o implementación puede acumular y generar, lo que potencialmente lleva a una oportunidad de arbitraje o, incluso, a una vulnerabilidad de la seguridad. Algunos ejemplos recientes incluyen:

Ve también la sección de “Consideraciones de Seguridad” en el ERC-4626 (los Búnker Tokenizados), los cuales recomiendan el uso de direcciones distintas redondeadas opuestas cuando se computa los intercambios de los búnker.

Dos recursos excelentes para implementar las funciones de matemática avanzada en Solidity son: la serie de blog de Mikhail Vladimirov Matemática en Solidity y la página web de Remco Bloeman. Este último inspiró a una de las bibliotecas de punto fijo más populares, eficiente con el gas y sofisticada: la biblioteca PRBMath, escrita por Paul Razvan Berg. En general, la biblioteca está, increíblemente, muy bien escrita y mantenida, incluyendo múltiples unidades de pruebas para sus funciones variadas. Sin embargo, usando Equivalence Checker, hemos descubierto recientemente un error de diseño previamente desconocido, en la biblioteca PRBMath que impacta la función:

function mulDivSigned(int256 x, int256 y, int256 denominator) pure
returns (int256 result)
/// @notice Calcula el piso(x*y÷denominator)con total precisión.
Enter fullscreen mode Exit fullscreen mode

El problema es simple, pero cuando se implementa en el contexto DeFi, puede llevar a vulnerabilidades críticas y la pérdida de fondos. Está presente en cada instancia de la biblioteca PRBMath, desde la versión 1.1.0 hasta (e incluyendo) la versión 4.0.

Hasta donde sabemos, esta es la primera vez que una herramienta automatizada ha encontrado un bug en una biblioteca de Solidity pública, de código abierto.

Descripción del Bug

A grosso modo, el algoritmo que PRBMath usa computa multiplicaciones y divisiones firmadas, las cuales pueden dividirse en tres pasos:

  1. Extrae las firmas de los valores absolutos de las entradas:
  • (abs_x,abs_y,abs_d) := valores absolutos de (x,y,d)
  • (sign_x,sign_y,sign_d) := firmas de (x,y,d)
// Obtiene los valores absolutos de x, y y del 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);
}
// Obtiene las firmas de x, y del denominador
uint256 sx;
uint256 sy;
uint256 sd;
// "sgt" es la instrucción de la asamblea de la “firma mayor a” y  "sub(0,1)" son los dos complementos en -1
assembly ("memory-safe") {
sx := sgt(x, sub(0, 1))
sy := sgt(y, sub(0, 1))
sd := sgt(denominator, sub(0, 1))
}
Enter fullscreen mode Exit fullscreen mode
  1. Computa el valor absoluto del resultado, reduciendo al caso sin firmar:
uint256 abs_result = mulDiv(abs_x, abs_y, abs_d);
Enter fullscreen mode Exit fullscreen mode

Donde

function mulDiv(uint256 x, uint256 y, uint256 denominator) pure
returns (uint256 result)
/// @notice Calcula el piso(x*y÷denominator) con total precisión.
Enter fullscreen mode Exit fullscreen mode
  1. Computa la firma en general y regresa el resultado:
uint256 overall_sign = sign_x ^ sign_y ^ sign_d;
result = (overall_sign == 0) ? -int256(abs_result) : int256(abs_result);
Enter fullscreen mode Exit fullscreen mode

El problema es que el paso 2 es erróneo. Realmente tenemos:

Image description

Así que, cuando el resultado es negativo, realmente estamos redondeándolo cerca a cero y no a menos infinito, llevando a un error por uno.

Impacto y Procedimiento de Revelación Adecuada

Mientras trabajamos en un proyecto, los auditores usualmente clasifican los bug de contratos inteligentes de acuerdo a la severidad (cuánto daño puede causar el bug: denegación de servicio, pérdida de fondos,...) y dificultad (qué tal difícil es para un actor maligno usar la vulnerabilidad para un exploit real).

Encontramos este bug por primera vez mientras trabajábamos con uno de los protocolos líderes DeFi en un código AMM¹ sin publicar, el cual usaba mulDivSigned como parte de su computación en la función de intercambio. Bajo ciertas circunstancias, este error aritmético pudo haber permitido a un atacante forzar la liquidez de los pools a aceptar intercambios pocos favorables², drenando sistemáticamente el valor de los tokens LP.

Originalmente, clasificamos esta vulnerabilidad como severamente crítica y de alta dificultad, y notificamos al cliente, quien arregló el problema en su código. Sin embargo, nuestra clasificación inicial se volvió complicada cuando nos percatamos que este error aritmético ocurre en múltiples instancias de la biblioteca PRBMath y, por lo tanto, puede potencialmente influenciar más sistemas, incluyendo los que están en vivo.

Esto presentó un dilema: incluso en el mundo de la seguridad “clásica” de la computación, los bugs de la biblioteca son notoriamente peligrosos y es muy difícil estimar la severidad y dificultad entre los proyectos. Esta dificultad se complica en Ethereum, el cual no tiene apoyo nativo para bibliotecas actualizables o mecanismos para distribuir hotfixes, y dónde, por el gas, las personas prefieren sólo copiar funciones específicas desde PRBMath y arreglarlas, en vez de importar toda la librería.

Luego de consultar con los investigadores líderes en seguridad samzsun y Mudit Gupta, realizamos una búsqueda exhaustiva a través de los repositorios públicos (ambos en y fuera de la cadena) y notificamos vulnerabilidades potenciales a los proyectos, en privado. También contactamos a Paul Razvan Berg (el autor de PRBMath) quién, inmediatamente, se unió a una llamada con nosotros y confirmó lo que encontramos.

Como resultado de nuestras investigaciones, creemos que en este punto en el tiempo, muy pocos contratos inteligentes usaron la porción de la aritmética firmada de PRBMath en una forma problemática. Por lo tanto, y dada la naturaleza inmutable de los contratos inteligentes, parece ser lo mejor exponer esto al público.

Mitigación

Para resolver el problema rápidamente, Paul sacó una reparación temporal (versión 4.1), que cambia la definición del mulDivSigned para que redondee a cero:

function mulDiv(uint256 x, uint256 y, uint256 denominator) pure
returns (uint256 result)
/// @notice Calcula x*y÷denominator con una precisión de 512-bit .
/// Notas:
/// - El resultado redondea a cero.
Enter fullscreen mode Exit fullscreen mode

En otros términos, este problema se le dará una solución a largo plazo, como parte de un plan actual para proveer soporte extensivo para múltiples modos de redondeo en PRBMath, ve la discusión aquí para saber más.

Conclusión

Las Bibliotecas Matemáticas son los bloques de construcción básicos para el ecosistema DeFi. Sin embargo, son sorprendentemente difíciles de hacer bien (especialmente cuando uno intenta optimizar agresivamente el consumo del gas), y auditarlos puede ser complicado y difícil.

El bug de arriba demuestra que, incluso con las pruebas comprensivas de la unidad, hay una gran ventaja metodológica en el proceso de escribir especificaciones formales para un sistema (si sólo se asegura que nada fue ignorado o pasado de largo). También sirve como un buen ejemplo para la expresividad del lenguaje CVL, una especificación elemental CVL (una “especificación equivalente”)

Image description

Fue capaz de detectar un bug viejo de 2 años en el código de Solidity, de una biblioteca matemática la cual envuelve segmentos extensivos Yul, numerosos trucos de hackeo de bit e incluso una teoría de número bit arrojado ahí, todo esto sin la necesidad de incluso entender los detalles de la implementación

¹ Mira, por ejemplo, el papel de la encuesta “SoK: Intercambios Descentralizados (DEX) con Protocolos Hechos del Mercado Automatizado AMM” para una revisión rápida de los DEX, AMM y la terminología DeFi relacionada.
² También conocida como AMM o Invariante CFMM

Este artículo es una traducción de Netanel, hecha por Gabriella Martínez. Puedes encontrar el artículo original aquí
Sería genial escucharte en nuestro Discord, puedes contarnos tus ideas, comentarios, sugerencias y dejarnos saber lo que necesitas.
Si prefieres puedes escribirnos a @web3dev_es en Twitter.

Discussion (0)