Demostrando la seguridad de los protocolos de consenso basados en DAG

Los protocolos de consenso basados en DAG están siendo utilizados por empresas de blockchain para reducir el uso de energía y mejorar la Seguridad. Estos protocolos trabajan juntos para crear un orden parcial de bloques de transacción, lo que lleva a una secuencia clara de bloques. Dada la importancia de las blockchains, es necesario demostrar que componentes esenciales, particularmente los protocolos de consenso, funcionan como se espera.

Este artículo se centra en un método formal para probar la corrección de dos protocolos basados en DAG. Las especificaciones revelan varios métodos para transmitir, construir el DAG y ordenar que pueden combinarse para expresar los dos protocolos. El enfoque formal necesita ajustes para modelar el consenso de manera precisa. Inicialmente, se demuestra la seguridad del consenso basado en DAG en bloques líderes, y luego se refina para incluir todos los bloques y procesos.

Las especificaciones de cada protocolo constan de varias líneas, mientras que el sistema de prueba verifica muchas obligaciones en solo unos minutos.

#Importancia de la Verificación Formal

Las criptomonedas y las finanzas descentralizadas (DeFi) ofrecen una nueva forma de manejar servicios bancarios y financieros, transformando el acceso y la gestión de estos servicios. Las blockchains sirven como la base para las criptomonedas, y los protocolos de consenso son cruciales para asegurar el acuerdo entre los procesos sobre el estado de la blockchain.

Los protocolos de consenso anteriores se basaban en entornos síncronos para garantizar seguridad y vitalidad. Recientemente, ha surgido un grupo de protocolos de consenso probabilísticos asíncronos que utilizan Grafos Acíclicos Dirigidos (DAG). Estos protocolos muestran un alto rendimiento con Tolerancia a Fallos Bizantinos (BFT), son justos con los procesos y mantienen una baja complejidad de comunicación. Varias blockchains líderes ahora dependen de protocolos basados en DAG para consenso.

Dado que grandes cantidades de dinero se mantienen en diferentes blockchains, manipular el Protocolo de Consenso puede convertirse en un objetivo de ataques. Por ejemplo, los ataques de doble gasto buscan abusar de protocolos inseguros encontrando entradas que llevan a estados inconsistentes, permitiendo que la misma moneda se gaste dos veces.

Aunque los protocolos de consenso están diseñados para ser seguros y mitigar tales ataques, el diseño informal del software dificulta probar la seguridad para todas las entradas. Las blockchains establecidas, a pesar de su reputación, no siempre pueden ser seguras.

Una forma estricta de asegurar la seguridad es usar verificación formal. Este método implica crear modelos matemáticos que describen el comportamiento del sistema y proporcionar prueba matemática de que el protocolo de consenso funciona correctamente para todas las entradas y configuraciones. Si bien algunos protocolos tienen tales pruebas, muchos se basan en suposiciones de seguridad sin respaldo formal. Esto se debe a la tediosa naturaleza de crear modelos formales, junto con la falta de bloques de construcción fáciles de usar para probar la corrección de nuevos protocolos.

Si bien reutilizar especificaciones es a menudo factible, el proceso de prueba generalmente requiere comenzar desde cero. Sin embargo, omitir modelado y pruebas de seguridad no es recomendable porque el número de interacciones posibles en entornos asíncronos es abrumador. Confiar únicamente en pruebas podría no exponer fallos en el diseño del protocolo, ya que comportamientos dañinos de procesos bizantinos pueden no ser completamente capturados por los casos de prueba. En general, las pruebas y la verificación de modelos tradicionales no garantizan la corrección para los procesos involucrados y sus configuraciones.

Este artículo presenta un estudio de caso del mundo real donde modelos verificados de protocolos de consenso guían el desarrollo. En nuestro estudio de caso, verificamos formalmente la seguridad de dos protocolos basados en DAG: DAG-Rider y Cordial Miners. Aunque estos protocolos funcionan bajo principios similares, las diferencias introducidas para mejorar el rendimiento pueden afectar la corrección. Por lo tanto, el desafío radica en crear especificaciones y pruebas que sean modulares y adaptables tanto para protocolos existentes como nuevos.

