En la cumbre de académicos de Web3, el profesor Shao Zhong presentó el modelo LiDO, promoviendo la verificación de la seguridad del protocolo de consenso.
La Cumbre de Académicos Web3 de 2025 se celebró recientemente, y 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 vitalidad de los protocolos de consenso refinados: LiDO y su expansión". Por primera vez, presentó públicamente el modelo LiDO y el marco de expansión LiDO-DAG desarrollado por su equipo. Este logro revolucionario tiene como objetivo proporcionar pruebas de seguridad y vitalidad verificables mecánicamente para protocolos de consenso complejo de Tolerancia a Fallos Bizantinos (BFT), sentando las bases tecnológicas para la fiabilidad y el desarrollo a gran escala del ecosistema Web3.
El profesor Shao Zhong señaló en su discurso que los protocolos de consenso existentes como PBFT y Jolteon, aunque se aplican ampliamente, a menudo ocultan vulnerabilidades 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:
Capa de abstracción de seguridad: mapear el protocolo como una máquina de estados linealizada, asegurando la consistencia de los registros (seguridad);
Capa de garantía activa: Introducción del mecanismo "Pacemaker" para resolver el problema de latencia de red mediante la difusión por tiempo de espera y la sincronización de rondas;
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 múltiples protocolos DAG, completando más de diez mil 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 4000 líneas y 1700 líneas, respectivamente. El profesor Shao Zhong enfatiza: "En la actualidad, los protocolos de consenso PoS enfrentan generalmente la dificultad de no poder lograr simultáneamente seguridad, actividad y descentralización. El modelo LiDO es precisamente una propuesta de diseño sistemático para romper este cuello de botella."
Como principal investigador del sistema operativo CertiKOS, el primer sistema operativo "sin vulnerabilidades" verificado formalmente a nivel mundial, el profesor Zhao Zhong ha acumulado una profunda experiencia en el campo de la seguridad de sistemas. Este logro no solo ha sentado bases sólidas para su investigación posterior, sino que también resalta su contribución excepcional en el ámbito de la seguridad de sistemas. En los últimos años, el profesor Zhao Zhong ha cambiado su enfoque de investigación hacia la seguridad en blockchain y, en 2017, cofundó una empresa de seguridad con socios, dedicada a aplicar la tecnología de verificación formal a la seguridad de contratos inteligentes y protocolos en cadena, proporcionando protección de seguridad a activos criptográficos por un valor de cientos de miles de millones.
El modelo LiDO ha completado actualmente el diseño y la verificación formal, y ha comenzado a explorar la posibilidad de integración con las principales cadenas de bloques y los protocolos descentralizados. El profesor Shao Zhong afirmó 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 Web3. Al final de la presentación, el profesor Shao Zhong enfatizó: "Una pila de protocolos de red confiable, segura y verificable será el camino clave hacia un futuro verdaderamente descentralizado."
This page may contain third-party content, which is provided for information purposes only (not representations/warranties) and should not be considered as an endorsement of its views by Gate, nor as financial or professional advice. See Disclaimer for details.
12 me gusta
Recompensa
12
7
Compartir
Comentar
0/400
CountdownToBroke
· hace1h
¿Quién entiende este tipo de cosas tan sofisticadas...?
Ver originalesResponder0
HodlOrRegret
· 07-06 18:32
Finalmente alguien ha atacado la capa de consenso.
Ver originalesResponder0
StablecoinAnxiety
· 07-05 23:32
¡El protocolo PoS ha sido salvado una vez más!!!
Ver originalesResponder0
DarkPoolWatcher
· 07-05 23:31
Tener solo teoría sin implementación es igual a cero.
El profesor Shao Zhong publicó el modelo LiDO para impulsar la verificación de la seguridad del protocolo de consenso de Web3.
En la cumbre de académicos de Web3, el profesor Shao Zhong presentó el modelo LiDO, promoviendo la verificación de la seguridad del protocolo de consenso.
La Cumbre de Académicos Web3 de 2025 se celebró recientemente, y 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 vitalidad de los protocolos de consenso refinados: LiDO y su expansión". Por primera vez, presentó públicamente el modelo LiDO y el marco de expansión LiDO-DAG desarrollado por su equipo. Este logro revolucionario tiene como objetivo proporcionar pruebas de seguridad y vitalidad verificables mecánicamente para protocolos de consenso complejo de Tolerancia a Fallos Bizantinos (BFT), sentando las bases tecnológicas para la fiabilidad y el desarrollo a gran escala del ecosistema Web3.
El profesor Shao Zhong señaló en su discurso que los protocolos de consenso existentes como PBFT y Jolteon, aunque se aplican ampliamente, a menudo ocultan vulnerabilidades 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:
Actualmente, LiDO se ha aplicado con éxito en el protocolo industrial Jolteon (BFT de dos fases) y en múltiples protocolos DAG, completando más de diez mil 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 4000 líneas y 1700 líneas, respectivamente. El profesor Shao Zhong enfatiza: "En la actualidad, los protocolos de consenso PoS enfrentan generalmente la dificultad de no poder lograr simultáneamente seguridad, actividad y descentralización. El modelo LiDO es precisamente una propuesta de diseño sistemático para romper este cuello de botella."
Como principal investigador del sistema operativo CertiKOS, el primer sistema operativo "sin vulnerabilidades" verificado formalmente a nivel mundial, el profesor Zhao Zhong ha acumulado una profunda experiencia en el campo de la seguridad de sistemas. Este logro no solo ha sentado bases sólidas para su investigación posterior, sino que también resalta su contribución excepcional en el ámbito de la seguridad de sistemas. En los últimos años, el profesor Zhao Zhong ha cambiado su enfoque de investigación hacia la seguridad en blockchain y, en 2017, cofundó una empresa de seguridad con socios, dedicada a aplicar la tecnología de verificación formal a la seguridad de contratos inteligentes y protocolos en cadena, proporcionando protección de seguridad a activos criptográficos por un valor de cientos de miles de millones.
El modelo LiDO ha completado actualmente el diseño y la verificación formal, y ha comenzado a explorar la posibilidad de integración con las principales cadenas de bloques y los protocolos descentralizados. El profesor Shao Zhong afirmó 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 Web3. Al final de la presentación, el profesor Shao Zhong enfatizó: "Una pila de protocolos de red confiable, segura y verificable será el camino clave hacia un futuro verdaderamente descentralizado."