Capítulo 4: Desarrollo¶
MIESC: Marco Integrado de Seguridad para Contratos Ethereum¶
4.1 Introducción¶
El presente capítulo documenta el proceso de desarrollo e implementación de MIESC (Marco Integrado de Seguridad para Contratos Ethereum), un framework de código abierto diseñado para abordar las deficiencias identificadas en el ecosistema de herramientas de auditoría de contratos inteligentes. La exposición sigue una estructura que refleja el proceso real de investigación: desde la identificación de problemas concretos hasta las decisiones de diseño adoptadas para resolverlos, incluyendo los callejones sin salida encontrados y las lecciones aprendidas durante el desarrollo.
4.1.1 Génesis del Proyecto¶
El origen de MIESC se encuentra en una experiencia práctica de auditoría realizada en 2023, donde el autor enfrentó la tarea de evaluar la seguridad de un protocolo DeFi con TVL (Total Value Locked) superior a los 50 millones de dólares. Durante ese proceso, se hicieron evidentes tres problemas que la literatura académica había señalado pero que la industria no había resuelto de manera satisfactoria:
Primer problema: La fragmentación de herramientas. Para realizar una auditoría comprehensiva, fue necesario ejecutar Slither, Mythril, Echidna y solicitar análisis manuales con GPT-4. Cada herramienta requirió instalación independiente, configuración específica, y produjo resultados en formatos incompatibles entre sí. El tiempo invertido en orquestar las herramientas superó al tiempo de análisis efectivo.
Segundo problema: La dependencia de servicios comerciales. El uso de GPT-4 para análisis semántico implicaba enviar código fuente confidencial a servidores externos. En el contexto de una auditoría pre-lanzamiento, donde el código representa propiedad intelectual valiosa y potencialmente contiene vulnerabilidades explotables, esta transmisión resultaba inaceptable desde la perspectiva de gestión de riesgos.
Tercer problema: La interpretación de resultados. Las herramientas generaron colectivamente más de 200 hallazgos, muchos de ellos duplicados o falsos positivos. La tarea de consolidación, priorización y verificación consumió varios días de trabajo manual.
Estos problemas no son únicos de la experiencia del autor. Durieux et al. (2020), en su evaluación empírica de 47,587 contratos, documentaron que "ninguna herramienta individual detecta más del 75% de las vulnerabilidades conocidas, y la combinación manual de herramientas es impráctica a escala" (p. 535). Rameder et al. (2022) llegaron a conclusiones similares, señalando que "la heterogeneidad de interfaces y formatos de salida constituye una barrera significativa para la adopción industrial de herramientas académicas" (p. 12).
4.1.2 Objetivos del Desarrollo¶
Los objetivos técnicos de MIESC se formularon como respuesta directa a los problemas identificados, siguiendo el enfoque de diseño dirigido por problemas (problem-driven design) propuesto por Shaw (2012):
-
Integración heterogénea: Desarrollar una capa de abstracción que permita invocar múltiples herramientas de seguridad a través de una interfaz unificada, ocultando las diferencias de instalación, configuración y formato de salida.
-
Defensa en profundidad: Organizar las herramientas en capas complementarias basadas en sus técnicas de análisis, de modo que las fortalezas de unas compensen las debilidades de otras.
-
Normalización de resultados: Implementar un esquema de mapeo que traduzca los hallazgos de cada herramienta a taxonomías estándar (SWC, CWE, OWASP), habilitando la deduplicación y priorización automática.
-
Soberanía de datos: Garantizar que todo el procesamiento, incluyendo el análisis con inteligencia artificial, se ejecute localmente sin transmisión de código fuente a servicios externos.
-
Costo cero operativo: Utilizar exclusivamente herramientas de código abierto y modelos de lenguaje con pesos abiertos, eliminando barreras de costo que limitan el acceso a auditorías de calidad.
4.1.3 Métricas Cuantitativas del Proyecto¶
La Tabla 4.1 presenta las métricas del proyecto en su versión 4.0.0, medidas mediante herramientas estándar de análisis de código.
Tabla 4.1. Métricas cuantitativas del proyecto MIESC v4.0.0
| Métrica | Valor | Método de Medición |
|---|---|---|
| Líneas de código Python (LOC) | 43,221 | cloc --include-lang=Python |
| Líneas de código Solidity | 1,927 | cloc --include-lang=Solidity |
| Archivos Python | 114 | find . -name "*.py" | wc -l |
| Archivos Solidity | 13 | find . -name "*.sol" | wc -l |
| Complejidad ciclomática promedio | 4.2 | radon cc --average |
| Índice de mantenibilidad | 72.3 | radon mi --show |
| Cobertura de tests | 78% | pytest --cov |
| Herramientas integradas | 25 | Conteo manual |
| Capas de análisis | 7 | Arquitectura documentada |
El índice de mantenibilidad de 72.3 supera el umbral de 65 propuesto por Oman y Hagemeister (1992) para código "altamente mantenible", lo cual valida las decisiones de diseño orientadas a la extensibilidad.
4.2 Arquitectura del Sistema¶
4.2.1 El Principio de Defensa en Profundidad: Fundamentos y Aplicación¶
La arquitectura de MIESC se fundamenta en el principio de defensa en profundidad (Defense-in-Depth, DiD), un concepto originado en doctrina militar que fue adaptado a la seguridad de sistemas de información durante la década de 1990. El Department of Defense (1996) formalizó este principio como "la aplicación de múltiples medidas de protección en serie, de modo que un adversario deba superar o evitar cada medida sucesivamente para comprometer el sistema protegido" (p. 3-12).
La aplicación de este principio al análisis de contratos inteligentes es una contribución original de este trabajo. La justificación teórica se fundamenta en la observación empírica de que diferentes técnicas de análisis tienen fortalezas y debilidades complementarias:
Análisis estático: Examina el código sin ejecutarlo, detectando patrones conocidos de vulnerabilidad con alta velocidad pero sin capacidad de razonar sobre comportamiento en tiempo de ejecución. Feist et al. (2019) reportan que Slither alcanza 82% de precisión pero solo 75% de recall, indicando que aproximadamente una de cada cuatro vulnerabilidades escapa a su detección.
Ejecución simbólica: Explora caminos de ejecución mediante representación simbólica de variables, capaz de descubrir vulnerabilidades dependientes de valores específicos de entrada. Baldoni et al. (2018) documentan su efectividad pero también su principal limitación: la explosión combinatoria de caminos en código complejo.
Fuzzing: Genera entradas aleatorias o guiadas para descubrir comportamientos inesperados, particularmente efectivo para encontrar casos límite no contemplados por el desarrollador. Miller et al. (1990) establecieron esta técnica, que Grieco et al. (2020) adaptaron específicamente para contratos inteligentes con Echidna.
Verificación formal: Demuestra matemáticamente propiedades del código mediante sistemas de prueba automatizados. Clarke et al. (2018) describen los fundamentos teóricos, mientras que Lahav et al. (2022) documentan su aplicación práctica en Certora Prover.
Análisis con IA: Modelos de lenguaje capaces de detectar vulnerabilidades de lógica de negocio que requieren comprensión semántica del código. Sun et al. (2024) demuestran que GPTScan detecta el 90.2% de vulnerabilidades de lógica que escapan a herramientas tradicionales.
Schneier (2000) articula la filosofía subyacente:
"La defensa en profundidad reconoce que ningún control de seguridad individual es perfecto. Al implementar múltiples capas, se reduce la probabilidad de que un atacante pueda evadir todos los controles" (p. 284).
4.2.2 Proceso de Selección: De la Teoría a las Siete Capas¶
La decisión de implementar exactamente siete capas no fue arbitraria sino el resultado de un proceso iterativo de evaluación. Inicialmente se consideraron tres configuraciones alternativas:
Configuración de 3 capas (descartada): Agrupaba las técnicas en análisis estático, análisis dinámico y verificación formal. Esta configuración, similar a la propuesta por Atzei et al. (2017), resultó demasiado gruesa: dentro de "análisis dinámico" coexistían fuzzing y ejecución simbólica, técnicas con filosofías fundamentalmente diferentes que se benefician de orquestación independiente.
Configuración de 5 capas (versión inicial): Separaba análisis estático, fuzzing, ejecución simbólica, verificación formal y análisis con IA. Esta configuración, implementada en MIESC v1.0 y v2.0, demostró ser funcional pero presentaba dos deficiencias: (1) no distinguía entre fuzzing de cobertura y mutation testing, y (2) agrupaba todas las técnicas de IA sin diferenciar property testing de análisis semántico.
Configuración de 7 capas (versión final): Resultado de refinar la configuración de 5 capas basándose en la experiencia operacional y los hallazgos de Rameder et al. (2022), quienes argumentan que "la granularidad de categorización afecta directamente la capacidad de orquestación y deduplicación" (p. 18).
La Tabla 4.2 presenta el análisis de complementariedad que fundamentó la selección final.
Tabla 4.2. Análisis de complementariedad de técnicas por tipo de vulnerabilidad
| Vulnerabilidad (SWC) | Estático | Simbólico | Fuzzing | Formal | IA |
|---|---|---|---|---|---|
| SWC-107 Reentrancy | Alta | Alta | Media | Muy Alta | Media |
| SWC-101 Integer Issues | Alta | Alta | Media | Muy Alta | Baja |
| SWC-104 Unchecked Return | Alta | Baja | Baja | Media | Media |
| SWC-115 tx.origin Auth | Alta | Media | Baja | Alta | Alta |
| Lógica de negocio | Baja | Media | Media | Baja | Alta |
| Oracle Manipulation | Baja | Baja | Alta | Media | Alta |
Nota: Efectividad estimada basada en Durieux et al. (2020) y experiencia operacional
4.2.3 Modelo de Capas Definitivo¶
Figura 7. Arquitectura de defensa en profundidad de MIESC
La numeración de capas refleja el orden típico de ejecución durante una auditoría: las técnicas más rápidas y con menor costo computacional (análisis estático) se ejecutan primero, permitiendo identificar problemas evidentes antes de invertir recursos en técnicas más costosas (ejecución simbólica, verificación formal).
4.2.4 Justificación de la Selección de Herramientas¶
La selección de las 25 herramientas que componen MIESC siguió un proceso de evaluación estructurado basado en cinco criterios:
-
Efectividad demostrada: Preferencia por herramientas con evaluación empírica publicada en literatura académica.
-
Licencia compatible: Exclusión de herramientas con licencias que impidieran redistribución o uso comercial del framework integrado.
-
Mantenimiento activo: Preferencia por proyectos con commits recientes y comunidad activa.
-
Complementariedad: Evitar redundancia entre herramientas de la misma capa.
-
Instalabilidad: Capacidad de instalación automatizada sin intervención manual compleja.
Capa 1 - Análisis Estático: Slither fue seleccionada como herramienta principal por su equilibrio entre precisión (82%) y velocidad (1.2s promedio), según los benchmarks de Durieux et al. (2020). Solhint complementa con verificación de estilo y mejores prácticas. Securify2 aporta análisis de patrones de seguridad específicos de Ethereum. Semgrep permite definir reglas personalizadas para patrones específicos de cada organización.
Capa 2 - Fuzzing: Echidna, desarrollada por Trail of Bits, fue seleccionada por su capacidad de property-based testing específico para contratos. Foundry Fuzz aporta integración con el ecosistema Foundry, ampliamente adoptado en la industria. Medusa proporciona fuzzing basado en cobertura con soporte para invariantes complejas. Vertigo implementa mutation testing, una técnica complementaria que evalúa la calidad de las pruebas existentes.
Capa 3 - Ejecución Simbólica: Mythril, también de Trail of Bits, fue seleccionada por su madurez y extensa documentación. Manticore aporta capacidades de análisis más profundas a costa de mayor tiempo de ejecución. Oyente, aunque menos mantenido, se incluyó por su relevancia histórica y detección de patrones específicos no cubiertos por las otras herramientas.
Capa 4 - Invariant Testing: Scribble permite anotar contratos con especificaciones que se verifican durante ejecución. Halmos implementa bounded model checking, verificando invariantes hasta cierta profundidad de exploración.
Capa 5 - Verificación Formal: SMTChecker está integrado en el compilador Solidity, proporcionando verificación formal sin herramientas adicionales. Certora Prover, aunque comercial, se incluyó opcionalmente por su capacidad de verificar propiedades complejas que otras herramientas no pueden abordar.
Capa 6 - Property Testing: PropertyGPT utiliza LLM para generar propiedades de prueba automáticamente. Aderyn implementa análisis de seguridad con reglas actualizadas frecuentemente. Wake proporciona un framework de testing con capacidades de property-based testing.
Capa 7 - Análisis con IA: GPTScan implementa la metodología de Sun et al. (2024). SmartLLM combina LLM con RAG (Retrieval-Augmented Generation) para análisis contextualizado. LLMSmartAudit proporciona auditoría automatizada completa. ThreatModel genera modelos de amenazas STRIDE. GasGauge analiza optimización de gas. UpgradeGuard verifica seguridad de patrones de upgrade. BestPractices evalúa adherencia a mejores prácticas documentadas.
4.3 Diseño de Software¶
4.3.1 El Problema de la Heterogeneidad¶
Cada herramienta de seguridad integrada en MIESC presenta características únicas que dificultan su orquestación unificada:
Diversidad de interfaces de invocación: Slither se invoca como módulo Python, Mythril como comando CLI, Echidna requiere archivos de configuración YAML, Certora utiliza archivos .conf con sintaxis propia.
Heterogeneidad de formatos de salida: Slither produce JSON estructurado, Mythril genera texto formateado o JSON según parámetros, Echidna emite logs de prueba, Manticore crea directorios de artefactos.
Inconsistencia en clasificación de severidad: Slither utiliza "High/Medium/Low/Informational", Mythril emplea "Critical/High/Medium/Low", algunas herramientas no clasifican severidad.
Variabilidad en información de ubicación: Algunas herramientas reportan archivo y línea, otras añaden columna, otras indican función y contrato, algunas solo mencionan el nombre del detector.
Esta heterogeneidad constituye la barrera principal para la adopción industrial de herramientas académicas, como documentan Rameder et al. (2022).
4.3.2 Solución: Patrón Adapter con Principios SOLID¶
La solución adoptada combina el patrón Adapter, documentado por Gamma et al. (1994), con los principios SOLID propuestos por Martin (2017). Esta combinación no es casual: el patrón Adapter proporciona la estructura para unificar interfaces, mientras que SOLID garantiza que el diseño sea extensible y mantenible.
Principio de Responsabilidad Única (SRP): Cada adaptador tiene una única responsabilidad: traducir la interfaz de una herramienta específica a la interfaz común de MIESC. El adaptador de Slither no conoce la existencia de Mythril, y viceversa.
Principio Abierto/Cerrado (OCP): El framework está abierto a extensión (agregar nuevos adaptadores) pero cerrado a modificación (el núcleo no cambia al agregar herramientas). Para integrar una herramienta nueva, solo se requiere implementar un adaptador que cumpla la interfaz ToolAdapter.
Principio de Sustitución de Liskov (LSP): Todos los adaptadores son intercambiables a través de la interfaz ToolAdapter. El orquestador puede invocar cualquier adaptador sin conocer su implementación concreta.
Principio de Segregación de Interfaces (ISP): La interfaz ToolAdapter define únicamente los métodos esenciales que todo adaptador debe implementar, sin imponer métodos que solo algunas herramientas necesitarían.
Principio de Inversión de Dependencias (DIP): El núcleo de MIESC depende de la abstracción ToolAdapter, no de implementaciones concretas como SlitherAdapter o MythrilAdapter.
Figura 8. Diagrama de clases del patrón Adapter en MIESC
4.3.3 Implementación de la Interfaz Base¶
La interfaz ToolAdapter se implementa utilizando el módulo abc (Abstract Base Classes) de Python, siguiendo las recomendaciones de van Rossum et al. (2001):
from abc import ABC, abstractmethod
from typing import Dict, Any, List
from dataclasses import dataclass
from enum import Enum
class ToolAdapter(ABC):
"""
Interfaz abstracta para adaptadores de herramientas de seguridad.
Esta clase define el contrato que todo adaptador debe cumplir para
integrarse con MIESC. El diseño sigue el patrón Adapter de Gamma
et al. (1994) y los principios SOLID de Martin (2017).
La abstracción permite que el orquestador de MIESC trabaje con
cualquier herramienta sin conocer sus detalles de implementación,
cumpliendo el Principio de Inversión de Dependencias.
"""
@abstractmethod
def get_metadata(self) -> 'ToolMetadata':
"""
Retorna metadatos estandarizados de la herramienta.
Los metadatos incluyen información sobre licencia, costo,
y requisitos de instalación, cumpliendo con los estándares
DPGA (2023) de transparencia.
"""
pass
@abstractmethod
def is_available(self) -> 'ToolStatus':
"""
Verifica la disponibilidad de la herramienta en el sistema.
Este método permite degradación elegante: si una herramienta
no está instalada, MIESC continúa con las demás en lugar de
fallar completamente.
"""
pass
@abstractmethod
def analyze(self, contract_path: str, **kwargs) -> Dict[str, Any]:
"""
Ejecuta el análisis de seguridad sobre un contrato.
Args:
contract_path: Ruta absoluta al archivo .sol
**kwargs: Parámetros específicos de la herramienta
(timeout, max_depth, etc.)
Returns:
Diccionario con estructura normalizada MIESC conteniendo
status, findings, y metadata del análisis.
"""
pass
@abstractmethod
def normalize_findings(self, raw_output: Any) -> List[Dict[str, Any]]:
"""
Normaliza hallazgos al formato MIESC estándar.
Este método implementa el mapeo de clasificaciones nativas
de cada herramienta a taxonomías estándar (SWC, CWE, OWASP).
La normalización es esencial para la deduplicación posterior.
"""
pass
4.3.4 Estructura de Metadatos¶
Los metadatos de herramientas siguen el principio de auto-descripción propuesto por Berners-Lee et al. (2001), permitiendo que el sistema documente automáticamente sus capacidades:
@dataclass
class ToolMetadata:
"""
Metadatos estandarizados de herramientas.
Cada campo fue seleccionado para cumplir requisitos específicos:
- license: Cumplimiento DPGA de transparencia de licencias
- cost: Cumplimiento DPGA de accesibilidad sin barreras de costo
- is_optional: Cumplimiento DPGA de no crear dependencias obligatorias
"""
name: str # Identificador único
version: str # Versión semántica (Preston-Werner, 2013)
category: ToolCategory # Capa a la que pertenece
author: str # Autor o mantenedor principal
license: str # Identificador SPDX
homepage: str # URL del proyecto
repository: str # URL del repositorio de código
documentation: str # URL de documentación
installation_cmd: str # Comando de instalación
capabilities: List[ToolCapability] # Capacidades declaradas
cost: float = 0.0 # Costo por uso (0 = gratuito)
requires_api_key: bool = False # Requiere credenciales externas
is_optional: bool = True # Puede omitirse sin afectar funcionalidad core
4.4 Normalización de Hallazgos¶
4.4.1 El Problema de la Babel de Vulnerabilidades¶
Sin normalización, los hallazgos de diferentes herramientas son incomparables. Considérese el siguiente ejemplo de una misma vulnerabilidad de reentrancy detectada por tres herramientas:
Slither:
{
"check": "reentrancy-eth",
"impact": "High",
"confidence": "Medium",
"elements": [{"source_mapping": {"filename": "Bank.sol", "lines": [42]}}]
}
Mythril:
==== State change after external call ====
SWC ID: 107
Severity: High
Contract: Bank
Function name: withdraw
PC address: 1234
GPTScan:
{
"vulnerability": "Reentrancy vulnerability in withdraw function",
"severity": "CRITICAL",
"line": 42
}
Observaciones: - Slither llama a la vulnerabilidad "reentrancy-eth", Mythril usa "State change after external call", GPTScan dice "Reentrancy vulnerability" - Slither usa "High", GPTScan usa "CRITICAL" (mismo concepto, diferente nomenclatura) - Solo Mythril referencia el estándar SWC-107 - El formato estructural es completamente diferente
4.4.2 Solución: Mapeo a Taxonomías Estándar¶
MIESC implementa un esquema de normalización que mapea hallazgos a tres taxonomías complementarias:
SWC (Smart Contract Weakness Classification): Taxonomía específica para contratos inteligentes mantenida por la comunidad Ethereum (SCSVS, 2023). Contiene 37 categorías de debilidades con identificadores únicos (SWC-100 a SWC-136).
CWE (Common Weakness Enumeration): Taxonomía general de debilidades de software mantenida por MITRE (2024). Permite correlacionar vulnerabilidades de smart contracts con debilidades conocidas en software tradicional, facilitando la comunicación con equipos de seguridad no especializados en blockchain.
OWASP Smart Contract Top 10: Lista de las vulnerabilidades más críticas desarrollada por OWASP (2023), útil para priorización ejecutiva.
4.4.3 Formato de Hallazgo Normalizado¶
El formato de hallazgo normalizado se diseñó siguiendo el estándar SARIF (Static Analysis Results Interchange Format) de OASIS (2020), con extensiones específicas para contratos inteligentes:
{
"id": "MIESC-2024-001",
"type": "reentrancy",
"severity": "Critical",
"confidence": 0.95,
"location": {
"file": "VulnerableBank.sol",
"line": 42,
"column": 8,
"function": "withdraw",
"contract": "VulnerableBank",
"code_snippet": "(bool ok,) = msg.sender.call{value: amount}(\"\");"
},
"message": "Reentrancy vulnerability: external call before state update",
"description": "The contract makes an external call to transfer Ether before updating the sender's balance. An attacker can re-enter the withdraw function before the balance is set to zero, allowing them to drain the contract's funds.",
"recommendation": "Apply the Checks-Effects-Interactions pattern: update state before making external calls. Alternatively, use OpenZeppelin's ReentrancyGuard modifier.",
"classifications": {
"swc_id": "SWC-107",
"cwe_id": "CWE-841",
"owasp": "SC01:2023-Reentrancy"
},
"detected_by": ["slither", "mythril", "gptscan"],
"references": [
"https://swcregistry.io/docs/SWC-107",
"https://consensys.github.io/smart-contract-best-practices/attacks/reentrancy/"
],
"metadata": {
"first_detected": "2024-11-29T14:30:00Z",
"analysis_duration_ms": 1234,
"miesc_version": "4.0.0"
}
}
4.4.4 Tablas de Mapeo¶
El mapeo de clasificaciones nativas a estándares se implementa mediante tablas de correspondencia validadas manualmente contra la documentación de cada herramienta y el registro SWC. La Tabla 4.3 presenta un extracto.
Tabla 4.3. Extracto del mapeo de clasificaciones nativas a estándares
| Herramienta | Clasificación Nativa | SWC-ID | CWE-ID | OWASP SC |
|---|---|---|---|---|
| Slither | reentrancy-eth | SWC-107 | CWE-841 | SC01 |
| Slither | reentrancy-no-eth | SWC-107 | CWE-841 | SC01 |
| Slither | arbitrary-send-eth | SWC-105 | CWE-284 | SC02 |
| Slither | controlled-delegatecall | SWC-112 | CWE-829 | SC02 |
| Slither | suicidal | SWC-106 | CWE-284 | SC02 |
| Mythril | State change after external call | SWC-107 | CWE-841 | SC01 |
| Mythril | Integer overflow | SWC-101 | CWE-190 | SC03 |
| Mythril | Dependence on tx.origin | SWC-115 | CWE-477 | SC02 |
| Echidna | assertion failure | SWC-110 | CWE-617 | SC03 |
| GPTScan | Reentrancy vulnerability | SWC-107 | CWE-841 | SC01 |
4.5 Implementación de Capas: Narrativa del Proceso¶
4.5.1 Capa 1: Análisis Estático - El Punto de Entrada¶
El análisis estático constituye la primera línea de defensa por razones tanto técnicas como prácticas. Desde el punto de vista técnico, el análisis estático no requiere ejecución del contrato, lo que permite identificar problemas incluso en código que no compila. Desde el punto de vista práctico, su velocidad (típicamente menos de 5 segundos por contrato) permite iteración rápida durante el desarrollo.
La implementación del adaptador de Slither ilustra el proceso de traducción de interfaces:
class SlitherAdapter(ToolAdapter):
"""
Adaptador para Slither - Framework de análisis estático.
Slither fue seleccionada como herramienta principal de análisis
estático por su balance entre precisión y velocidad, documentado
en Durieux et al. (2020). Su arquitectura basada en SlithIR
(representación intermedia) permite análisis de flujo de datos
sofisticado manteniendo tiempos de ejecución razonables.
Consideraciones de implementación:
- Slither se invoca como comando CLI (no como biblioteca Python)
para garantizar aislamiento de dependencias
- La salida JSON se parsea y normaliza al formato MIESC
- Los detectores se mapean a taxonomías SWC/CWE mediante tabla
"""
# Mapeo validado manualmente contra documentación de Slither
# y registro SWC (verificado: 2024-11-01)
DETECTOR_MAPPING = {
"reentrancy-eth": {
"swc_id": "SWC-107",
"cwe_id": "CWE-841",
"owasp": "SC01:2023-Reentrancy",
"severity": "Critical",
"confidence_base": 0.90
},
"reentrancy-no-eth": {
"swc_id": "SWC-107",
"cwe_id": "CWE-841",
"owasp": "SC01:2023-Reentrancy",
"severity": "High",
"confidence_base": 0.85
},
"arbitrary-send-eth": {
"swc_id": "SWC-105",
"cwe_id": "CWE-284",
"owasp": "SC02:2023-Access-Control",
"severity": "High",
"confidence_base": 0.85
},
# ... mapeos para 40+ detectores
}
def analyze(self, contract_path: str, **kwargs) -> Dict[str, Any]:
"""
Ejecuta análisis estático con Slither.
El proceso sigue tres etapas:
1. Invocación de Slither con parámetros optimizados
2. Parseo de salida JSON
3. Normalización al formato MIESC
La exclusión de 'naming-convention' reduce falsos positivos
sin afectar la detección de vulnerabilidades de seguridad.
"""
timeout = kwargs.get("timeout", 60)
cmd = [
"slither",
contract_path,
"--json", "-", # Salida JSON a stdout
"--exclude", "naming-convention", # Reduce ruido
]
try:
result = subprocess.run(
cmd,
capture_output=True,
timeout=timeout,
text=True
)
raw_output = json.loads(result.stdout)
findings = self.normalize_findings(raw_output)
return {
"tool": "slither",
"version": self._get_version(),
"status": "success",
"findings": findings,
"metadata": {
"detectors_run": len(raw_output.get("detectors", [])),
"contracts_analyzed": len(raw_output.get("contracts", [])),
"execution_time_ms": result.returncode
}
}
except subprocess.TimeoutExpired:
return self._error_response("Timeout exceeded", timeout)
except json.JSONDecodeError as e:
return self._error_response(f"Invalid JSON output: {e}", None)
4.5.2 Capa 3: Ejecución Simbólica - Explorando lo Posible¶
La ejecución simbólica representa un salto cualitativo respecto al análisis estático. Mientras el análisis estático identifica patrones sintácticos, la ejecución simbólica explora el espacio de estados posibles del contrato, descubriendo vulnerabilidades que dependen de valores específicos de entrada.
El fundamento teórico se encuentra en el trabajo seminal de King (1976), quien demostró que representar variables como símbolos en lugar de valores concretos permite explorar múltiples caminos de ejecución simultáneamente. Baldoni et al. (2018) proporcionan una revisión comprehensiva de la evolución de esta técnica.
La implementación del adaptador de Mythril ilustra consideraciones específicas de ejecución simbólica:
class MythrilAdapter(ToolAdapter):
"""
Adaptador para Mythril - Herramienta de ejecución simbólica.
Mythril utiliza el solver SMT Z3 (de Moura & Bjørner, 2008) para
determinar si existen entradas que conduzcan a estados vulnerables.
Limitaciones conocidas que afectan la implementación:
1. Path explosion: El número de caminos crece exponencialmente con
la complejidad del contrato. Se mitiga con max_depth.
2. Operaciones criptográficas: Los hashes son tratados como cajas
negras, limitando análisis de código que depende de ellos.
3. Consumo de memoria: Contratos complejos pueden agotar RAM.
Se mitiga con execution_timeout.
"""
def analyze(self, contract_path: str, **kwargs) -> Dict[str, Any]:
"""
Ejecuta análisis simbólico con Mythril.
Parámetros críticos:
- execution_timeout: Limita tiempo de exploración para evitar
análisis infinitos en contratos complejos
- max_depth: Limita profundidad de exploración de caminos
- solver_timeout: Limita tiempo por query SMT individual
Los valores por defecto fueron calibrados empíricamente sobre
un corpus de 100 contratos representativos.
"""
timeout = kwargs.get("timeout", 120)
execution_timeout = kwargs.get("execution_timeout", 60)
max_depth = kwargs.get("max_depth", 22) # Default de Mythril
cmd = [
"myth", "analyze",
contract_path,
"--output", "json",
"--execution-timeout", str(execution_timeout),
"--max-depth", str(max_depth),
"--solver-timeout", "10000" # 10s por query SMT
]
# ... resto de implementación
4.5.3 Capa 7: Análisis con IA - Comprensión Semántica¶
La capa de inteligencia artificial representa la contribución más distintiva de MIESC. Mientras las capas anteriores detectan patrones técnicos, la IA puede comprender la semántica del código y detectar vulnerabilidades de lógica de negocio que no corresponden a patrones conocidos.
La decisión de implementar esta capa con modelos locales (Ollama) en lugar de APIs comerciales (OpenAI, Anthropic) se fundamenta en tres consideraciones:
-
Confidencialidad: El código de contratos pre-auditoría es propiedad intelectual valiosa que no debe transmitirse a terceros.
-
Costo: Las APIs comerciales generan costos significativos a escala (estimado $2,500/año para 100 auditorías mensuales).
-
Disponibilidad: La dependencia de APIs externas introduce puntos de falla fuera del control del auditor.
class GPTScanAdapter(ToolAdapter):
"""
Implementación de GPTScan con backend Ollama.
Basado en la metodología de Sun et al. (2024), quienes demostraron
que LLMs detectan el 90.2% de vulnerabilidades de lógica de negocio
que escapan a herramientas tradicionales.
Modificaciones respecto al paper original:
1. Backend Ollama en lugar de OpenAI API (soberanía de datos)
2. Prompts optimizados para modelos de menor parámetros
3. Caché de resultados para eficiencia en re-análisis
Modelos soportados (orden de preferencia):
- qwen2.5-coder:7b: Mejor rendimiento en código según benchmarks
- codellama:7b: Alternativa robusta con buen balance
- llama3.2:3b: Fallback para sistemas con recursos limitados
"""
SECURITY_PROMPT = """You are a smart contract security auditor
with expertise in Ethereum and Solidity. Analyze the following
contract for security vulnerabilities.
Focus specifically on:
1. Reentrancy vulnerabilities (SWC-107)
2. Integer overflow/underflow (SWC-101)
3. Access control issues (SWC-105, SWC-115)
4. Unchecked external calls (SWC-104)
5. Logic errors in business logic
6. Flash loan attack vectors
7. Oracle manipulation possibilities
For each vulnerability found, respond in JSON format:
{
"vulnerabilities": [
{
"title": "Brief description",
"severity": "CRITICAL|HIGH|MEDIUM|LOW",
"confidence": 0.0-1.0,
"line": line_number,
"description": "Detailed explanation",
"recommendation": "Specific fix"
}
]
}
CONTRACT CODE:
```solidity
%CONTRACT_CODE%
```
Respond ONLY with valid JSON."""
def _run_ollama_analysis(
self,
contract_code: str,
model: str = "llama3.2:3b"
) -> str:
"""
Ejecuta análisis mediante Ollama local.
La verificación de localhost garantiza que el código nunca
sale del sistema local, cumpliendo requisitos de soberanía.
"""
if not self._verify_local_only():
raise SecurityError(
"LLM backend must be localhost for data sovereignty"
)
prompt = self.SECURITY_PROMPT.replace("%CONTRACT_CODE%", contract_code)
result = subprocess.run(
["ollama", "run", model, prompt],
capture_output=True,
timeout=120,
text=True
)
return result.stdout
4.6 Orquestación y Deduplicación¶
4.6.1 El Pipeline de Análisis¶
La orquestación de las siete capas sigue el patrón Pipeline propuesto por Hohpe y Woolf (2003), adaptado para ejecución paralela intra-capa y secuencial inter-capa. Esta estrategia maximiza el throughput aprovechando que las herramientas dentro de una misma capa son independientes entre sí.
class MIESCAuditOrchestrator:
"""
Orquestador de auditoría multi-capa.
La estrategia de ejecución sigue la Ley de Amdahl (1967):
- Paralelización intra-capa: Herramientas independientes se ejecutan
simultáneamente, reduciendo el tiempo de capa a max(tiempos)
- Secuencialización inter-capa: Las capas se ejecutan en orden,
permitiendo early-exit si se detectan vulnerabilidades críticas
La deduplicación al final del pipeline reduce el volumen de
hallazgos típicamente en 60-70%, según observaciones empíricas.
"""
def run_full_audit(
self,
contract_path: str,
layers: List[int] = None,
parallel_workers: int = 4
) -> AuditReport:
"""
Ejecuta auditoría completa multi-capa.
El parámetro parallel_workers controla el nivel de paralelismo
intra-capa. El valor por defecto de 4 está calibrado para
sistemas con 8+ GB de RAM.
"""
layers = layers or list(range(1, 8))
all_findings = []
layer_results = {}
for layer_num in layers:
layer_tools = self.get_layer_tools(layer_num)
layer_findings = []
# Ejecución paralela de herramientas de la capa
with ThreadPoolExecutor(max_workers=parallel_workers) as executor:
futures = {
executor.submit(
tool.analyze, contract_path
): tool for tool in layer_tools if tool.is_available()
}
for future in as_completed(futures):
try:
result = future.result(timeout=300)
layer_findings.extend(result.get("findings", []))
except Exception as e:
tool = futures[future]
self.logger.warning(
f"Tool {tool.name} failed: {e}"
)
all_findings.extend(layer_findings)
layer_results[f"layer_{layer_num}"] = {
"tools_available": len([t for t in layer_tools if t.is_available()]),
"tools_total": len(layer_tools),
"findings_count": len(layer_findings)
}
# Deduplicación
unique_findings = self._deduplicate_findings(all_findings)
return AuditReport(
findings=unique_findings,
total_raw=len(all_findings),
total_unique=len(unique_findings),
deduplication_rate=1 - len(unique_findings)/max(len(all_findings), 1),
layer_results=layer_results
)
4.6.2 Algoritmo de Deduplicación¶
La deduplicación de hallazgos es crítica para la usabilidad del framework. Sin deduplicación, una vulnerabilidad detectada por cinco herramientas aparecería cinco veces en el reporte, dificultando la priorización y consumiendo tiempo del auditor.
El algoritmo implementado se inspira en técnicas de record linkage (Fellegi & Sunter, 1969), adaptadas al dominio específico de vulnerabilidades de smart contracts:
def _deduplicate_findings(self, findings: List[Dict]) -> List[Dict]:
"""
Deduplica hallazgos de múltiples herramientas.
Estrategia de deduplicación:
1. Generar clave única por (tipo, archivo, línea aproximada)
2. Agrupar hallazgos por clave
3. Consolidar: preservar máxima severidad y confianza
4. Registrar todas las herramientas que detectaron cada hallazgo
La tolerancia de ±2 líneas en la clave de deduplicación maneja
diferencias menores en cómo las herramientas reportan ubicaciones.
Por ejemplo, Slither puede reportar línea 42 mientras Mythril
reporta línea 43 para la misma vulnerabilidad.
"""
unique = {}
for finding in findings:
# Clave de deduplicación con tolerancia de línea
key = (
finding.get("type", "unknown"),
finding.get("location", {}).get("file", "unknown"),
finding.get("location", {}).get("line", 0) // 3
)
if key not in unique:
unique[key] = finding.copy()
unique[key]["detected_by"] = [finding.get("tool", "unknown")]
else:
existing = unique[key]
# Preservar mayor severidad
if self._severity_rank(finding.get("severity")) > \
self._severity_rank(existing.get("severity")):
new_finding = finding.copy()
new_finding["detected_by"] = existing["detected_by"]
unique[key] = new_finding
# Agregar herramienta a lista de detectores
tool = finding.get("tool", "unknown")
if tool not in unique[key]["detected_by"]:
unique[key]["detected_by"].append(tool)
# Preservar mayor confianza
if finding.get("confidence", 0) > existing.get("confidence", 0):
unique[key]["confidence"] = finding["confidence"]
return list(unique.values())
def _severity_rank(self, severity: str) -> int:
"""Convierte severidad textual a valor numérico para comparación."""
ranks = {
"critical": 4,
"high": 3,
"medium": 2,
"low": 1,
"informational": 0
}
return ranks.get(severity.lower() if severity else "", 0)
4.7 Soluciones a Desafíos Técnicos Encontrados¶
El desarrollo de MIESC enfrentó varios desafíos técnicos no documentados en la literatura. Esta sección describe los problemas encontrados y las soluciones implementadas, con el objetivo de facilitar el trabajo de futuros investigadores.
4.7.1 Incompatibilidad de Manticore con Python 3.11¶
Problema identificado: Manticore depende de la biblioteca wasm, la cual utiliza collections.Callable, un alias eliminado en Python 3.11 según PEP 585 (van Rossum et al., 2019).
Síntoma: Error de importación al intentar usar Manticore:
Análisis: El cambio en Python 3.11 movió clases de tipado de collections a collections.abc para clarificar que son abstract base classes. Código legacy que importa collections.Callable falla.
Solución implementada: Parche en tiempo de instalación que modifica el archivo afectado:
# Script de instalación: scripts/patch_wasm.py
import site
import os
site_packages = site.getsitepackages()[0]
wasm_types_path = os.path.join(site_packages, 'wasm', 'types.py')
if os.path.exists(wasm_types_path):
with open(wasm_types_path, 'r') as f:
content = f.read()
# Aplicar parche
patched = content.replace(
'isinstance(cur_field, collections.Callable)',
'isinstance(cur_field, collections.abc.Callable)'
)
with open(wasm_types_path, 'w') as f:
f.write(patched)
Fundamentación: El principio de encapsulación de Parnas (1972) sugiere aislar cambios en un único punto. El parche modifica solo el archivo afectado sin alterar el resto del sistema.
4.7.2 Containerización de Herramientas Legacy¶
Problema identificado: Oyente requiere versiones antiguas de dependencias (solc 0.4.x, z3 4.5.x) incompatibles con entornos modernos de desarrollo.
Síntoma: Conflictos de dependencias al intentar instalar Oyente junto con Slither y Mythril en el mismo entorno virtual.
Solución implementada: Ejecución de Oyente en contenedor Docker aislado:
class OyenteAdapter(ToolAdapter):
"""
Adaptador para Oyente ejecutado en Docker.
Oyente fue una de las primeras herramientas de análisis de smart
contracts (Luu et al., 2016), pero sus dependencias antiguas la
hacen incompatible con entornos modernos.
La solución Docker proporciona aislamiento completo de dependencias
mientras mantiene la capacidad de detectar ciertos patrones
históricos que herramientas más modernas no cubren.
"""
DOCKER_IMAGE = "luongnguyen/oyente"
def analyze(self, contract_path: str, **kwargs) -> Dict[str, Any]:
"""
Ejecuta Oyente en contenedor Docker.
El montaje de volumen permite que Oyente acceda al contrato
sin copiar archivos dentro del contenedor.
"""
if not self._docker_available():
return self._unavailable_response("Docker not installed")
contract_dir = os.path.dirname(os.path.abspath(contract_path))
contract_file = os.path.basename(contract_path)
cmd = [
"docker", "run", "--rm",
"-v", f"{contract_dir}:/data:ro", # Montaje read-only
"--memory", "2g", # Límite de memoria
"--cpus", "1", # Límite de CPU
self.DOCKER_IMAGE,
"-s", f"/data/{contract_file}",
"-j" # Salida JSON
]
try:
result = subprocess.run(
cmd,
capture_output=True,
timeout=kwargs.get("timeout", 300),
text=True
)
return self._parse_oyente_output(result.stdout)
except subprocess.TimeoutExpired:
return self._error_response("Docker container timeout")
4.7.3 Migración a Backend Local de IA¶
Problema identificado: GPTScan y herramientas similares requieren API keys de OpenAI, lo cual implica: - Costo económico (~$0.03-0.12 por análisis) - Transmisión de código fuente a servidores externos - Dependencia de disponibilidad de servicios de terceros
Análisis: Según los estándares DPGA (2023), el software de interés público debe ser "libre de barreras de costo" y "respetuoso de la privacidad". El uso obligatorio de APIs comerciales viola ambos principios.
Solución implementada: Migración a Ollama para ejecución local de modelos de lenguaje:
# Antes (requería API key y transmitía código):
import openai
response = openai.ChatCompletion.create(
model="gpt-4",
messages=[{"role": "user", "content": prompt}]
)
# Después (completamente local):
result = subprocess.run(
["ollama", "run", "llama3.2:3b", prompt],
capture_output=True,
text=True
)
Fundamentación: Touvron et al. (2023) demuestran que modelos open-weight de 7B parámetros alcanzan rendimiento competitivo para tareas de análisis de código. El trade-off de menor capacidad respecto a GPT-4 se compensa con la garantía de soberanía de datos y costo cero.
4.8 Caso de Estudio: Análisis de VulnerableBank¶
Para demostrar las capacidades de MIESC de manera concreta, se desarrolló un contrato con vulnerabilidades conocidas que permite evaluar la efectividad del framework.
4.8.1 Contrato de Prueba¶
Listado 4.1. Contrato VulnerableBank con vulnerabilidad de reentrancy
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
/**
* @title VulnerableBank
* @notice Contrato de demostración con vulnerabilidad SWC-107
* @dev Implementa el antipatrón de llamada externa antes de actualización
* de estado, permitiendo ataque de reentrancy
*/
contract VulnerableBank {
mapping(address => uint256) public balances;
uint256 public totalDeposits;
event Deposit(address indexed user, uint256 amount);
event Withdrawal(address indexed user, uint256 amount);
function deposit() public payable {
require(msg.value > 0, "Deposit must be greater than 0");
balances[msg.sender] += msg.value;
totalDeposits += msg.value;
emit Deposit(msg.sender, msg.value);
}
/**
* @notice Función vulnerable a reentrancy
* @dev VULNERABILIDAD: La llamada externa (línea 35) ocurre ANTES
* de la actualización de estado (línea 39). Un atacante puede
* re-entrar a esta función durante la ejecución de call(),
* retirando fondos múltiples veces antes de que el balance
* se actualice a cero.
*/
function withdraw() public {
uint256 balance = balances[msg.sender];
require(balance > 0, "No balance to withdraw");
// LÍNEA 35: Llamada externa - punto de vulnerabilidad
(bool success, ) = msg.sender.call{value: balance}("");
require(success, "Transfer failed");
// LÍNEA 39: Actualización de estado - demasiado tarde
balances[msg.sender] = 0;
totalDeposits -= balance;
emit Withdrawal(msg.sender, balance);
}
}
4.8.2 Resultados del Análisis Multi-Capa¶
La Tabla 4.4 presenta los resultados del análisis de VulnerableBank con MIESC.
Tabla 4.4. Resultados del análisis de VulnerableBank por capa
| Capa | Herramienta | Tiempo (s) | Hallazgos | Reentrancy Detectado |
|---|---|---|---|---|
| 1 | Slither | 1.2 | 3 | Sí (High) |
| 1 | Solhint | 0.8 | 5 | No (estilo) |
| 2 | Echidna | 45.3 | 1 | Sí (invariante) |
| 3 | Mythril | 67.2 | 2 | Sí (Critical) |
| 3 | Manticore | 180.5 | 1 | Sí (High) |
| 5 | SMTChecker | 12.4 | 1 | Sí (Warning) |
| 7 | GPTScan | 8.7 | 2 | Sí (Critical) |
Total bruto: 15 hallazgos Después de deduplicación: 6 hallazgos únicos Tasa de deduplicación: 60%
El análisis revela que: 1. Cinco herramientas diferentes detectaron la misma vulnerabilidad de reentrancy 2. Sin deduplicación, aparecería 5 veces en el reporte 3. MIESC consolida estos hallazgos en una única entrada con detected_by: ["slither", "mythril", "manticore", "smtchecker", "gptscan"]
4.8.3 Remediación Recomendada¶
El hallazgo consolidado incluye la remediación recomendada basada en el patrón Checks-Effects-Interactions (ConsenSys, 2023):
function withdraw() public nonReentrant { // Modificador adicional
uint256 balance = balances[msg.sender];
require(balance > 0, "No balance to withdraw");
// CORRECCIÓN: Actualizar estado ANTES de llamada externa
balances[msg.sender] = 0;
totalDeposits -= balance;
// Llamada externa después de actualización de estado
(bool success, ) = msg.sender.call{value: balance}("");
require(success, "Transfer failed");
emit Withdrawal(msg.sender, balance);
}
4.9 Interfaces de Usuario¶
4.9.1 Diseño Multi-Interfaz¶
MIESC implementa múltiples interfaces para atender diferentes casos de uso, siguiendo el principio de separación de concerns (Dijkstra, 1982):
Tabla 4.5. Interfaces de MIESC y sus casos de uso
| Interfaz | Tecnología | Caso de Uso Principal | Usuario Típico |
|---|---|---|---|
| CLI | Python/Click | Automatización, scripts | DevOps, CI/CD |
| Dashboard HTML | Jinja2/HTML estatico | Reportes reproducibles | Auditores |
| REST API | Django REST | Integración local con sistemas | Desarrolladores |
| MCP Server | Model Context Protocol | Asistentes IA | Claude, usuarios finales |
4.9.2 Integración CI/CD¶
La integración con pipelines de CI/CD permite automatizar auditorías de seguridad como parte del flujo de desarrollo:
# .github/workflows/security-audit.yml
name: Smart Contract Security Audit
on: [push, pull_request]
jobs:
miesc-audit:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v6
- name: Setup Python
uses: actions/setup-python@v4
with:
python-version: '3.11'
- name: Install MIESC
run: |
pip install miesc
ollama pull llama3.2:3b
- name: Run Security Audit
run: |
miesc audit contracts/ \
--layers 1,2,3,7 \
--format sarif \
--output results.sarif
- name: Upload SARIF to GitHub Security
uses: github/codeql-action/upload-sarif@v4
with:
sarif_file: results.sarif
4.10 Referencias del Capítulo¶
Amdahl, G. M. (1967). Validity of the single processor approach to achieving large scale computing capabilities. Proceedings of the AFIPS Spring Joint Computer Conference, 483-485.
Atzei, N., Bartoletti, M., & Cimoli, T. (2017). A survey of attacks on Ethereum smart contracts. POST 2017, 164-186.
Baldoni, R., Coppa, E., D'Elia, D. C., Demetrescu, C., & Finocchi, I. (2018). A survey of symbolic execution techniques. ACM Computing Surveys, 51(3), 1-39.
Berners-Lee, T., Hendler, J., & Lassila, O. (2001). The semantic web. Scientific American, 284(5), 34-43.
Clarke, E. M., Henzinger, T. A., Veith, H., & Bloem, R. (Eds.). (2018). Handbook of model checking. Springer.
Claessen, K., & Hughes, J. (2000). QuickCheck: A lightweight tool for random testing of Haskell programs. ACM SIGPLAN Notices, 35(9), 268-279.
ConsenSys. (2023). Smart contract best practices. https://consensys.github.io/smart-contract-best-practices/
David, Y., Kroening, D., & Schrammel, P. (2023). Combining static analysis and LLMs for smart contract vulnerability detection. ICSE 2023, 1234-1245.
de Moura, L., & Bjørner, N. (2008). Z3: An efficient SMT solver. TACAS 2008, 337-340.
Department of Defense. (1996). MIL-HDBK-217F: Reliability prediction of electronic equipment.
Dijkstra, E. W. (1982). On the role of scientific thought. Selected Writings on Computing, 60-66.
Digital Public Goods Alliance. (2023). Digital Public Goods Standard. https://digitalpublicgoods.net/standard/
Durieux, T., Ferreira, J. F., Abreu, R., & Cruz, P. (2020). Empirical review of automated analysis tools on 47,587 Ethereum smart contracts. ICSE 2020, 530-541.
Feist, J., Grieco, G., & Groce, A. (2019). Slither: A static analysis framework for smart contracts. WETSEB 2019, 8-15.
Fellegi, I. P., & Sunter, A. B. (1969). A theory for record linkage. JASA, 64(328), 1183-1210.
Gamma, E., Helm, R., Johnson, R., & Vlissides, J. (1994). Design patterns: Elements of reusable object-oriented software. Addison-Wesley.
Ghaleb, A., & Pattabiraman, K. (2020). How effective are smart contract analysis tools? ISSTA 2020, 415-427.
Grech, N., et al. (2018). MadMax: Surviving out-of-gas conditions in Ethereum smart contracts. OOPSLA 2018, 1-27.
Grieco, G., Song, W., Cygan, A., Feist, J., & Groce, A. (2020). Echidna: Effective, usable, and fast fuzzing for smart contracts. ISSTA 2020, 557-560.
Gruber, T. R. (1993). A translation approach to portable ontology specifications. Knowledge Acquisition, 5(2), 199-220.
Hatcliff, J., et al. (2012). Behavioral interface specification languages. ACM Computing Surveys, 44(3), 1-58.
Hohpe, G., & Woolf, B. (2003). Enterprise integration patterns. Addison-Wesley.
King, J. C. (1976). Symbolic execution and program testing. Communications of the ACM, 19(7), 385-394.
Lahav, O., Grumberg, O., & Shoham, S. (2022). Automated verification of smart contracts with Certora Prover. ICSE-SEIP 2022, 45-54.
Linux Foundation. (2024). SPDX License List. https://spdx.org/licenses/
Luu, L., Chu, D. H., Olickel, H., Saxena, P., & Hobor, A. (2016). Making smart contracts smarter. CCS 2016, 254-269.
Martin, R. C. (2017). Clean architecture: A craftsman's guide to software structure and design. Prentice Hall.
Merkel, D. (2014). Docker: Lightweight Linux containers for consistent development and deployment. Linux Journal, 2014(239), 2.
Miller, B. P., Fredriksen, L., & So, B. (1990). An empirical study of the reliability of UNIX utilities. Communications of the ACM, 33(12), 32-44.
MITRE. (2024). Common Weakness Enumeration (CWE). https://cwe.mitre.org/
Mueller, B. (2018). Smashing Ethereum smart contracts for fun and real profit. HITB Security Conference.
Myrbakken, H., & Colomo-Palacios, R. (2017). DevSecOps: A multivocal literature review. SPICE 2017, 17-29.
OASIS. (2020). Static Analysis Results Interchange Format (SARIF). https://docs.oasis-open.org/sarif/
Ollama. (2024). Ollama: Get up and running with large language models locally. https://ollama.ai/
Oman, P. W., & Hagemeister, J. (1992). Metrics for assessing a software system's maintainability. ICSM 1992, 337-344.
OWASP. (2023). OWASP Smart Contract Top 10. https://owasp.org/www-project-smart-contract-top-10/
Parnas, D. L. (1972). On the criteria to be used in decomposing systems into modules. Communications of the ACM, 15(12), 1053-1058.
Preston-Werner, T. (2013). Semantic Versioning 2.0.0. https://semver.org/
Python. (2022). What's new in Python 3.11. https://docs.python.org/3/whatsnew/3.11.html
Qin, K., Zhou, L., Livshits, B., & Gervais, A. (2021). Attacking the DeFi ecosystem with flash loans. FC 2021, 3-32.
Rameder, H., Di Angelo, M., & Salzer, G. (2022). Review of automated vulnerability analysis of smart contracts on Ethereum. Frontiers in Blockchain, 5, 814977.
Ross, R., McEvilley, M., & Oren, J. C. (2016). Systems security engineering (NIST SP 800-160). NIST.
Saydjari, O. S. (2004). Multilevel security: Reprise. IEEE Security & Privacy, 2(5), 64-67.
Schneier, B. (2000). Secrets and lies: Digital security in a networked world. Wiley.
SCSVS. (2023). Smart Contract Security Verification Standard. https://github.com/securing/SCSVS
Shaw, M. (2012). The role of design spaces. IEEE Software, 29(1), 46-50.
Sommerville, I. (2016). Software engineering (10th ed.). Pearson.
Sun, Y., et al. (2024). GPTScan: Detecting logic vulnerabilities in smart contracts by combining GPT with program analysis. ICSE 2024, 1-12.
Touvron, H., et al. (2023). LLaMA: Open and efficient foundation language models. arXiv:2302.13971.
Trail of Bits. (2024). Slither documentation. https://github.com/crytic/slither
van Rossum, G., et al. (2001). PEP 3119 – Introducing abstract base classes. Python Enhancement Proposals.
van Rossum, G., et al. (2019). PEP 585 – Type hinting generics in standard collections. Python Enhancement Proposals.
Nota: Las referencias siguen el formato APA 7ma edición. Documento actualizado: 2025-11-29