Resumen Técnico: Análisis Quiral de Contratos Inteligentes

1. Planteamiento del Problema

Las vulnerabilidades en los contratos inteligentes frecuentemente no derivan de sentencias inseguras aisladas, sino de inconsistencias relacionales entre rutas de negocio que están semánticamente emparejadas pero son sintácticamente distintas. Los ejemplos comunes incluyen discrepancias entre:

• Puntos de entrada únicos vs. por lotes (batch).
• Flujos directos vs. basados en adaptadores.
• Rutas de cotización (previsualización) vs. ejecución.
• Operaciones inversas (ej. compra vs. venta, acuñación vs. quema).

Los analizadores estáticos existentes sobresalen en la detección de patrones sintácticos locales, dependencias de tipo taint y vulnerabilidades de función única (ej. reentrada, llamadas no verificadas). Sin embargo, carecen de un "oráculo" para errores relacionales: no pueden determinar si dos rutas correspondientes preservan los mismos guardas, transiciones de estado, flujos de valor o comportamientos de fallo. Estos errores a menudo requieren comparar la lógica de un envoltorio (wrapper) contra una función central, o un despachador por lotes contra una ruta de operación única, para poder ser detectados.

2. Metodología: Análisis Quiral

El artículo introduce el análisis quiral, un modelo relacional que trata las rutas de negocio semánticamente emparejadas como especificaciones implícitas entre sí. El término "quiral" captura operaciones que son de tipo espejo, alternativas o relacionadas con el ciclo de vida (ej. único/lote, envoltorio/núcleo) sin requerir identidad sintáctica.

2.1 El Modelo de Vulnerabilidad Quiral

Los autores formalizan una relación quiral ($R_\chi$) como un análogo estático de una relación metamórfica. Consiste en dos rutas ($p, q$), un tipo de relación ($\tau$) y un conjunto de obligaciones inducidas por la relación. Estas obligaciones son aproximaciones de los comportaciones esperadas a través de siete dimensiones semánticas:

1. Guarda (Guard): Modificadores, precondiciones y comprobaciones de elegibilidad.
2. Actor: Identidades de llamadores, firmantes, pagadores y receptores de reembolsos.
3. Estado (State): Conjuntos de lectura/escritura, banderas, contadores y deltas de estado.
4. Valor (Value): Unidades, comisiones, recompensas, transferencias y manejo de reembolsos.
5. Orden (Order): Secuencias de chequeo-efecto-interacción y tiempos de liquidación.
6. Fallo (Failure): Comportamiento de reversión (revert), semántica de éxito parcial y emisión de eventos.
7. Externo (External): Uso de oráculos, callbacks y dependencias entre contratos.

Una vulnerabilidad quiral se define como una violación de tal obligación que resulta en un impacto de seguridad o de protocolo factible (ej. pérdida de fondos, cambio de estado no autorizado o errores de contabilidad).

2.2 El Pipeline ChiralDetector

Los autores implementan este modelo en ChiralDetector, un pipeline de cuatro etapas diseñado para equilibrar el recall con la precisión mientras se gestionan los costos de los Modelos de Lenguaje de Gran Escala (LLM):

1. Extracción de Rutas y Resumen:

   • Construye un grafo de llamadas a nivel de proyecto desde el código fuente de Solidity.
   • Extrae "rutas de negocio" (funciones únicas, cadenas de entrada a hoja y segmentos de bifurcación).
   • Genera un resumen de hechos semánticos ($\Phi(p)$) para cada ruta, capturando lecturas/escrituras de almacenamiento, transferencias de valor, modificadores y llamadas externas. Esta abstracción es intencionalmente pérdida de información pero orientada a la relación.

2. Reducción de Pares Candidatos:

   • Evita comparaciones exhaustivas $O(n^2)$ mediante el uso de un clasificador estático.
   • Califica pares de rutas basándose en huellas de almacenamiento compartidas, llamadas externas superpuestas, pistas de nomenclatura (ej. "claim" vs. "batchClaim") y similitudes de actor/flujo de valor.
   • Prioriza pares que probablemente formen una relación quiral sin eliminar señales de alto recall que sean inciertas.

3. Filtrado Semántico y Detección (basado en LLM):

   • Filtro Semántico: Determina si un par forma plausiblemente una relación quiral y asigna un tipo de relación (ej. inversa, envoltorio/núcleo). Se le instruye para aceptar pares con diferentes longitudes de ruta u direcciones económicas opuestas.
   • Detector Consciente de la Relación: Dada una relación confirmada, el LLM identifica obligaciones específicas violadas, proporciona evidencia de la fuente y formula una tesis de impacto. Los prompts están estructurados como "contratos" para forzar un razonamiento explícito en lugar de conclusiones vagas.

