Introducción

Con el objetivo claro de atraer usuarios a su red, Cardano ha estado trabajando en una nueva máquina virtual con la capacidad de ejecutar contratos inteligentes del tipo Turing Completo, con paralelización y gran velocidad. Esta máquina, denominada KEVM está siendo construida para ser compatible con la EVM de Ethereum, permitiendo así que los desarrolladores de smart contracts de Ethereum, puedan portar sus smart contracts a Cardano y gozar de una mayor escalabilidad y capacidades de red. De esta manera, los desarrolladores de Cardano buscan extender el horizonte y dotar de interoperabilidad a las aplicaciones que se ejecutan entre estas blockchains. 

¿Qué es la KEVM?

Para entender un poco qué es la KEVM, debemos comprender un poco como funcionan los compiladores de lenguajes de programación. Estos compiladores tienen la tarea de convertir programas escritos en lenguajes de alto nivel en programas escritos en bajo nivel (generalmente código binario). Luego, estos códigos son interpretados por lo que llamamos una "máquina". A veces, esta máquina está implementada en silicio (llamada "CPU" o "núcleo"), pero a veces, es otro programa que hace las veces de un CPU, al cual llamamos "Máquina Virtual" o "VM". En pocas palabras, una Máquina Virtual o VM, es simplemente "una CPU implementada en software" que acepta determinadas instrucciones y las realiza según su programación. 

Este mecanismo es usado en prácticamente todas las criptomonedas, en menor o mayor medida, pero fue Ethereum la primera en explotar sus posibilidades al máximo. En Ethereum, se conoce como Ethereum Virtual Machine (EVM) a la máquina virtual capaz de hacer funcionar las instrucciones de sus transacciones y smart contracts (contratos inteligentes) sobre su blockchain.

Origen del proyecto

Sin embargo, no es la única y de hecho, en 2017, IOHK financió la Universidad de Illinois y Runtime Verification para; (1) desarrollar KEVM, una especificación formal para EVM, (2) utilizar la especificación para generar automáticamente una implementación correcta por construcción (una máquina virtual) y, (3) que esto fuera lo suficientemente rápida para usarse en una red de prueba. En el trabajo, también se incluyeron pruebas de corrección de los contratos inteligentes.

La misma especificación que produce KEVM se usa para mostrar que un contrato hace lo que se supone que debe hacer. Esto nos da una idea del enfoque de Runtime Verification:

Primero haga el arduo trabajo de crear una especificación formal, luego obtenga los beneficios al obtener herramientas y capacidades por menos dinero que si se desarrollaran de forma independiente

El trabajo de KEVM formalizó un diseño de máquina virtual existente para Cardano. Esa experiencia, más el trabajo previo en el marco del compilador LLVM, sugirió una nueva máquina virtual con el potencial de ser más rápida que EVM, inherentemente más resistente a las vulnerabilidades de los contratos inteligentes y diseñada para facilitar las pruebas de la corrección del contrato.

KEVM es un entorno de desarrollo diseñado por Cardano, cuyo nombre proviene de “K Ethereum Virtual Machine”, y está pensado para proporcionar a los desarrolladores una máquina virtual a través de la cual puedan desplegar y probar sus contratos inteligentes creados con Solidity, sin tener que aprender nuevas habilidades de programación. Con esta opción, los desarrolladores tienen la posibilidad de realizar sus actividades de producción de contratos inteligentes en un entorno más rápido y con un costo mucho menor. Y lo mejor, tienen la capacidad de expandir las funcionalidades de Cardano a nuevos niveles. 

Objetivo de su funcionamiento

Al igual que EVM de Ethereum, el objetivo primordial de KEVM es la de proveer a los desarrolladores de un entorno de desarrollo mediante el cual puedan realizar sus actividades en la programación y puesta a punto de aplicaciones y contratos inteligentes que se ejecutan en la blockchain. Por otro lado, KEVM busca desplegar sus funcionalidades a mayor velocidad y con un gasto económico mucho menor a como ocurre en la blockchain de Ethereum.

Además, también busca abrir nuevas vías de cooperación en una comunidad que cada día se expande vertiginosamente. En este sentido, con KEVM, Cardano abre sus puertas a la comunidad Solidity/Ethereum, mediante una plataforma compatible e interoperable usando su código nativo.

