Destacados de la Cumbre de Académicos de Web3: Modelo de verificación de seguridad del nuevo protocolo de consenso presentado por primera vez

En la reciente Cumbre de Académicos Web3 2025, un profesor del departamento de ciencias de la computación de la Universidad de Yale dio una conferencia titulada "Pruebas de seguridad y vitalidad de protocolos de consenso refinados: LiDO y su marco de expansión", presentando por primera vez al público el modelo LiDO desarrollado por su equipo y el marco de expansión LiDO-DAG. Este logro innovador tiene como objetivo proporcionar pruebas de seguridad y vitalidad verificables mecánicamente para protocolos de consenso de tolerancia a fallos bizantinos (BFT) complejos, estableciendo una base técnica para el desarrollo de la fiabilidad y escalabilidad del ecosistema Web3.

En su discurso, el profesor señaló que, a pesar de que los protocolos de consenso existentes (como PBFT, Jolteon) se utilizan ampliamente, a menudo existen riesgos de seguridad potenciales debido a su alta complejidad de implementación. Para abordar este problema, el modelo LiDO propuso de manera innovadora un marco de verificación refinado en tres capas:

1. Capa de abstracción de seguridad: mapea el protocolo como una máquina de estados linealizada, asegurando la consistencia del registro (seguridad);
2. Capa de garantía activa: Introducción del mecanismo "Pacemaker" para resolver el problema de latencia de la red a través de la difusión de tiempo de espera y la sincronización de rondas;
3. Capa de expansión DAG: soporta protocolos DAG emergentes como Narwhal y Bullshark, logrando una verificación eficiente del consenso sin líder.

Actualmente, LiDO se ha aplicado con éxito en el protocolo industrial Jolteon (BFT de dos fases) y en varios protocolos DAG, completando más de 10,000 líneas de prueba mecánica de código Coq, en las que las líneas de código para la verificación de seguridad y actividad alcanzan respectivamente 4,000 y 1,700 líneas. El ponente enfatizó: "Actualmente, los protocolos de consenso PoS enfrentan la difícil situación de no poder lograr simultáneamente seguridad, actividad y descentralización. El modelo LiDO es un plan de diseño sistemático propuesto precisamente para romper esta limitación."

Este profesor lideró un equipo que desarrolló el primer sistema operativo "sin vulnerabilidades" del mundo a través de la verificación formal, CertiKOS, que ha sido aclamado como un "hito en la seguridad de sistemas ciberfísicos". Este logro no solo sentó las bases tecnológicas para la empresa de seguridad que fundó posteriormente, sino que también demostró su profunda acumulación en el campo de la seguridad de sistemas. En los últimos años, ha centrado su investigación en la seguridad de blockchain, dedicándose a aplicar la tecnología de verificación formal a la seguridad de contratos inteligentes y protocolos en cadena, proporcionando protección de seguridad para activos criptográficos de cientos de miles de millones.

LiDO ha completado el diseño del modelo y la verificación formal, y ha comenzado a explorar la posibilidad de integración con las principales cadenas de bloques públicas y protocolos descentralizados. El ponente indicó que están comprometidos con la validación de los mecanismos clave en Web3.0 para ofrecer productos y servicios de ciclo completo, apoyando mejor la estrategia de desarrollo a largo plazo de las empresas y ecosistemas de Web3. Al final de la charla, enfatizó: "Una pila de protocolos de red confiable, segura y verificable será el camino clave hacia un futuro verdaderamente descentralizado."