Registro:
| Documento: | Tesis de Grado |
| Título: | Verificación automática de smart contracts move en Sui |
| Autor: | Mansini, Leo |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Fecha de defensa: | 2025-09-09 |
| Fecha en portada: | 2025 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Garbervetsky, Diego David |
| Jurado: | Galeotti, Juan Pablo; Godoy, Javier Ignacio |
| Idioma: | Español |
| Palabras clave: | VERIFICACION AUTOMATICA; SMART CONTRACTS; MOVE; SUI; RUST; KANI VERIFIERAUTOMATED VERIFICATION; SMART CONTRACTS; MOVE; SUI; RUST; KANI VERIFIER |
| Formato: | PDF |
| Handle: |
https://hdl.handle.net/20.500.12110/seminario_nCOM000891_Mansini |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000891_Mansini.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000891_Mansini |
| Ubicación: | Dep.COM 000891 |
| Derechos de Acceso: | Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Mansini, Leo. (2025). Verificación automática de smart contracts move en Sui. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000891_Mansini |
Resumen:
En el ecosistema de las blockchains, la verificación formal de contratos inteligentes es fundamental para garantizar su seguridad y confiabilidad, evitando vulnerabilidades que podrían resultar en pérdidas económicas o fallas de funcionamiento. Sui, una blockchain que utiliza el lenguaje Move, presenta un enfoque innovador para la gestión de objetos y transacciones, pero aún cuenta con un ecosistema de herramientas de verificación en desarrollo. Este trabajo tiene como objetivo explorar métodos para la verificación automática de contratos en Sui. Se realiza un estudio del estado actual de la verificación en Move, evaluando la herramienta Move Prover en su capacidad para comprobar propiedades de seguridad en módulos escritos para Sui. Además, se propone un flujo de trabajo alternativo que traduce código Move a Rust de manera controlada, con el fin de habilitar el uso del verificador Kani, herramienta enfocada en análisis exhaustivo de propiedades y detección de errores en tiempo de compilación. Los resultados muestran que Move Prover no es capaz de interpretar el modelo actual de objetos de Move, mientras que la traducción a Rust permitió aprovechar verificadores externos con mucha mejor capacidad de verificación, aunque requirió ajustes manuales y simplificaciones del código para poder representar el funcionamiento de Move en Rust.
Abstract:
In the blockchain ecosystem, the formal verification of smart contracts is essential to ensure their security and reliability, preventing vulnerabilities that could lead to economic losses or functional failures. Sui, a blockchain that uses the Move language, offers an innovative approach to object and transaction management, but still has a verification tool ecosystem in development. This work aims to explore methods for the automated verification of contracts in Sui. It examines the current state of verification in Move, evaluating the Move Prover tool in its ability to check security properties in modules written for Sui. In addition, it proposes an alternative workflow that translates Move code into Rust in a controlled manner, in order to enable the use of the Kani verifier, a tool focused on exhaustive property analysis and error detection at compile time. The results show that Move Prover is not capable of interpreting Move’s current object model, whereas translation to Rust made it possible to leverage external verifiers with much greater verification capabilities, although it required manual adjustments and code simplifications in order to represent Move’s behavior in Rust.
Citación:
---------- APA ----------
Mansini, Leo. (2025). Verificación automática de smart contracts move en Sui. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000891_Mansini
---------- CHICAGO ----------
Mansini, Leo. "Verificación automática de smart contracts move en Sui". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2025.https://hdl.handle.net/20.500.12110/seminario_nCOM000891_Mansini
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000891_Mansini.pdf
Distrubución geográfica
