En un esfuerzo de verificación formal, Ethereum busca la certeza de los contratos inteligentes

Hay una nueva palabra de moda en blockchain que llega justo a tiempo para el otoño: verificación formal.

La frase (usada para describir la aplicación de las matemáticas para verificar programas de software) hasta ahora ha sido evocada escasamente.en la prensa. Pero si la conversación en la cumbre de desarrolladores de Ethereum la semana pasada fue una indicación, podría desempeñar un papel cada vez más importante dadas las preguntas de seguridad que aún rodean a los contratos inteligentes y las cadenas de bloques en general.

Como lo demuestran las múltiples charlas dedicadas al tema en Devcon2, la idea de brindar nuevas garantías a los programadores de Ethereum está siendo ampliamente aceptada por la comunidad de desarrollo. El concepto ya se propone como una forma de inspirar confianza en todos los ámbitos, desde el propio protocolo de Ethereum hasta su blockchain experimental de prueba de participación.

Que esto haya sucedido quizás no sea una sorpresa dado el colapso repentino de The DAO este verano, hasta la fecha el contrato inteligente más grande lanzado en la plataforma de desarrollo de aplicaciones descentralizadas.

Pero mientras tantoverificación formal Puede parecer complejo, pero el concepto puede quizás resumirse sucintamente en su aplicación a Ethereum : los programadores actualmente usan un lenguaje en gran medida nuevo (Solidity) para escribir contratos inteligentes, escribiendo comandos que luego se traducen en código de bytes para su uso en la máquina virtual Ethereum (EVM) y se difunden a los nodos de la red para su ejecución.

En cierto sentido, la verificación formal puede verse como una manera más objetiva de garantizar que cuando los diferentes componentes de la red reciben estas instrucciones, las ejecutan según lo previsto en nombre de los usuarios.

Grant Passmore, cofundador de Aesthetic Integration, es un emprendedor que ve una oportunidad en ayudar en este esfuerzo, utilizando Devcon2 para lanzar Imandra Contracts, una plataforma de verificación formal para contratos inteligentes de blockchain.

En el evento, evocó la idea de que Ethereum podría servir como un "paraíso" para la verificación formal (un punto de contacto ampliamente citado en las conversaciones) dados los objetivos de su comunidad y las importantes responsabilidades que desea confiar al código.

Passmore le dijo a CoinDesk:

La comunidad de Ethereum se encuentra en una posición única. Tras The DAO, comprendemos que es necesaria una ingeniería rigurosa. No se puede abordar la redacción de un contrato inteligente como si se tratara de una aplicación web.

En otros lugares, oradores como Philip Daian de Cornell hablaron sobre el interés en la metodología de manera más amplia y le dijeron a la audiencia que cree que la verificación formal podría ayudar a Ethereum a resolver problemas clave.

"Será una pieza clave del panorama general. Espero usar Ethereum para establecer el estándar y mostrarle a la gente cómo se hace", afirmó.

ruedas de entrenamiento

Dado el énfasis reciente que las empresas financieras han puesto en explorarlenguajes de contratación inteligenteQuizás fue el concepto de aplicar la verificación formal a Solidity el que fue el tema de discusión más frecuente.

Desarrollado para la plataforma Ethereum , Solidity ha enfrentado críticas por no haber sido probado en gran medida y ser difícil de escribir, en gran parte debido a su reciente desarrollo. Estos problemas se han agravado debido a... asuntoscon el compilador del lenguaje, la falta de bibliotecas públicas y el colapso de The DAO, que fue examinado por miembros notables de su comunidad de desarrollo.

En este sentido, Christian Reitweissner, el creador de Solidity, reconoció que existe un impulso para implementar una verificación formal para que los codificadores de Ethereum puedan detectar los errores de manera más efectiva.

Reitweissner declaró a CoinDesk que los desarrolladores de contratos inteligentes podrían ONE día usar herramientas de verificación formal para, por ejemplo, determinar si existen errores imprevistos en su trabajo. Indicó que dicha herramienta podría utilizarse para determinar si, al sumar dos saldos, el resultado se extiende más allá del campo asignado por el compilador.

