Pruebas simbólicas con Halmos: aprovechamiento de las pruebas existentes para la verificación formal

La verificación formal, el proceso de usar métodos matemáticos para "inspeccionar" un programa o contrato inteligente en cualquier número de entradas, generalmente se considera la alternativa más concisa y completa a las pruebas tradicionales para escribir código más seguro y de mayor calidad. Pero en realidad, la verificación formal es un proceso abierto e interactivo. Al igual que las pruebas unitarias, los desarrolladores deben definir dinámicamente y superponer especificaciones formales, iterando en su enfoque a medida que evolucionan su código y análisis. Además, la verificación formal solo es tan efectiva como sus especificaciones, cuya redacción puede llevar mucho tiempo (y, a menudo, conlleva una curva de aprendizaje pronunciada). 

Para muchos desarrolladores que consideran que el proceso es desalentador, las pruebas unitarias suelen ser la ruta más rentable y eficiente en el tiempo para determinar la corrección de un programa. En la práctica, la verificación formal no es una alternativa más integral a las pruebas unitarias, sino complementaria. Estos procesos tienen diferentes puntos fuertes y limitaciones, lo que proporciona una seguridad aún mayor cuando se usan juntos. Los desarrolladores siempre necesitarán escribir pruebas unitarias, entonces, ¿qué pasaría si pudiéramos usar las mismas propiedades para la verificación formal?

Halmos, nuestra herramienta de verificación formal de código abierto, permite a los desarrolladores reutilizar las mismas propiedades escritas para pruebas unitarias para especificaciones formales a través de pruebas simbólicas. En lugar de tener que crear un conjunto sólido de propiedades desde el principio, los desarrolladores pueden evitar la duplicación de trabajo y mejorar sus pruebas con algunas especificaciones a la vez sin comenzar desde cero. Diseñamos esta herramienta para su uso, junto con otras en el proceso de verificación formal, como una vía de acceso a la verificación formal; los desarrolladores pueden comenzar con algunos análisis con un esfuerzo mínimo, antes de agregar más adelante en el proceso.

En esta publicación, cubrimos los desafíos de la verificación formal y el potencial para cerrar la brecha entre las pruebas unitarias y la verificación formal con pruebas simbólicas. Luego recorremos una demostración de Halmos utilizando el código de contrato inteligente existente y echamos un vistazo rápido a otras herramientas de verificación formales (muchas de código abierto) disponibles para los desarrolladores.

Verificación formal vs prueba

Verificación formal - generalmente favorecido por los desarrolladores de blockchain por su rigor y exhaustividad - es el proceso de probar la corrección de un programa mediante la verificación de que cumple con ciertas propiedades de corrección. Las propiedades, que son específicas del programa, generalmente se proporcionan de forma externa y se expresan mediante un lenguaje formal o una notación respaldada por la herramienta de verificación que se utiliza. Los desarrolladores a menudo perciben la verificación formal como una solución de botón para probar las propiedades en todos los escenarios posibles de forma automática, pero en realidad, la verificación formal puede ser un proceso que requiere mucha mano de obra y es altamente interactivo.

Al igual que la verificación formal, las pruebas unitarias implican evaluar si un programa funciona como se espera; la prueba, sin embargo, solo verifica el comportamiento del programa para algo entradas, mientras que la verificación formal puede comprobarlo para todos entradas posibles. Tanto la prueba como la verificación formal requieren una descripción del comportamiento esperado del programa (con casos de prueba usados ​​en la prueba y especificaciones formales usadas en la verificación formal). Pero, cuando se usan juntos, pueden proporcionar un examen más completo de un programa. Las pruebas, por ejemplo, son efectivas para encontrar errores y fallas simples, pero generalmente son más rápidas y fáciles de realizar. La verificación formal, aunque más engorrosa de usar, es lo suficientemente potente como para demostrar la ausencia de errores o revelar errores sutiles que son fáciles de pasar por alto en las pruebas o revisiones de código.

Sobrecarga de especificación

