Verificación y Validación Formal de Contratos Inteligentes para Blockchain con Alloy
Resumo
Blockchain es la base tecnológica de una nueva forma de realiz-ar transacciones de manera segura en una red descentralizada. Dicha tecnología permite registrar la validez y el origen de los datos, y realizar transacciones de manera digital, compartida, inalterable y sin la intervención de intermediarios. Frecuentemente, las transacciones requieren de lógica automa-tizada. En estos casos, se vuelve necesaria la definición de con-tratos inteligentes, programas de computación almacenados en Blockchain que se ejecutan automáticamente cuando se cumplen condiciones predeterminadas. Los errores en contra-tos inteligentes pueden tener graves consecuencias, especial-mente en ámbitos como finanzas descentralizadas. Una clara definición de las condiciones es esencial; sin embargo, éstas son generalmente descriptas en lenguaje natural por las partes involucradas, lo que conlleva a la ambigüedad de interpretación por parte de los programadores del contrato. Por otro lado, los errores en la programación también pueden derivar a que el contrato no se ejecute como se esperaba. La calidad del contra-to inteligente podría ser mejorada si las condiciones fueran especificadas en UML con OCL, y luego transformadas al len-guaje de modelado Alloy para llevar a cabo la verificación y validación formal a través del método Model Checking. En este artículo, se describe una línea de investigación que propone un modelo para la especificación de contratos inteligentes en UML y OCL, complementado con una transformación automática a Alloy para su verificación y validación. Dicho modelo contribuye a realizar una auditoría más rigurosa de contratos inteligentes antes de despliegue en Blockchain.
Referências
R. Fekih, “Formal verification of smart contracts based on model checking: An overview,” 2023. Accessed: Jun. 21, 2024. [Online]. Available: [link].
D. C. Schmidt, “Model-driven engineering,” IEEE Computer, vol. 39, no. 2, pp. 25–31, 2006, DOI: 10.1109/MC.2006.5810.
OMG. Unified Modeling Language (UML), version 2.5.1. 2017., [link]
OMG. Object Constraint Language (OCL), version 2.4. 2017. [link]
A. Van Deursen, P. Klint, and J. Visser, “Domain-specific languages: An annotated bibliography,” SIGPLAN Not., vol. 35, no. 6, pp. 26–36, 200011.
A. Garis and A. Sanchez, “Verification and Validation of Domain Specification Languages using Alloy,” in Proceedings of the XXI Congreso Argentino de Ciencias de la Computación (CACIC 2015), 2015, pp. 589-5984.
Alloy 6.2.0; [link]
A. Cunha, A. Garis, and D. Riesco, “Translating between Alloy specifications and UML class diagrams annotated with OCL,” Softw Syst Model, vol. 14, pp. 5–25, 2015, DOI: 10.1007/s10270-013-0353-52.
C. Bartolini, C. Palomba, and F. Lomuscio, “Smart Contract Modeling using UML and OCL for Formal Verification,” in 2021 IEEE International Conference on Software Architecture (ICSA), 2021, pp. 139–1501.
Y. Hsain, N. Laaz, and S. Mbarki, “Ethereum’s Smart Contracts Construction and Development using MDE Technologies: A Review,” Procedia Computer Science, vol. 181, pp. 250–257, 20216.
D. Jackson, Software Abstractions: Logic, Language, and Analysis, 2nd ed. MIT Press, 20127.
I. Grishchenko, M. Maffei, and C. Schneidewind, “A Semantic Framework for the Security Analysis of Ethereum Smart Contracts,” POPL, 20185.
D. Marmsoler, A. Ahmed, and A. D. Brucker, “Secure Smart Contracts with Isabelle/Solidity,” in Software Engineering and Formal Methods (SEFM 2024), A. Madeira and A. Knapp, Eds. Springer, 20259.
F. Vergés, A. Garis, and C. Tissera, “Sistema de Certificación Digital de Títulos Universitarios en Blockchain (UNSL Cert),” 2024.