"Esto podría suceder y la herramienta de verificación formal lo detectaría automáticamente. Se puede detectar con antelación y reaccionar dentro del contrato inteligente", explicó.

Reitweissner dijo que el equipo de Solidity ya ha estado explorando cómo aplicar la verificación formal a su trabajo. Yael pasado octubreHabía prototipos de cómo un kit de herramientas llamado Why3 podría usarse para este propósito, aunque dichas ofertas aún no están disponibles para el lenguaje completo.

Campo de pruebas

Que Ethereum podría usarse para probar cómo se podría aplicar la verificación formal a las Finanzas de manera más amplia también fue un tema muy discutido durante la conferencia.

Passmore, por ejemplo, dijo que Aesthetic Integration ha estado trabajando en la aplicación de la verificación formal en el trabajo con instituciones financieras desde 2014, y que hasta ahora, los clientes han buscado usarla en áreas limitadas, como los dark pools, donde los comerciantes requieren certeza sobre la imparcialidad.

En los contratos inteligentes, Passmore sugirió que ve a Ethereum como una comunidad que podría impulsar aún más la aceptación.

"Muchos de nuestros clientes bancarios, cuando empezamos a trabajar con ellos, nos enteramos de que estaban interesados en el sector, pero que les preocupaba la corrección de los contratos inteligentes", afirmó.

El avance de la verificación formal también ha atraído a Yoichi Hirai por razones similares. Ingeniero de verificación formal, actualmente empleado por la Fundación Ethereum , su interés en el concepto surgió como investigador y en su anterior empleo en FireEye, empresa líder en ciberseguridad.

En una charla en la conferencia, Hirai habló sobre su frustración al aplicar la verificación formal en entornos donde no tenía acceso al código fuente o las tareas eran quizás demasiado amplias para avanzar en el concepto.

"Encontré Ethereum, vi el EVM, el documento amarillo, la especificación, solo tenía 32 páginas y pensé que realmente podía traducirlo y escribir pruebas sobre contratos inteligentes", dijo.

Ethereum, por el contrario, ofrece lo que él llamó una "especificación más pequeña" y un "problema solucionable" para que los ingenieros determinen cuál es la mejor manera de traducir Solidity en código de bytes.

"Creo que vendrán muchos más investigadores de verificación formal", dijo.

No hay bala de plata

Sin embargo, a pesar del entusiasmo, se están tomando medidas para prevenir el alcance de la verificación formal. El desarrollador Alex Beregszaszi, quien trabaja en las actualizaciones de la EVM, mencionó la necesidad de un conjunto de soluciones que ayuden a los desarrolladores a garantizar que el código de los contratos inteligentes funcione correctamente.

Passmore también señaló que es difícil decir si su nuevo sistema podría haber detectado problemas con The DAO, ya que las herramientas de verificación formal aún requieren intervención Human .

"Puedes codificar los problemas que ocurrieron con The DAO y verificar que no los tengas, pero debes saber qué buscar", explicó.

Reitweissner y Passmore reconocieron las limitaciones y advirtieron a los desarrolladores que no pensaran en la verificación formal como una “solución milagrosa”.

Reitweissner, sin embargo, ve la metodología como una que avanzará a medida que se use más ampliamente y los desarrolladores se vuelvan lentamente mejores en identificar problemas y desarrollar repositorios donde el conocimiento de los problemas comunes pueda hacerse accesible.

De esta manera, Passmore cree que la comunidad Ethereum está logrando "evangelizar" el concepto, algo que, según él, en última instancia hará avanzar la investigación de blockchain.

Passmore concluyó:

Aunque esto es algo a lo que muchos nunca han estado expuestos, la verificación formal es lo que necesitamos. Es un proceso de aprendizaje, pero hay que aceptarlo, y eso es emocionante.

Imágenes de Pete Rizzo para CoinDesk