Uno de los principales desafíos de la verificación formal es la sobrecarga de escribir y mantener especificaciones formales. Este proceso a menudo implica la tarea que lleva mucho tiempo de escribir manualmente las especificaciones usando un lenguaje especializado (que muchos desarrolladores necesitarán aprender primero). El proceso también es incremental, generalmente comienza escribiendo propiedades simples y verificándolas primero, luego agrega gradualmente propiedades más complejas en la parte superior. Al igual que las pruebas, es un proceso abierto, sin un punto de parada claro, y solo se pueden agregar tantas propiedades como sea posible dentro del marco de tiempo disponible. Además, cuando los desarrolladores cambian el código mientras se verifica, también deben actualizar sus especificaciones existentes, lo que genera esfuerzos de mantenimiento adicionales. Estos factores pueden hacer que la verificación formal sea una tarea desalentadora para algunos desarrolladores que dudan en comprometerse con los gastos generales adicionales.

Y aunque las pruebas y la verificación formal pueden mejorar la calidad del código cuando se usan juntas, ambas requieren descripciones (a veces similares) del comportamiento esperado de un programa en diferentes lenguajes y formatos. Escribir y mantener estas descripciones requiere mucho trabajo, y mantener dos formas diferentes de la misma descripción puede parecer un esfuerzo duplicado. Esto plantea la siguiente pregunta: ¿es posible describir el comportamiento esperado de una manera que los desarrolladores puedan usar tanto para la prueba como para la verificación?

Cerrando la brecha entre las pruebas y la verificación formal con pruebas simbólicas y Halmos

La prueba simbólica, la práctica de ejecutar pruebas con entradas simbólicas, es un método de verificación formal eficaz que reduce la sobrecarga de especificación. Este enfoque permite el uso de los mismos casos de prueba tanto para la prueba como para la verificación formal. A diferencia de las pruebas tradicionales, que verifican que un programa funciona correctamente para un conjunto limitado de entradas, las pruebas simbólicas verifican el programa en busca de todas las entradas posibles, por lo tanto, un programa que pasa las pruebas simbólicas puede considerarse formalmente verificado.

Halmos es una herramienta de verificación formal diseñada para pruebas simbólicas. En lugar de requerir especificaciones separadas o aprender un nuevo idioma, Halmos usa pruebas existentes como especificaciones formales. Ejecutar pruebas a través de Halmos verificará automáticamente que pasen todas las entradas posibles o proporcionará contraejemplos. Esto no solo elimina la necesidad de escribir especificaciones adicionales, sino que también permite la reutilización de pruebas escritas para pruebas unitarias o fuzzing, con fines de verificación formal.

Por lo tanto, los desarrolladores tienen una mayor flexibilidad para elegir entre una variedad de opciones de control de calidad, que incluyen pruebas unitarias, fuzzing y verificación formal, según sus necesidades actuales. Por ejemplo, las pruebas pueden identificar rápidamente errores simples, posiblemente con la ayuda de un fuzzer que genera entradas aleatorias, y luego Halmos puede aumentar aún más la confianza en la corrección del programa en todas las entradas.

Ejemplo: Probar el isPowerOfTwo() función

Como ejemplo, considere lo siguiente isPowerOfTwo() función, que determina si un número dado es una potencia de dos. Esta función utiliza un algoritmo de manipulación de bits para la eficiencia, pero puede ser un desafío probar su corrección, particularmente en el caso en que la entrada no sea una potencia de dos.

Imagine la siguiente prueba para el isPowerOfTwo() función: compara la salida real de la función con la salida esperada para una entrada dada. Esta es una prueba parametrizada (también conocida como prueba basada en propiedades), lo que significa que puede ejecutarla fácilmente con diferentes valores de entrada, posiblemente con herramientas de fuzzing como Foundry.

Puede utilizar esta prueba para examinar la isPowerOfTwo() funcionar a través de pruebas unitarias o pruebas fuzz, ejecutándolo con una selección de entradas. Pruebas como estas no pueden probar formalmente la corrección de la función, ya que es computacionalmente inviable ejecutar la prueba para cada entrada posible.

Sin embargo, Halmos permite a los desarrolladores reutilizar estas pruebas preexistentes para la verificación formal con solo un pequeño esfuerzo adicional. La herramienta verifica que las pruebas pasen para todas las entradas posibles realizando una ejecución simbólica de la prueba y luego verificando que la afirmación nunca se viole (o, si la afirmación is violado, proporcionando un contraejemplo). Esto significa que si la prueba pasa Halmos, la corrección de la función se verifica formalmente, lo que significa que el algoritmo se implementa correctamente y el compilador lo ha traducido con precisión en código de bytes.