Para lograr eso, creamos especificaciones modulares que capturan los aspectos comunes de los protocolos a la vez que permiten la reutilización de pruebas. Este proceso implica seleccionar abstracciones adecuadas para los protocolos, lo que nos permite descomponer propiedades y pruebas en componentes más pequeños. Nuestro trabajo es un paso crucial hacia la producción de un conjunto de especificaciones y pruebas que puedan ser fácilmente reutilizadas, necesitando solo ajustes menores para diferentes protocolos basados en DAG.

Hemos hecho disponible públicamente una especificación formal y una prueba de código abierto para DAG-Rider y Cordial Miners. La especificación está escrita en la Lógica Temporal de Acciones (TLA+) y las pruebas se realizan utilizando el sistema de pruebas TLA+ (TLAPS), que verifica la corrección de las pruebas de manera eficiente.

#Resumen de Protocolos de Consenso Basados en DAG

Los protocolos de consenso basados en DAG abordan el problema de Difusión Atómica Bizantina (BAB), que implica ordenar bloques de mensajes (transacciones) en un entorno donde algunos procesos pueden actuar de manera maliciosa. Estos protocolos suponen una red de procesos donde un cierto número puede comportarse incorrectamente.

Los procesos pueden crear, firmar y enviar mensajes entre sí. Se asume que cada mensaje enviado desde un proceso correcto a otro será eventualmente recibido, y cada proceso puede producir mensajes de manera secuencial.

El objetivo principal de un protocolo de consenso basado en DAG es asegurar que las salidas cumplan con dos propiedades clave: seguridad y vitalidad. La seguridad significa que las secuencias de salidas de cualquier par de procesos correctos deben ser consistentes, lo que implica que una es un prefijo de la otra. La vitalidad requiere que cada mensaje enviado por un proceso correcto eventualmente sea producido por todos los procesos correctos con un alto grado de certeza.

En términos generales, es crucial formular el problema de consenso, especialmente para los lectores familiarizados con el consenso tradicional pero no con los conceptos de blockchain. El problema de consenso tiene como objetivo establecer un acuerdo común entre los procesos sobre las transacciones actuales y su orden.

Los protocolos de consenso basados en DAG están diseñados para gestionar procesos bizantinos hasta un cierto límite. Operan bajo la suposición de que algunos procesos ejecutan el protocolo de consenso mientras un número definido puede ser bizantino.

Las propiedades necesarias para los protocolos de consenso basados en DAG incluyen:

1. Seguridad: Las secuencias de salida de transacciones de todos los procesos correctos deben ser consistentes.
2. Vitalidad: Cada transacción enviada por un proceso correcto eventualmente será producida por todos los procesos correctos.

Para aclarar, la consistencia en la seguridad se basa en la idea de un prefijo para las secuencias de transacción. Dada una colección de secuencias, una es un prefijo de otra si representa el inicio de esa secuencia. Las salidas se consideran consistentes cuando una es un prefijo de la otra.

La construcción de protocolos basados en DAG ocurre en dos etapas: una fase de comunicación y una fase de ordenación.

#Fase de Comunicación

En esta fase, los procesos crean y comparten vértices dentro de rondas específicas. Un vértice incluye el ID del creador, un número de ronda, referencias a vértices de rondas anteriores y el bloque propuesto. Cada proceso construye su DAG local, que contiene sus vértices creados y los recibidos de otros.

Los bordes salientes en el DAG local conectan vértices a aquellos que referencian. Un vértice se añade a un DAG local una vez que sus referencias están presentes; de lo contrario, permanece en un búfer.

Se dice que un proceso ha completado una ronda cuando su DAG local contiene un número específico de vértices de esa ronda. Un proceso solo puede crear y compartir un vértice en la siguiente ronda después de terminar la ronda actual.

Cada DAG local organiza naturalmente los vértices en capas; los vértices de la ronda cero forman la capa inferior, y los de rondas superiores apuntan a los más bajos. Por lo tanto, cada DAG local describe un orden parcial sobre sus vértices. Es importante señalar que los DAG locales entre diferentes procesos no tienen que ser iguales o incluso seguir la misma estructura. Sin embargo, el protocolo asegura que si un vértice aparece en más de un DAG local, su historia causal es la misma en ambos.

#Fase de Ordenación

En la fase de ordenación, cada proceso tiene que ordenar completamente los vértices de su DAG local de forma independiente y sin más comunicación. El desafío radica en lograr un orden idéntico entre todos los procesos correctos.