Proporcionar un entorno para el desarrollo de herramientas derivadas, tales como intérpretes, verificadores de tipos, verificadores de equivalencia y depuradores. Así como su utilización para la creación de herramientas de análisis tanto estáticas como dinámicas.

Reducir significativamente las vulnerabilidades de la máquina virtual de Ethereum (EVM). Existen muchas clases de errores sutiles de este tipo en los contratos inteligentes, que van desde dependencias de ordenación de transacciones hasta excepciones mal gestionadas. El problema se torna mucho más complicado debido a la interconexión que existe entre los contratos inteligentes. Es decir, la EVM admite la ejecución entre contratos, y éstos descargan información de otros contratos en la red para realizar sus cálculos.

Separar la especificación de las herramientas de análisis de la especificación de lenguajes de programación particulares u otros modelos, facilitando la especificación tanto de las herramientas de análisis como de los lenguajes de programación.  KEVM permite proporcionar una definición formal, limpia y no ambigua que puede transformarse mecánicamente en un intérprete de referencia para el EVM y una serie de herramientas de análisis formalmente rigurosas.

Relacionado: Solidity, el lenguaje de programación de Ethereum

¿Cómo funciona?

KEVM es una versión de la máquina virtual de Ethereum EVM, con la variante de que KEVM se desarrolla sobre el framework K. Este framework K, es una plataforma semántica utilizada para crear lenguajes de programación y máquinas virtuales formalmente verificadas. Esto en consonancia a que Cardano es un proyecto donde la verificación formal y científica es fundamental para toda tecnología dentro del proyecto. 

De esta forma, el framework K permite a los desarrolladores definir o implementar la semántica formal de un lenguaje de programación de forma intuitiva y modular. K también genera una máquina virtual ejecutable, “correcta por construcción” a partir de su especificación formal. De esta forma, es lo suficientemente rápida y potente para ejecutar programas reales y contratos inteligentes. 

Por otro lado, los desarrolladores de este framework, esperan a largo plazo y con ayuda de otras empresas como Runtime Verification, construir un entorno K en el que sea posible "conectar y usar" nuevas máquinas virtuales. Esto permitiría elevar los niveles de interoperabilidad blockchain a un nivel donde las mismas VM de las criptomonedas sean capaces de habilitar dicho funcionamiento sin segundas capas. 

Con la implementación de KEVM, Cardano busca proveer a los miembros de su comunidad, diferentes recursos de soporte. Entre ellos, una red de prueba a través de la cual brindan la oportunidad a los desarrolladores de probar todas las funciones de la red principal de Ethereum, así como lo ha venido haciendo con las redes de Shelley y Goguen.  Entre estos recursos, se incluyen operaciones de grupos de interés, bloqueo de tokens, metadatos y más. La red de prueba de Cardano también le ofrece la funcionalidad de lanzamiento previo a la red principal.

Rigurosidad y semántica comprobables

En KEVM además, se define una instancia formalmente rigurosa y ejecutable de la semántica EVM en el framework K, cubriendo todas las instrucciones de EVM. Basada en la semántica formal proporcionada en K es capaz de encontrar ambigüedades presentes en la especificación original de EVM, aparentemente formal pero incompleta, validando el enfoque del propio framework K. KEVM es de código abierto, para su uso como semántica de referencia en el desarrollo de clientes de Ethereum.

También KEVM funciona como intérprete de referencias EVM. Utilizando la semántica formal del framework K, se genera automáticamente un intérprete de referencia EVM capaz de ejecutar transacciones EVM y actualizar el estado del mundo EVM en consecuencia. En el que se abstraen algunos detalles del propio sistema blockchain, y proporciona un intérprete derivado formalmente capaz de ejecutar el conjunto de pruebas oficial de EVM con un tiempo de ejecución razonable. 

Este es el primer intérprete completo de Ethereum formalmente riguroso que no depende de una implementación incorporada de la EVM, y el primer intérprete de la EVM formalmente especificado que pasa el conjunto de 40683 pruebas de conformidad con el EVM. Además, el intérprete derivado demuestra un buen rendimiento, que lo hace útil como plataforma de pruebas en el mundo real.

Verificación de funcionalidades

En su función como verificador de programa de EVM, también se pueden observar características que hacen de KEVM una herramienta apropiada para trabajar en Ethereum. La propiedad especificada incluye tanto la corrección funcional del programa EVM, así como la complejidad del gas del programa. Al hacerlo se demuestran herramientas de análisis de software EVM rigurosamente derivadas y respaldadas por una semántica EVM formal, completa y legible para el ser humano de la semántica EVM.