Limitación: ejecución simbólica limitada

Por lo general, no es posible realizar pruebas simbólicas completas y totalmente automáticas, ya que esto requeriría resolver el problema de detención, que se sabe que es indecidible. Una de las razones de esto es que a menudo es imposible determinar automáticamente cuántas veces un ciclo debe iterar simbólicamente. Como resultado, la verificación formal completamente automática es generalmente indecidible.

Dadas estas limitaciones fundamentales, Halmos prioriza la automatización sobre la integridad. Con este fin, Halmos está diseñado para realizar un razonamiento simbólico acotado para bucles no acotados (donde el número de iteraciones depende de las entradas del programa) o arreglos de longitud variable (incluyendo cadenas). Esto sacrifica algo de integridad, pero permite a Halmos evitar que el usuario proporcione anotaciones adicionales, como invariantes de bucle.

Por ejemplo, considere la siguiente versión iterativa del isPowerOfTwo() función, que presenta un bucle while ilimitado, donde el número de iteraciones del bucle está determinado por el número mínimo de bits necesarios para representar el número de entrada.

Halmos itera simbólicamente este bucle ilimitado solo hasta un límite especificado. Por ejemplo, si el límite se establece en 3, Halmos iterará el ciclo como máximo 3 veces y no considerará los valores de entrada que harían que el ciclo itera más de 3 veces (es decir, cualquier valor mayor o igual a 2^3 ). En este caso particular, establecer el límite en 256 o más permitiría que Halmos esté completo.

Demostración: Verificación formal de ERC721A con Halmos

Para demostrar las capacidades de Halmos, lo usamos para probar simbólicamente y verificar formalmente ERC721A, una implementación altamente optimizada de gas del estándar ERC721 que permite la acuñación por lotes a casi el mismo costo que la acuñación única. ERC721A incluye varios innovadores optimizaciones para lograr esta eficiencia; por ejemplo, se puede ahorrar gasolina retrasando las actualizaciones de los datos de propiedad del token hasta que se transfiera el token, no en el momento de la acuñación. Esto requiere el uso de estructuras de datos y algoritmos complejos para recuperar de manera eficiente la información de propiedad de la estructura de datos diferida. Y aunque esta optimización mejora la eficiencia del gas, también aumenta la complejidad del código y dificulta probar la corrección de la implementación. Esto convierte a ERC721A en un buen candidato para la verificación formal, ya que puede aumentar la confianza en la implementación y beneficiar a los usuarios potenciales.

Propiedades de prueba simbólicas

Dado que las pruebas existentes para ERC721A se escribieron en JavaScript con Hardhat (que actualmente no es compatible con Halmos), escribimos nuevas pruebas en Solidity para las principales funciones del punto de entrada: mint(), burn()y transfer(). Estas pruebas comprobaron que cada función actualiza correctamente la propiedad y el saldo del token, y solo afecta a los usuarios relevantes sin alterar el saldo o la propiedad de otros usuarios. Esto último no es trivial de probar debido al uso del algoritmo de estructura de datos perezosos en ERC721A. Por ejemplo, la siguiente prueba verifica que el transfer() la función actualiza correctamente la propiedad del token especificado:

Otra prueba verifica que el transfer() La función no altera el saldo de otras direcciones, lo cual es difícil de probar como se mencionó anteriormente:

Resultados de la verificación

Realizamos un experimento de verificación usando Halmos en el contrato inteligente ERC721A escribiendo un total de Prueba 19. Las pruebas se realizaron a través de Halmos con un límite de desarrollo de bucle de 3, que tardó 16 minutos en completarse. El desglose del tiempo de verificación se puede ver en la siguiente tabla. El experimento se realizó en una MacBook Pro con un chip M1 Pro y 16 GB de memoria.

