¿Qué es la KEVM? Un proyecto para mejorar la EVM desde Cardano

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.