Por Grigore Rosu, Everett Hildenbrandt, Daejun Park, Shuvendu Lahiri
"Las pruebas muestran la presencia, no la ausencia de errores" (Dijkstra, 1969). Aunque se ha logrado un progreso notable en las pruebas durante los últimos 50 años, las pruebas exhaustivas siguen siendo inviables en la mayoría de los casos y hemos aprendido, a veces de la manera más dura, que los errores restantes pueden tener consecuencias catastróficas.
La naturaleza de la blockchain, donde el código que accede a un estado compartido es público y puede ser invocado por cualquiera desde cualquier lugar, amplifica tanto la velocidad a la que los hackers encuentran errores como las consecuencias de sus explotaciones. Por lo tanto, las pruebas son simplemente insuficientes aquí. La verificación formal es la única alternativa viable conocida.
Esta charla explicará qué es la verificación formal en el contexto de contratos inteligentes, tokens y protocolos de blockchain, por qué se está volviendo cada vez más crítica, cómo se realiza y qué herramientas están disponibles. Se cubren varios enfoques, desde los automatizados y ligeros que encuentran errores hasta los interactivos y exhaustivos que analizan todos los comportamientos, desde el código fuente de alto nivel que los desarrolladores escriben y entienden hasta el bytecode de bajo nivel que es ejecutado por los clientes de nodo.
Esta charla también tiene como objetivo crear conciencia de que, contrariamente a la comprensión común donde la verificación formal se confunde con la auditoría de código, se requiere significativamente más esfuerzo para verificar formalmente un programa que para escribir el programa en primer lugar. ¡Piensa en 9 veces más! De hecho, una regla general en NASA es que el 20% del presupuesto de un proyecto se destina a la escritura de código y el 80% a la verificación y validación; y el código de NASA no es público y nadie más que NASA puede invocarlo una vez desplegado.