Si los procesos pueden acordar ciertos vértices "ancla", pueden organizar los vértices no ordenados restantes según un procedimiento de ordenación topológica predefinido. Se anota el primer ancla, seguido de anclas adicionales. La diferencia en la historia causal entre estos anclajes puede ordenarse usando la ordenación acordada.

Dado que el protocolo es asíncrono y determinista, los anclajes deben elegirse de manera aleatoria. Cada proceso divide su DAG local en varias olas, lo que permite seleccionar un vértice líder aleatorio para cada ola utilizando una moneda perfecta global, que a menudo se implementa con firmas umbral.

El consenso sobre la secuencia de líderes de ola comprometidos (anclajes) es esencial para obtener un orden consistente de los vértices en los DAG. Los bloques representados por los vértices ordenados pueden ser producidos secuencialmente para asegurar la seguridad.

#Especificaciones y Pruebas Reutilizables

La arquitectura de las especificaciones y pruebas incorpora la creación de abstracciones para hacerlas modulares y reutilizables. El principal desafío es cómo representar el estado de la red, ya que los procesos pueden haber recibido diferentes conjuntos de mensajes que conducen a DAG locales únicos.

La abstracción del estado de la red almacena un DAG local para cada proceso. Cada DAG local se almacena como un arreglo bidimensional, representando los vértices creados por diferentes procesos en varias rondas. Algunas posiciones pueden estar vacías, indicando que un proceso no ha recibido comunicación de otros en esa ronda.

El objetivo es acordar un vértice representativo para cada posición en el DAG local. Esta tarea implica manejar tanto estrategias de comunicación confiables como no confiables.

En el caso de transmisiones confiables, puede existir como máximo un vértice en cualquier posición en el DAG local. Para transmisiones no confiables, puede haber múltiples vértices en una sola posición. Esto requiere técnicas para seleccionar un vértice representante único para cada posición.

Al abstraer la selección de vértices como un proceso de dos pasos, la especificación para los protocolos de consenso puede dividirse en secciones acompañantes. La especificación de comunicación incluye elementos de la fase de comunicación, mientras que la especificación de ordenación se centra en acordar las posiciones de líderes de ola comprometidos.

Para mantener una representación uniforme de la especificación de ordenación, simplificamos las representaciones de DAG locales para centrarnos únicamente en las posiciones de los líderes de ola. Cada ola tiene una posición de líder única, lo que resulta en la creación de un wave-DAG, donde los vértices reflejan solo los vértices líderes.

Los bordes en este wave-DAG muestran relaciones basadas en el protocolo de comunicación actual, ya sea el cierre transitivo de bordes fuertes para DAG-Rider o la relación de ratificación para Cordial Miners.

#Pruebas de Seguridad

La seguridad de las especificaciones está respaldada por varios teoremas e invariantes. Cada especificación tiene su propio conjunto de invariantes que deben ser establecidos y luego probados dentro del marco.

Para mantener la seguridad de las fases de ordenación y comunicación, invariantes específicos como LeaderConsistency y LeaderMonotonicity deben ser validados. LeaderConsistency asegura que las secuencias de líderes comprometidos de cualquier par de procesos correctos se alineen de manera consistente, mientras que LeaderMonotonicity requiere que los compromisos de ola sigan un orden específico e inmutable.

Cada invariante se prueba de manera independiente, y las dependencias entre ellas están estructuradas sistemáticamente. El proceso de prueba utiliza diversas estrategias que incluyen inducción, lo que permite asegurar que los invariantes se mantengan en todos los estados accesibles dentro de la fase de ordenación.

#Conclusión

El esfuerzo general para especificar y probar varios protocolos de consenso basados en DAG tomó una cantidad considerable de tiempo, pero cuando se modularizó, el tiempo necesario para especificar y probar el protocolo de Cordial Miners se redujo drásticamente. Esto significa que muchos otros protocolos podrían probablemente ser modelados y probados con un esfuerzo similarmente reducido.

La precisión introducida por las especificaciones y pruebas verificables por máquina requiere un enfoque más riguroso, asegurando que la implementación corresponda de cerca al modelo utilizado para la verificación formal. Estamos en el proceso de extender estas especificaciones y pruebas para apoyar protocolos basados en DAG mejorados basados en los conocimientos adquiridos a lo largo de las fases de especificación y prueba.

Los beneficios de este proceso de verificación formal son claros: no solo ayudan a asegurar la seguridad, sino que contribuyen a implementaciones más robustas y fiables de protocolos de consenso en diversas aplicaciones de blockchain.