⛓️ Blockchain Learning Path
GitHub

Clase 20 · Auditoría reproducible y remediación

Clase independiente 20 de 66 · Nivel: Avanzado · Fuente base: Trail of Bits Building Secure Contracts y ConsenSys Smart Contract Best Practices

⬅️ Clase anterior · 📚 Índice de las 66 clases · 🗂️ Mapa del tema · ➡️ Clase siguiente

Punto de partida

Pregunta guía: ¿Cómo se demuestra que un hallazgo fue corregido sin introducir otro?

Caso que abre la clase: Un parche bloquea el exploit conocido pero deja otra ruta equivalente.

Un exploit local obliga a reproducir antes de opinar. El parche se somete a regresión y a una ruta alternativa para separar corrección aparente de remediación completa.

Gráfico pedagógico

Recorre el gráfico en voz alta: identifica supuestos, transformaciones y el punto exacto donde aparece evidencia.

flowchart TD
  C["Caso observado"] --> O{"¿Qué sabemos?"}
  O --> A["alcance y commit auditado"]
  O --> B["análisis estático, fuzzing e invariantes"]
  A --> P["Probar: regresión, retest y riesgo residual"]
  B --> P
  P --> L["Conclusión con límites"]

Fundamentos que sostienen la respuesta

  1. alcance y commit auditado. En esta clase delimita qué objeto o relación estamos observando antes de sacar conclusiones. Localízalo explícitamente en «Un parche bloquea el exploit conocido pero deja otra ruta equivalente.» y anota qué dato faltaría para refutar tu lectura.
  2. análisis estático, fuzzing e invariantes. En esta clase explica el mecanismo que conecta la situación inicial con el cambio observable. Localízalo explícitamente en «Un parche bloquea el exploit conocido pero deja otra ruta equivalente.» y anota qué dato faltaría para refutar tu lectura.
  3. regresión, retest y riesgo residual. En esta clase permite contrastar el resultado y formular el límite de la evidencia. Localízalo explícitamente en «Un parche bloquea el exploit conocido pero deja otra ruta equivalente.» y anota qué dato faltaría para refutar tu lectura.

Qué detecta cada técnica (y qué no)

Ninguna herramienta cubre todo el espectro; una auditoría seria las apila porque sus puntos ciegos son complementarios:

Clase de bug Análisis estático (Slither) Fuzzing (Foundry/Echidna) Invariantes Revisión manual
Reentrancia por patrón de código ✅ detecta el patrón ⚠️ solo si la prueba lo ejercita ✅ si el invariante de saldos está definido ✅
Control de acceso faltante ✅ parcial ✅ con llamadas desde cuentas aleatorias ✅ ✅
Redondeo y precisión ❌ ✅ excelente con entradas extremas ✅ ⚠️ fácil de pasar por alto
Lógica económica multi-contrato ❌ ⚠️ requiere entorno completo ✅ la técnica más fuerte ✅
Error de diseño del protocolo ❌ ❌ ❌ ✅ única técnica que lo ve

La consecuencia práctica: un slither . limpio y un fuzzing en verde acotan clases enteras de errores, pero el caso Euler demuestra que el fallo puede vivir en la interacción entre funciones individualmente correctas, territorio exclusivo de los invariantes bien elegidos y de la revisión humana.

Dónde encaja la verificación formal

La verificación formal formula una propiedad y comprueba, mediante razonamiento simbólico o una prueba matemática, que se cumple para los estados cubiertos por un modelo. El SMTChecker del compilador de Solidity puede detectar aserciones violables y condiciones aritméticas sin enumerar manualmente cada entrada. Herramientas especializadas permiten expresar reglas de protocolo más ricas.

La garantía siempre tiene borde: prueba la propiedad escrita, sobre el código y los supuestos modelados, con las limitaciones declaradas por la herramienta. No demuestra que la especificación represente la intención económica, que un oráculo sea honesto ni que el despliegue use el bytecode revisado. La evidencia profesional incluye propiedad, versión de herramienta, resultado, supuestos, funciones fuera de alcance y una prueba o revisión complementaria.

Alcance, reproducción y cierre de hallazgos

Una auditoría empieza por fijar repositorio, commit, contratos, dependencias, compilador y supuestos excluidos. Sin ese corte, un informe correcto puede aplicarse a código distinto. Cada hallazgo contiene condición, recorrido explotable, impacto, severidad y prueba mínima. Herramientas estáticas amplían cobertura, pero no sustituyen revisar lógica económica, privilegios y composición.

Remediar exige algo más que cambiar la línea señalada: se reproduce el exploit, se aplica el parche, se ejecuta una regresión y se busca una ruta equivalente. El cierre registra qué versión fue reexaminada y qué riesgo residual permanece. Un test verde demuestra una propiedad codificada; no demuestra que el equipo haya formulado todas las propiedades importantes.

Trabajo práctico

Método propio: laboratorio exploit-parche-retest.

Actividad: Explotar en local, corregir y ejecutar una prueba de regresión.

Trabaja en entorno local, regtest, signet o testnet según corresponda. Conserva entradas, comandos, salidas y bloque o instante de corte. Una captura aislada no demuestra reproducibilidad.

Errores que esta clase corrige

Vuelve al caso inicial, elige el error más peligroso y describe una comprobación concreta que lo detectaría.

Demostración de aprendizaje

Entregable: Informe versionado con evidencia, corrección y resultado del retest.

Comprobación formativa: ¿Qué evidencia permite cerrar un hallazgo y qué riesgo puede permanecer?

Para aprobar debes conectar el hecho observado con el concepto correcto, descartar al menos una interpretación alternativa y redactar una conclusión cuyo alcance no exceda la prueba.

Límite ético y legal de esta clase

El alcance de auditoría define repositorio, commit, entorno, técnicas permitidas y canal de escalamiento. Encontrar una debilidad no amplía por sí solo esa autorización.

Aplica la guía transversal ¿Y si cruzas la línea? antes de proponer una intervención.

Fuentes para comprobar y ampliar

Consulta además la bibliografía razonada, que declara procedencia y uso.

Cierre de la clase

Responde otra vez la pregunta guía sin mirar notas. Si tu respuesta no menciona evidencia, supuesto y límite, todavía describe el tema pero no lo domina. Continúa solo cuando otra persona pueda reproducir tu entregable.