El artículo de investigación presenta un método de verificación formal que aprovecha la norma #ColoredPetriNets (CPN) para mejorar la seguridad de los contratos inteligentes #Blockchain-based , abordando específicamente las vulnerabilidades #reentrancy . Estas vulnerabilidades plantean amenazas significativas debido al uso cada vez mayor de contratos inteligentes en aplicaciones del mundo real, lo que genera implicaciones financieras.
Los problemas abordados incluyen los riesgos de seguridad inherentes asociados con los contratos inteligentes, que surgen debido a sus características y entornos de ejecución únicos. Las vulnerabilidades de reentrada, donde los contratos pueden explotarse para realizar llamadas reentrantes no autorizadas, lo que genera comportamientos inesperados y pérdidas financieras, son una preocupación principal.
Para mitigar estos riesgos, el artículo propone un enfoque de verificación formal basado en la CPN. Introduce los conceptos de flujo de datos y flujo de control para modelar mejor los procesos de ejecución de transacciones, centrándose en el contrato #DAO (Organización Autónoma Descentralizada) como estudio de caso. El modelo CPN simula jerárquicamente la ejecución de contratos y reproduce los comportamientos de los atacantes para identificar vulnerabilidades potenciales.
La investigación presenta análisis experimentales utilizando herramientas CPN para simular la ejecución normal de contratos, escenarios de ataque y análisis posteriores de espacios de estados, informes de estado y diagramas de estado. Estos análisis tienen como objetivo detectar anomalías en las transacciones de datos e identificar vulnerabilidades potenciales dentro de los contratos inteligentes.
Los hallazgos demuestran la eficacia de la herramienta basada en CPN para detectar vulnerabilidades de reentrada sin falsos positivos, superando a las herramientas de análisis existentes como Oyente, Mythril y Slither. Sin embargo, el enfoque CPN requiere la participación humana en el modelado y análisis, lo que indica la necesidad de técnicas de modelado automatizado más maduras.
En conclusión, el artículo subraya la importancia de los métodos de verificación formal como CPN para mejorar la seguridad de los contratos inteligentes. El trabajo futuro implica refinar los modelos para manejar transacciones de múltiples partes y realizar más investigaciones sobre CPN para mejorar la seguridad de los contratos inteligentes y optimizar su rendimiento.