Probar	Hora (s)
pruebaBurnBalanceUpdate	6.67
testBurnNextTokenIdSin cambios	1.40
pruebaQuemarOtroSaldoPreservación	5.69
testBurnOtherPropiedadPreservación	189.70
pruebaBurnOwnershipUpdate	3.81
requisitos de prueba de grabación	71.95
pruebaMintBalanceUpdate	0.20
pruebaMintNextTokenIdActualizar	0.18
pruebaMintOtherBalancePreservation	0.26
pruebaCasa de la monedaOtroPropiedadPreservación	5.74
pruebaMintOwnershipUpdate	1.38
testMintRequisitos	0.09
testTransferBalanceSin cambios	9.03
pruebaTransferirSaldoActualizar	53.53
testTransferNextTokenIdSin cambios	4.47
pruebaTransferirOtroSaldoPreservación	19.57
pruebaTransferirOtroPropiedadPreservación	430.61
pruebaTransferirPropiedadActualizar	18.71
requisitos de transferencia de prueba	149.18

Si bien la mayoría de las pruebas se completaron en cuestión de segundos, algunas de ellas tardaron varios minutos. Estas pruebas que requerían mucho tiempo fueron difíciles de verificar debido a la naturaleza compleja de los casos a considerar, y estaban estrechamente relacionadas con la corrección del algoritmo de estructura de datos perezosos.

En general, los resultados de este experimento indican que Halmos puede verificar de manera efectiva la corrección del código de contrato inteligente. Brinda mayor confianza en la integridad del código, a pesar de la complejidad y los posibles casos extremos del contrato inteligente.

Experimente con errores inyectados

Para demostrar la efectividad del razonamiento acotado de Halmos, lo usamos para detectar errores en una versión anterior del contrato ERC721A. Esta versión tenía un problema que manejaba mal el desbordamiento aritmético y potencialmente permitía la acuñación por lotes de una gran cantidad de tokens, lo que podría romper la integridad de la estructura de datos diferidos y provocar que algunos usuarios perdieran la propiedad de sus tokens (un problema resuelto en la versión actual). Realizamos el mismo conjunto de 19 pruebas para ERC721A en la versión con errores, y Halmos pudo encontrar un contraejemplo para las propiedades del mint() función. Específicamente, Halmos proporcionó valores de entrada que condujeron al escenario de explotación descrito anteriormente. Los resultados de este experimento indican que, a pesar de estar incompleto, el razonamiento acotado de Halmos puede ser una forma efectiva de detectar y prevenir errores explotables en contratos inteligentes.

Trabajo relacionado

Varios equipos han desarrollado herramientas de verificación formal para el código de bytes del contrato inteligente de Ethereum. Estas herramientas, incluido Halmos, se pueden usar para ayudar a garantizar la seguridad y la corrección de los contratos inteligentes. Comparar y comprender las diferentes características, capacidades y limitaciones de estas herramientas puede ayudar a los desarrolladores a elegir la más adecuada para sus necesidades únicas.

Si bien Halmos es una valiosa adición al conjunto de herramientas disponible para la verificación inteligente de contratos, está destinado a complementar (no reemplazar) las herramientas existentes. Los desarrolladores pueden combinar Halmos con otras herramientas para lograr un mayor nivel de seguridad en sus contratos. A continuación, comparamos Halmos con algunas herramientas formales seleccionadas que admiten el código de bytes EVM.

• K es un poderoso marco de verificación formal que permite la verificación deductiva y la demostración interactiva de teoremas. Su teoría e implementación subyacentes proporcionan un alto nivel de expresividad, lo que lo hace adecuado para verificar programas y algoritmos complejos. Sin embargo, debe tenerse en cuenta que K no está diseñado con un gran énfasis en la verificación automatizada y carece de ciertas características de automatización que pueden requerir más esfuerzo manual durante el proceso de verificación. Para usar el marco K, las especificaciones formales están escritas en el lenguaje K, que debe aprenderse antes de su uso. Su fortaleza es particularmente útil en la verificación de sistemas complejos, que pueden ser difíciles de analizar mediante el razonamiento automatizado.
• Certora es una herramienta de verificación formal para contratos inteligentes que se enfoca en la verificación automatizada y admite la verificación de modelos acotados, similar a Halmos. Para usar Certora, los desarrolladores deben aprender su nuevo lenguaje, CVL, con el fin de escribir especificaciones. Este lenguaje permite la descripción concisa de muchas propiedades críticas a través de contratos invariantes, una función que Halmos actualmente no admite. A pesar de ser una herramienta propietaria de código cerrado, Certora proporciona una sólida herramienta de verificación formal, con un desarrollo continuo y una buena asistencia al usuario.
  
  Halmos, por otro lado, es una herramienta de código abierto que es de menor escala y actualmente carece de algunas funciones proporcionadas por Certora, pero está destinada a servir como un bien público y está pensada como una solución de nicho para verificar rápidamente contratos inteligentes sin la necesidad de una instalación y un mantenimiento extensos.
