Cumbre de académicos de Web3: El profesor de Yale revela el modelo LiDO, ayudando a mejorar la seguridad del protocolo de consenso

En la Cumbre de Académicos de Web3 de 2025, el profesor Shao Zhong del Departamento de Ciencias de la Computación de la Universidad de Yale pronunció una conferencia titulada "Prueba de Seguridad y Actividad del Protocolo de Consenso Refinado: LiDO y su Extensión", donde presentó por primera vez el modelo LiDO y el marco de extensión LiDO-DAG desarrollado por su equipo. Este innovador logro tiene como objetivo proporcionar pruebas de seguridad y actividad verificables mecánicamente para protocolos de consenso tolerantes a fallos bizantinos (BFT) complejos, sentando la base técnica para el desarrollo de la fiabilidad y escalabilidad 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 utilizan 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 (seguridad).
2. Capa de garantía activa: se introduce el mecanismo "Pacemaker" para resolver el problema de la 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íderes.

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 código Coq con pruebas mecanizadas, donde la cantidad de código para la verificación de seguridad y actividad alcanza las 4,000 y 1,700 líneas, respectivamente. El profesor Shao Zhong enfatizó en su discurso: "Actualmente, los protocolos de consenso PoS enfrentan la difícil situación de lograr simultáneamente seguridad, actividad y descentralización. El modelo LiDO es precisamente una propuesta de diseño sistemático para romper este dilema."

Cabe mencionar que el profesor Shao Zhong lideró anteriormente un equipo que desarrolló CertiKOS, el primer sistema operativo "sin vulnerabilidades" del mundo validado formalmente, el cual ha sido aclamado como un "hito en la seguridad de los sistemas ciberfísicos". Este logro no solo consolida su profunda acumulación en el campo de la seguridad de sistemas, sino que también proporciona una base sólida para la investigación futura en seguridad blockchain. En 2017, el profesor Shao Zhong y su estudiante, el profesor Gu Ronghui, introdujeron conjuntamente la tecnología de verificación formal en el ámbito de la seguridad de contratos inteligentes y protocolos en la cadena, proporcionando protección de seguridad para activos criptográficos de miles de millones de dólares.

El modelo LiDO ha completado actualmente su diseño y verificación formal, y está explorando la posibilidad de integración con cadenas de bloques públicas principales y protocolos descentralizados. El profesor Shao Zhong declaró que están comprometidos a validar los mecanismos clave en Web3.0 para proporcionar 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 conferencia, el profesor Shao Zhong enfatizó: "Una pila de protocolos de red confiable, segura y verificable será la clave para un futuro verdaderamente descentralizado." Este punto de vista destaca la importancia del modelo LiDO en la promoción del desarrollo de la tecnología Web3 y la garantía de seguridad.