Por otro lado, KEVM representa un conjunto de herramientas unificado. Existen muchas herramientas de análisis de software para el ecosistema de Ethereum. Con KEVM se puede generar automáticamente este conjunto de herramientas a partir de una única semántica formal, comprobable y ejecutable que reduce la probabilidad de que se produzcan errores en dichas herramientas a causa de modelos divergentes.

Diferencias entre la KEVM y la EVM

  1. La primera gran diferencia entre KEVM y EVM, es que la primera parte de un enfoque de desarrollo más formal y verificable. Esto permite que KEVM sea mucho más íntegra y segura. Además, de que su creación con el framework K le permita una mayor portabilidad e interoperabilidad.
  2. Otra gran diferencia es que la especificación e implementación de la KEVM es menos ambigua, lo que da lugar a una mejor seguridad. Esto significa que errores como los que llevaron a la caída de The DAO o el fallo del Parity Bug serían mucho más difíciles de cometer, y en caso de existir, estos podrían detectarse de mejor manera e incluso crear mecanismos de seguridad que eviten por completo esos comportamientos maliciosos.
  3. KEVM también ofrece un mejor soporte para ataques DoS usando instrucciones de computación infinita (lo que llevó a la creación del Gas en Ethereum y su EVM), lo que permite relajar esta regla (el uso de Gas) abaratando el coste de las transacciones.
  4. KEVM cuenta con la capacidad de ser fácilmente portable a otras blockchains (usando el framework K) algo que la EVM no tiene. Esto por ejemplo, permite que la KEVM pueda ser portada a nuevas arquitecturas u otras blockchain de forma mucho más sencilla.

Relacionado: Matic se convierte en la primera plataforma en lanzar feeds nativos de Chainlink fuera de Ethereum

Conclusiones

Una consecuencia del éxito práctico y académico de la primera criptomoneda que irrumpe en el ámbito de la economía criptográfica (bitcoin), es la búsqueda de aplicaciones potencialmente prometedoras en la tecnología blockchain.

Entre estas búsquedas se cuenta la EVM de Ethereum, que consiste en una máquina virtual para el desarrollo y ejecución de programas en la blockchain, a modo de una computadora mundial sobre la blockchain de Ethereum.

Uno de los objetivos de la implementación de EVM en Ethereum es permitir el desarrollo de aplicaciones y scripts arbitrarios que se ejecuten en transacciones de la blockchain, utilizando ésta para sincronizar su estado globalmente de una manera que puede ser verificada por cualquier participante en el sistema. 

Los participantes y los contratos en el sistema Ethereum realizan transacciones en una moneda distribuida conocida como Ether. Las cuentas de la red Ethereum pueden estar asociadas a programas en un lenguaje basado en máquinas virtuales llamado EVM.

Ahora bien, estas características de las EVM al ejecutar programas (contratos inteligentes) la ha hecho muy versátil. Esto ha incrementado su popularidad en la ejecución de transacciones sin la necesidad de intervención de terceras personas en las negociaciones.

Desafortunadamente, el auge de estas tecnologías se ha visto empañado por una serie repetida de vulnerabilidades de seguridad y fallas de contratos de alto perfil. Para abordar estas fallas, la comunidad de Ethereum ha recurrido a la verificación formal y al análisis de programas. Dos opciones que muestran una gran promesa debido a la simplicidad computacional y la ejecución en tiempo limitado inherentes a los contratos inteligentes. 

A pesar de esto, no existe ningún sistema completamente formal, riguroso y la semántica ejecutable de la EVM (Ethereum Virtual Machine) que existe actualmente, deja una falta de rigor en la que basar dichas herramientas. En este trabajo, Cardano presenta KEVM, la primera semántica formal completamente ejecutable del EVM, el lenguaje de código de bytes en el que se ejecutan los contratos inteligentes.

Esta semántica es creada en un framework para la semántica ejecutable llamado framework K. Esta semántica no solo demostró que pasa el conjunto oficial de pruebas de estrés de 40683 pruebas para implementaciones de EVM. Sino que también reveló ambigüedades y posibles fuentes de error en la formalización en papel existente de la semántica de EVM en la que se basa KEVM.  Estas propiedades hacen de KEVM una implementación de referencia formal ideal frente a la cual se pueden evaluar otras implementaciones.