• HEVM es otra herramienta de verificación formal que es similar a Halmos. Anteriormente formaba parte de DappTools, que es un precursor de Foundry. Tanto HEVM como Halmos tienen la característica de no requerir una especificación separada y pueden ejecutar simbólicamente pruebas existentes para identificar violaciones de afirmaciones. Esto permite a los usuarios usar ambas herramientas indistintamente o ejecutarlas en paralelo para las mismas pruebas, brindándoles múltiples opciones para pruebas simbólicas.
  
  Vale la pena señalar que, a pesar de sus similitudes, HEVM y Halmos se han desarrollado de forma independiente y difieren en los detalles de implementación; particularmente en términos de optimizaciones y estrategias de razonamiento simbólico. Además, HEVM está escrito en Haskell, mientras que Halmos está escrito en Python, lo que brinda exposición al rico ecosistema de Python. Tener la capacidad de usar ambas herramientas brinda a los usuarios más flexibilidad y opciones para garantizar la seguridad y la corrección de los contratos inteligentes.

Halmos es de código abierto y actualmente se encuentra en su fase beta. Estamos trabajando activamente en nuevos Características y funcionalidad, incluidos los códigos de trucos de Foundry y varias otras funciones clave de usabilidad. Apreciaríamos mucho sus opiniones sobre qué características son las más importantes y agradecemos cualquier comentario, sugerencia y contribución para hacer de Halmos una mejor herramienta para todos.

**

Las opiniones expresadas aquí son las del personal individual de AH Capital Management, LLC ("a16z") citado y no son las opiniones de a16z o sus afiliados. Cierta información contenida aquí se ha obtenido de fuentes de terceros, incluso de compañías de cartera de fondos administrados por a16z. Si bien se tomó de fuentes que se consideran confiables, a16z no ha verificado de forma independiente dicha información y no hace declaraciones sobre la precisión actual o duradera de la información o su idoneidad para una situación determinada. Además, este contenido puede incluir anuncios de terceros; a16z no ha revisado dichos anuncios y no respalda ningún contenido publicitario incluido en ellos.

Este contenido se proporciona solo con fines informativos y no debe considerarse como asesoramiento legal, comercial, de inversión o fiscal. Debe consultar a sus propios asesores sobre estos asuntos. Las referencias a cualquier valor o activo digital son solo para fines ilustrativos y no constituyen una recomendación de inversión ni una oferta para proporcionar servicios de asesoramiento de inversión. Además, este contenido no está dirigido ni destinado a ser utilizado por ningún inversionista o posible inversionista, y bajo ninguna circunstancia se puede confiar en él al tomar una decisión de invertir en cualquier fondo administrado por a16z. (Una oferta para invertir en un fondo a16z se realizará solo mediante el memorando de colocación privada, el acuerdo de suscripción y otra documentación relevante de dicho fondo y debe leerse en su totalidad). Cualquier inversión o compañía de cartera mencionada, referida o descritos no son representativos de todas las inversiones en vehículos administrados por a16z, y no puede garantizarse que las inversiones serán rentables o que otras inversiones realizadas en el futuro tendrán características o resultados similares. Una lista de inversiones realizadas por fondos administrados por Andreessen Horowitz (excluyendo inversiones para las cuales el emisor no ha otorgado permiso para que a16z divulgue públicamente, así como inversiones no anunciadas en activos digitales que cotizan en bolsa) está disponible en https://a16z.com/investments /.

Los cuadros y gráficos proporcionados en el interior tienen únicamente fines informativos y no se debe confiar en ellos al tomar cualquier decisión de inversión. El rendimiento pasado no es indicativo de resultados futuros. El contenido habla sólo a partir de la fecha indicada. Todas las proyecciones, estimaciones, pronósticos, objetivos, perspectivas y/u opiniones expresadas en estos materiales están sujetas a cambios sin previo aviso y pueden diferir o ser contrarias a las opiniones expresadas por otros. Consulte https://a16z.com/disclosures para obtener información adicional importante.