Las cadenas de bloques son mantenidas por una red de participantes, nodos mineros, que ejecutan algoritmos diseñados para mantener colectivamente una máquina distribuida tolerante a los ataques bizantinos. Desde el punto de vista de los usuarios, las cadenas de bloques ofrecen la ilusión de ordenadores centralizados que realizan cálculos verificables y fiables, en los que todos los cálculos son deterministas y los resultados no pueden manipularse ni deshacerse.
Los investigadores del Instituto IMDEA Software Martín Ceresa y César Sánchez publican “Multi: A Formal Playground for Multi-Smart Contract” en el que implementan un modelo de ejecución que permite el estudio de las interacciones de los contratos inteligentes.
Cada cadena de bloques está equipada con una criptomoneda. Los programas que se ejecutan en las cadenas de bloques se denominan contratos inteligentes y están escritos en un lenguaje de programación especial con semántica determinista. Cada transacción comienza con una invocación de un usuario externo a un contrato inteligente. Los contratos inteligentes tienen almacenamiento local y pueden llamar a otros contratos y, lo que es más importante, almacenan, envían y reciben criptomonedas.
Una vez instalado en una blockchain, el código del smart-contract no puede modificarse. Por lo tanto, es muy importante garantizar que los contratos son correctos antes de su despliegue. Sin embargo, el ecosistema resultante hace muy difícil razonar sobre la corrección de los programas, ya que los smart-contracts pueden ser ejecutados por usuarios malintencionados o pueden diseñarse smart-contracts malintencionados para explotar otros contratos que los llamen. Muchos ataques y fallos se deben a interacciones inesperadas entre varios contratos, el contrato atacado y código desconocido que realiza el exploit.
Además, existe una competencia muy agresiva entre las distintas blockchains para ampliar su base de usuarios. Las ideas se implementan rápidamente y las blockchains compiten por ofrecer y adoptar nuevas características con rapidez.
En este trabajo, los invetigadores proponen un campo de juego formal que permite razonar sobre interacciones multicontrato y es extensible para incorporar nuevas características, estudiar su comportamiento y, en última instancia, demostrar propiedades antes de que las características se incorporen a la blockchain real. Además, implementan un modelo de computación que modela la plataforma de ejecución, abstrae el código interno de cada contrato individual y se centra en las interacciones contractuales. Aunque su implementación es todavía un trabajo en curso, muestran cómo muchas características, existentes o propuestas, pueden utilizarse para razonar sobre las interacciones multicontrato.
