La verificación formal es un método poderoso para garantizar matemáticamente que los programas funcionen de una correcta y segura, pero sigue siendo un uso intensivo de recursos debido a su vigor. La verificación formal funciona mejor cuando los programas están escritos con un alto nivel de abstracción, admiten el razonamiento de ecuaciones y se descomponen en módulos discretos que se pueden verificar. La universidad de Yale con fondos de Columbia-IBM Blockchain Center, Columbia Data Science Institute. QTum Foundation y Ethereum Foundation, CertiK esta desarrollando el lenguaje de programación DeepSEA, que facilita el trabajo de la verificación formal y generar automáticamente el código ejecutable, con un modelo formal que se puede cargar en el demostrador del teorema de Coq. El modelo se genera como un programa funcional y con un mayor nivel de abstracción y con estilo de capas de abstracción.
La seguridad dentro de la Blockchain es un tema primordial, escribir un software de sistema certificable que este correcto requiere de bastante trabajo. Los lenguajes de programación actuales no son adecuados para la tarea y mucho menos compatibles con la verificación formal. DeepSEA es un nuevo lenguaje para escribir contratos inteligentes verificados. Veamos algunos detalles:
¿Qué es DeepSEA y por qué se diseñó?
DeepSEA es un lenguaje que permite a los programadores manejar código extremadamente complejo mientras operan de manera elegante y segura para los propios codificadores. Ha sido diseñado para ser útil cuando se utiliza una verificación formal completa en el sistema de Coq que es un asistente de prueba.
La verificación forma demuestra matemáticamente que el código funcionara según lo previsto, calculando todos los escenarios posibles y como pioneros de la tecnología de verificación formal en contratos inteligentes y cadenas de bloques, CertiK descubrió que, aunque la verificación formal del software totalmente correcto seguía siendo muy costo y desafiante. Parte del problema se debe a la falta de compatibilidad con el lenguaje de programación. El lenguaje existente como C, OCaml y Solidity, no están preparados e integrados con las herramientas de verificación y requiere tiempo para crear y probar pruebas manuales. Sin embargo, el lenguaje que proporciona una forma de verificar formalmente las propiedades de corrección difíciles sobre los contratos inteligentes utilizando Coq Proof Assistant de una manera escalable y automatiza.
Suponiendo que gran parte del tiempo de un desarrollador se dedica a escribir pruebas en un asistente de prueba interactivo como Coq. DeepSEA tiene como objetivo eliminar la mayor cantidad de trabajo ocupado posible y ayudar a los desarrolladores a estructurar su sistema en modulo separados para que le resto del sistema contengan datos verificados. Pruebas herméticas.
¿Cómo se construye?
Al diseñar el lenguaje, se usaron cuatro principios que combinan las mejores características de varios otros lenguajes de programación.
Razonamiento ecuacional
Cada termino de DeepSEA se traduce en una especificación funcional correspondiente, que luego se puede razonar en el asistente de pruebas dentro de Coq.
Especificación en capas
DeepSEA mantiene las pruebas manejables mediante capas de abstracción que brindan una vista de alto nivel del programa. El compilador de muestra que la implementación del código en bytes sin formato se comporta como se esperaba, mientras que el programador solo necesita mirar la representación de alto nivel.
Encapsulación y composición
Cada capa de DeepSEA consta de un conjunto de objetos que se construyen sobre otra capa, y se puede comprobar que las capas son correctas una a la vez.
Refinamiento abstracto
DeepSEA verifica sistemas más grandes en pasos fáciles de usar. El proceso está estructurado como una serie de pruebas de refinamiento vinculadas que demuestran que un programa vinculado cumple con la especificación
¿Por qué importa todo esto?
Los ecosistemas de blockchain se construyen sobre las bases de la confianza. Si bien algunos argumentan que los protocolos de consenso son lo que hace que las cadenas de bloques sean confiables, algunos códigos aun no son realmente confiables debido a esos errores dentro de los programas y los piratas información que los aprovechan y explotan con sus malas intenciones.
Por ejemplo, si una función particular dentro de su contrato inteligente se desborda, eso es un problema. Si la implementación de una función no cumple con las especificaciones y genera una vulnerabilidad (No) intencionada, eso es un problema.
El programa debe de ser digno de confianza. Este requisito es importante en blockchain porque una vez que se implementa un contrato inteligente, no hay una manera fácil de deshacerlo, dejando las vulnerabilidades no detectadas abiertas a la explotación.
La verificación formal es la única forma confiable de asegurarse de que el código sea hermético y se verifique con hechos matemáticos inequívocos. Al demostrar que el programa maneja correctamente todos los valores de entrada posibles, matemáticamente se asegura que el código funcione solo como esta previsto. Todos los casos en los que se aplica la verificación formal, DeepSEA permite a los desarrolladores probar una cantidad arbitraria de contratos complejos.
Los contratos varían de simples a complejos al igual que la verificación formal. Las herramientas automáticas existente funcionan bien con contratos muy simples como los tokens; Sin embargo, para verificar contratos complejos como esquemas de votación o interacciones entre cadenas, necesitamos la flexibilidad para definir especificación y pruebas arbitrariamente complicadas.
Aquí es donde brilla los asistentes de prueba interactivos como Coq. Al integrar contratos inteligente y Coq, se puede aplicar la verificación formal a las tareas mas complicadas, lo que permite un sistema completamente verificado de principio a fin.
¿Hay otro idioma que lo admitan?
Hoy en día, casi todos los contratos están escritos en leguaje de programación que se diseñaron sin tener en cuenta la verificación formal. Incluso cuando se integran con un sistema de verificación formal, generalmente están orientados a tratar automáticamente casos simples.
El solucionar integrado Solidity SMT es un buen ejemplo. El solucionador SMT permite a los programadores anotar una función con condiciones que se suponen que son verdaderas, escribir afirmaciones que se deberían cumplirse y pedirle al compilador que las pruebe automáticamente. Sin embargo, las afirmaciones se limitan a un vocabulario fijo (sobre números y matrices) y solo puede hablar sobre el estado de un programa durante una llamada a un método en particular. Es decir, el solucionar solo puede probar la afirmación y no otros tipos de teoremas del mismo modo, el usuario debe confiar en que el compilador en si no tiene errores.
Los sistemas de verificación mas ambiciosos, por ejemplo, el marco K, eliminan algunos de estos problemas mediante el uso de una especificación formal del EVM y dejan que el programador realice mas trabajo manual (Por ejemplo, proporcionando invariantes de bucle) Sin embargo, estos sistemas de verificación carecen de abstracción de código en bytes y todavía solo se enfocan en propiedades de ejecución única con un vocabulario fijo.
Para obtener suficiente poder para verificar propiedades arbitrariamente complicadas, queremos usar un asistente de prueba interactivo como Coq o Isabelle. Aunque los asistentes de prueba interactivos tienen sus lenguajes de programación integrados, compilan mediante lenguajes de programación funcionales que utilizan recolectores de basura (recolectores de memoria automáticos)
En el contexto de Blockchain, tener un recolector de basura hace que los contratos inteligentes sean lentos y costosos, ya que se requiere de gas. Por lo tanto, el lenguaje integrado de Coq no se puede usar directamente para Ethereum. Afortunadamente, el compilador de DeepSEA cierra la brecha al generar un código ejecutable eficiente (Se puede ejecutar sin un recolector de basura) y un modelo formal que se puede cargar con Coq.
DeepSEA es un lenguaje muy flexible y compatible que puede crear un diseño fundamental e intuitivo con un alto nivel de abstracción y razonamiento utilizando Coq. DeepSEA proporciona una solución elegante para proteger el código: más nítido, más fuerte y más eficiente.
Parala tecnología de próxima generación, se requiere de una seguridad de próxima generación.
El lenguaje esta en etapa de construcción y pronto sera lanzado el Alpha.
GitHub del Manual : Website
Fuente / CertiK
¡Saludos!