4. Validación Estricta y Deduplicación:

   • Un validador estricto intenta refutar los hallazgos verificando si la relación está justificada, si existe evidencia y si rutas de código alternas invalidan el impacto.
   • La deduplicación de causa raíz fusiona múltiples reportes que comparten el mismo defecto subyacente y la solución probable, distinguiendo entre el ruido a nivel de par y los problemas de raíz.

3. Contribuciones Clave

• Modelo de Análisis Quiral: Un marco de vulnerabilidad relacional que trata las rutas de negocio correspondientes como especificaciones implícitas, yendo más allá del análisis de función única.
• Formalización: Definición de relaciones quirales como análogos metamórficos estáticos y la derivación de siete dimensiones de obligación específicas.
• Implementación de ChiralDetector: Un prototipo de pipeline que integra análisis estático, clasificación estática de pares, detección semántica basada en LLM, validación de falsificación estricta y deduplicación de causa raíz.
• Evidencia Empírica: Una evaluación preliminar en el protocolo Phi que demuestra la detección de inconsistencias de lógica de negocio que son difíciles de expresar como reglas de función única.

4. Resultados de la Evaluación

Los autores evaluaron ChiralDetector en el protocolo Phi, un proyecto de Solidity que contiene diversas formas de relación (claim/batch, adapter/factory, quote/execution).

• Métricas de Embudo:

  • Comenzó con 3,217 pares candidatos clasificados estáticamente.
  • Se redujo a 1,643 pares para detección semántica.
  • Produjo 201 hallazgos limpios/candidatos sospechosos.
  • Se colapsó a 101 grupos de deduplicación local.
  • 44 grupos sobrevivieron a la validación estricta.
  • La deduplicación manual final de causa raíz arrojó 13 problemas únicos efectivos.

• Hallazgos Representativos:

  • M10: Reutilización de pruebas Merkle de artes cruzadas (Violación de flujo/guarda similar).
  • M13: Desajuste de unidad de comisión (puntos básicos vs. wei) (Violación de valor/unidad).
  • M12: Ayudantes de seguimiento público que corrompen el estado del curador (Violación de estado/acceso).
  • M05/M02/M04: Brechas de propagación de reembolsos y asimetrías de guarda entre rutas únicas y por lotes (Violaciones de flujo de valor de envoltorio/núcleo y de único/lote).

• Análisis de Costos:

  • La ejecución completa costó aproximadamente 212.70 CNY (excluyendo tiempo humano).
  • El costo dominante fue la inferencia de LLM (filtrado semántico, detección y validación), no el análisis estático.
  • El validador estricto redujo significativamente el ruido, rechazando 57 de los 101 grupos de deduplicación local.

5. Significado y Reivindicaciones

El artículo afirma que el análisis quiral expone una clase de errores —inconsistencias relacionales— que son naturalmente difíciles de expresar como reglas de función única, pero que son críticas para la seguridad del protocolo.

• Perspectiva: Muchos errores de lógica de negocio existen porque dos rutas relacionadas discrepan en cómo manejan un objeto de negocio compartido (ej. un receptor de reembolso o un cálculo de comisión), en lugar de porque una función sea localmente insegura.
• Uso Estructurado de LLM: El artículo argumenta que usar LLMs dentro de un pipeline estructurado (reducción estática $\to$ filtrado semántico $\to$ validación estricta) es más efectivo y rentable que la "auditoría de agentes directa" (lectura no restringida de código). El pipeline externaliza las decisiones intermedias (pares, relaciones, obligaciones), haciendo que el análisis sea inspeccionable y depurable.
• Modestia: Los autores declaran explícitamente que la evaluación actual es un estudio de caso preliminar sobre un solo protocolo. No pretenden haber establecido métricas generales de recall o precisión. Reconocen limitaciones, incluyendo la aproximación de la semántica de Solidity en la extracción de rutas, el potencial de alucinaciones de los LLM y la falta de generación automática de testigos (witnesses) o transacciones de prueba de concepto ejecutables.

El trabajo se posiciona como un paso hacia la creación de un razonamiento de lógica de negocio explícito y repetible en la auditoría de contratos inteligentes, ofreciendo un vocabulario para describir por qué ciertas inconsistencias son importantes.