KEVM
KEVM se denomina a la implementación formalmente verificada de la Ethereum Virtual Machine mediante el framework K. Esta implementación opera en una red lateral (side-chain) a la red principal de Cardano (mainnet) permitiendo la portabilidad de los contratos inteligentes en Solidity.
Sobre la verificación formal
¿Qué es la verificación formal?
Muy parecido a la matemática, la ciencia o la lógica, el desarrollador de software al escribir un programa informático siempre se encuentra con el problema de la corrección: ¿Se comporta realmente el código como pienso? ¿Resuelve correctamente el problema que busco resolver? Ante esta cuestión, una primera forma de resolver este problema es el testing, es decir, someter al programa a un número abundante y diverso de datos de entrada para verificar si este retorna en la totalidad de los casos la respuesta correcta. Entre mayor sea la cantidad de pruebas que se haga al software mayor será entonces su corrección, sin embargo, según este método, la corrección nunca es absoluta pues siempre puede existir un caso límite ulterior que imprevisiblemente retorne un error. Pues bien, una segunda alternativa para resolver este problema es la verificación formal, este es un proceso de demostración donde se comprueba a través de técnicas lógicas-matemáticas que el código es correcto, en caso de tener éxito queda comprobado entonces que el código cumple de forma completa los requerimientos esperados (independiente de cualquier variación en los datos de entrada). Este método es semejante al proceso que hace un matemático para demostrar que un triangulo tiene siempre 180º indiferente del largo de sus lados, a diferencia de ir calculando que esto es así tomando en cuenta una cantidad de triángulos ejemplares.
¿Por qué la verificación formal es importante?
La verificación formal es el medio por el cual se comprueba de forma universal que un código tiene ciertas propiedades, por lo tanto, garantiza con exactitud el comportamiento de una pieza de software para todos los escenarios posibles. La verificación de un software con este nivel de certeza siempre es deseable, pero debido a la gran cantidad de trabajo que lleva hacer una demostración es raro que en la práctica todo el código se encuentre formalmente verificado. Ahora bien, hay sistemas informáticos en los que una falla implica la pérdida de vidas o grandes cantidades de recursos económicos, para estas situaciones de alto riesgo es crucial el uso de estos métodos. Un claro ejemplo de aquello es la tecnología blockchain donde se gestionan abundantes cantidades de dinero, por lo cual la verificación formal se está volviendo una creciente tendencia en el mundo del desarrollo de la web 3.0.
Explicación KEVM
K Framework
Es un framework de código abierto que fue desarrollado por la empresa Runtime Verification que sirve para verificación formal de lenguajes de programación, así se puede resolver el problema de la corrección especificando definiciones básicas del código y reglas sobre cómo este debe comportarse. Por otra parte, el objetivo de este framework es acelerar y facilitar el desarrollo de nuevos lenguajes de programación, pues una vez especificado el lenguaje con el framework K este puede de forma automática derivar un entorno de desarrollo con herramientas de compilación y depuradores (debugging). Su uso no solo se limita al desarrollo de lenguajes de programación sino también para cualquier segmento de código que se desee verificar, siendo así una herramienta útil para demostrar la corrección de contratos inteligentes que gestionan transacciones en redes blockchain.
KEVM
Esta es una versión corregida de la máquina virtual de Ethereum impulsada por el área de investigación la empresa IOHK, a través del uso del framework K se busca realizar una implementación formalmente verificada que genere código EVM compatible, con esto se busca disminuir de forma significativa las vulnerabilidades de la versión original y hacer que el código resultante de la compilación sea también mas eficiente.
Nota: Para ver una explicación en detalle de la máquina virtual de Ethereum véase este artículo.
Ethereum side-chain
La KEVM se desplegará en una cadena lateral (side-chain) a la cadena principal de Cardano, esta es una red de capa 2 en desarrollo que tiene como objetivo fomentar la venida de proyectos del ecosistema presentes en Ethereum a Cardano. En ella se podrá portar exactamente igual los contratos que hayan sido escritos en Solidity en la red principal de Ethereum, asimismo a lo largo del tiempo se mantendrá compatible con cualquier hard fork de Ethereum, facilitando de ese modo la migración de cualquier proyecto que haya estado operando anteriormente en la red de Ethereum. Por otro lado, a diferencia de Ethereum no funcionará mediante un protocolo basado en proof of work, sino que, utilizará una versión del protocolo Ouroboros (Ouroboros Byzantine Fault Tolerance) el cual permite disminuir sustantivamente los costos de operación y lograr una mayor rapidez de la red.
Bibliografía
- Runtime Verification: K Framework for Smart Contract Formal Verification with Rikard Hjort. ETHWarsaw. https://www.youtube.com/watch?v=M_dYueOubBA
- K Framework - An Overview. Run time verification. https://runtimeverification.com/blog/k-framework-an-overview/
- KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine paper. https://daejunpark.github.io/kevm.pdf
- Nikolai Kudasov: Formal Semantics for Programming Languages. CQFN talks and lectures. https://www.youtube.com/watch?v=2ztCZIpQ-3E
- Introducing the KEVM - an Ethereum Virtual Machine for Cardano smart contract development. IOKH. https://www.youtube.com/watch?v=fGGV4fzV2Z8
- K semantic framework docs. https://kframework.org/
- ¿Qué es la KEVM? Un proyecto para mejorar la EVM desde Cardano. Cointelegraph Blog. https://es.cointelegraph.com/explained/what-is-kevm-a-project-to-improve-evm-from-cardano
- Introducing the Cardano EVM sidechain. IOHK blog. https://iohk.io/en/blog/posts/2022/07/06/introducing-the-cardano-evm-sidechain/