Cumbre de académicos de Web3: El profesor de la Universidad de Yale presenta por primera vez el modelo LiDO

En la reciente cumbre de académicos Web3 2025, el profesor Shao Zhong del departamento de ciencias de la computación de la Universidad de Yale pronunció un discurso titulado "Prueba de seguridad y actividad 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 actividad verificables mecánicamente para protocolos de consenso tolerantes a fallos bizantinos (BFT) complejos, estableciendo una base técnica importante para la fiabilidad y el desarrollo escalable del ecosistema Web3.

El profesor Shao Zhong señaló en su discurso que, a pesar de que los protocolos de consenso existentes (como PBFT, Jolteon) se han aplicado ampliamente, a menudo existen vulnerabilidades de seguridad potenciales debido a la complejidad de su implementación. Para abordar este problema, el modelo LiDO propuso un innovador marco de verificación refinada en tres capas:

1. Capa de abstracción de seguridad: mapea el protocolo como una máquina de estados linealizada, asegurando la consistencia de los registros para garantizar la seguridad;
2. Capa de garantía activa: Introducción del mecanismo "Pacemaker", que resuelve el problema de la latencia de la red mediante 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 sin consenso de 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 diez mil líneas de pruebas mecánicas de código Coq, donde la cantidad de código para la verificación de seguridad y actividad alcanza las 4000 y 1700 líneas, respectivamente. El profesor Shao Zhong enfatizó en su discurso: "En la actualidad, los protocolos de consenso PoS enfrentan generalmente la dificultad de lograr seguridad, actividad y descentralización al mismo tiempo. El modelo LiDO es una solución de diseño sistémico propuesta precisamente para superar esta limitación."

Cabe mencionar que el sistema CertiKOS, desarrollado anteriormente por el equipo liderado por el profesor Shao Zhong, es el primer "sistema operativo sin vulnerabilidades" del mundo que ha sido verificado formalmente, y ha sido aclamado como un "hito en la seguridad de los sistemas ciberfísicos". Este logro no solo demuestra la profunda acumulación de su equipo en el campo de la seguridad de sistemas, sino que también sienta una base sólida para la investigación futura en seguridad de blockchain.

El modelo LiDO ha completado actualmente su diseño y verificación formal, y ha comenzado a explorar la posibilidad de integración con cadenas de bloques públicas y protocolos descentralizados de corriente principal. El profesor Shao Zhong ha declarado que están comprometidos con la verificación de los mecanismos clave en Web3.0, para proporcionar productos y servicios a lo largo de todo el ciclo, apoyando mejor la estrategia de desarrollo a largo plazo de las empresas y ecosistemas de Web3.

Al final de la conferencia, el profesor Shao Zhong enfatizó: "Un conjunto de protocolos de red confiables, seguros y verificables será el camino clave hacia un futuro verdaderamente descentralizado." Esta perspectiva destaca el papel importante del modelo LiDO en el impulso del desarrollo de la tecnología Web3, proporcionando nuevas ideas y métodos para la seguridad y confiabilidad de los sistemas descentralizados en el futuro.