Traducción al español 
Documento Original publicado por Jeremy Wood, Jefe de Estrategia, el 11 de Julio de 2018
La tecnología de los contratos inteligentes atrae la atención a medida que se innova en informática
Como una blockchain (cadena de bloques) de tercera generación, Cardano incorpora tecnología de última generación que atrae el interés de científicos informáticos en todo el mundo. El año pasado, se presentaron trabajos que describían el algoritmo de consenso de Cardano en las principales conferencias de criptografía, y este mes fue el turno de su tecnología de contratos inteligentes para estar en el foco de atención.
Grigore Rosu, profesor de informática en la Universidad de Illinois en Urbana-Champaign, y su startup Runtime Verification han estado trabajando con IOHK desde junio de 2017 para desarrollar nueva tecnología basada en la semántica formal para Cardano, incluyendo una nueva máquina virtual. Él y su colega Everett Hildenbrandt vinieron a Reino Unido la semana pasada para dar presentaciones en la séptima Conferencia de Lógica Federada (FLoC), que este año se celebra en la ciudad de Oxford y se celebra del 6 al 19 de julio con unos 2000 asistentes. Esta importante conferencia se celebra aproximadamente cada cuatro años en varios lugares del mundo, y bajo su paraguas se celebran juntos nueve importantes conferencias internacionales de informática. Estos cubren temas como los métodos formales, la lógica y los lenguajes de programación. Destacadas figuras de estos mundos vienen a participar y los discursos principales de este año son de Shafi Goldwasser y Silvio Micali, los criptógrafos y ganadores de los premios Turing, y el matemático George Gonthier.
El sábado, Grigore tuvo el honor de dar su primera charla invitada por FLoC, en el marco lógico y los meta-lenguajes: Taller de “Teoría y Práctica” y su charla fue sobre el marco K. Se trataba de una presentación técnica, que profundizaba en el formalismo lógico subyacente a la K, y en la lógica de emparejamiento, una variante lógica de primer orden para especificar y razonar sobre la estructura por medio de patrones y emparejamiento de patrones.
Grigore Rosu
Esta tecnología, desarrollada por Grigore y su start-up Runtime Verification, ha sido desarrollada en los últimos 15 años y se utiliza en software de misión crítica que no puede permitirse el lujo de fallar. Con este fin, Runtime Verification ha trabajado con empresas como NASA, Boeing y Toyota y muchas otras. Su colaboración con IOHK comenzó después de haber sido contactado por el CEO Charles Hoskinson, quien se dio cuenta de que las vulnerabilidades de software que habían resultado en una serie de problemas en las blockchains y en el drenaje de cientos de millones de dólares, podían haberse evitado utilizando los métodos formales desarrollados por Grigore y su equipo.
El marco K se utilizó para modelar formalmente la semántica de la máquina virtual Ethereum, y el conocimiento obtenido de este proceso se empleó para diseñar IELE, la máquina virtual para Cardano que se lanzará en un formato de prueba dentro de unas semanas. Esta es la primera vez que esta tecnología se implementa en la industria de las blockchain. Es importante destacar que K es un medio para verificar formalmente el código de los contratos inteligentes, de modo que se puedan comprobar automáticamente los tipos de defectos que han conducido a pérdidas financieras catastróficas, y deben evitarse a toda costa.
Dijo Grigore: “Diseñamos IELE desde cero como una especificación formal utilizando K y generamos la VM automáticamente a partir de la especificación. Por lo tanto, no hay nada que probar acerca de la VM en términos de exactitud, porque es correcto por construcción”. Añadió: “Analizamos retrospectivamente la especificación EVM que definimos anteriormente, y analizamos todos nuestros intentos de verificar contratos inteligentes con ella y luego volvimos a pensar cómo debería haber sido diseñada una máquina virtual para superar todos esos problemas. Se nos ocurrió IELE. Esta es una VM similar a LLVM para la blockchain. Para mí, como diseñador de K, este es un hito muy importante, y es la primera vez que se define un lenguaje real en K y se genera automáticamente su implementación”.
El miércoles por la tarde, Grigore dará una segunda charla invitada en FLoC, en la Conferencia Internacional sobre Estructuras Formales de Cálculo y Deducción (FSCD), sobre la importancia del análisis formal y la verificación de blockchain y máquinas virtuales. La presentación será un poco menos técnica que su primera charla, y cubrirá Cardano, y cómo las herramientas desarrolladas por Runtime Verification permitieron la generación automática de una máquina virtual correcta por contrastación, IELE, a partir de una especificación formal.
Y el martes, en el 31º Simposio IEEE Computer Security Foundations, Everett presentará cómo él y el equipo desarrollaron KEVM. Everett dijo: “KEVM es una especificación formal de la Ethereum Virtual Machine (EVM) en K, que genera no sólo una VM sino también un motor de ejecución simbólica, así como un verificador de programa deductivo para contratos inteligentes de Ethereum. Había una gran necesidad de una especificación formal de EVM tan completa, porque la semántica anterior era demasiado informal o incompleta. Sin una semántica formal de EVM, el problema de verificar un contrato inteligente no tiene sentido”.
Runtime Verification y IOHK
Con tres charlas en total en FLoC en Oxford, es genial ver esta tecnología reconocida en un evento internacional tan importante. La seguridad es de suma importancia en el diseño y la producción de blockchains y en IOHK ponemos los métodos formales en el centro de nuestro enfoque de diseño. K ya ha sido utilizado para formalizar C, Java, JavaScript, PHP, Python, Rust, y usando estas técnicas también planeamos hacer que IELE esté abierto a desarrolladores de muchos lenguajes, no sólo a Solidity. También ofreceremos nuestros propios idiomas, Plutus y Marlowe, que actualmente están en desarrollo con científicos informáticos como Philip Wadler y Simon Thompson.
Los lectores que deseen experimentar con la testnet KEVM pueden hacerlo a través de nuestro sitio web de testnets Cardano. Estamos listos para lanzar el IELE en este mismo sitio en tan sólo unas semanas a partir de ahora. Manténgase en sintonía para más actualizaciones.
Material gráfico, Mike Beeple