El 8 de abril, durante la Conferencia de Académicos Web3 2025 celebrada en Hong Kong, el profesor del Departamento de Ciencias de la Computación de la Universidad de Yale y cofundador de CertiK, Zhao Zhong, pronunció una conferencia titulada "Seguridad y prueba de actividad de protocolos de consenso refinados: LiDO y su extensión", donde presentó por primera vez el modelo LiDO desarrollado por su equipo y el marco de extensión LiDO-DAG. Este logro revolucionario tiene como objetivo proporcionar pruebas de seguridad y actividad verificables mecánicamente para protocolos de consenso complejos de Tolerancia Byzantine a fallos (BFT), sentando así las bases tecnológicas para la fiabilidad y el desarrollo a gran escala del ecosistema Web3.
En esta charla, el profesor Shao Zhong señaló que, aunque los protocolos de consenso existentes (como PBFT y Jolteon) se utilizan ampliamente, a menudo ocultan vulnerabilidades potenciales debido a su compleja implementación. Para resolver este problema, el modelo LiDO propone de forma innovadora un marco de verificación detallado de tres capas:
Capa de abstracción de seguridad: Mapea el protocolo a una máquina de estados linealizada, asegurando la consistencia de los registros (seguridad);
Capa de garantía activa: Introduce el mecanismo "Pacemaker" para resolver el problema de la latencia en la red a través de la difusión de 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 de consenso sin líder.
Actualmente, LiDO se ha aplicado con éxito en el protocolo industrial Jolteon (BFT de dos etapas) y en múltiples protocolos DAG, completando la mecanización de más de diez mil líneas de código Coq, con una verificación de seguridad y actividad de 4000 y 1700 líneas, respectivamente. "Actualmente, los protocolos de consenso PoS enfrentan el dilema de no poder lograr simultáneamente seguridad, actividad y descentralización", señaló el profesor Shao Zhong en su discurso. "El modelo LiDO es un plan de diseño sistémico propuesto precisamente para romper este dilema."
El CertiKOS, desarrollado por el profesor Shao Zhong y su equipo, 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 establece las bases tecnológicas de la empresa de seguridad CertiK, sino que también destaca su profunda acumulación en el campo de la seguridad de sistemas. En los últimos años, el profesor Shao Zhong ha estado profundamente involucrado en la seguridad de blockchain, y en 2017 cofundó CertiK con su alumno, el profesor Gu Ronghui, introduciendo la tecnología de verificación formal en la seguridad de contratos inteligentes y protocolos en cadena, protegiendo así la seguridad de activos criptográficos por valor de miles de millones de dólares.
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 públicas y protocolos descentralizados. El profesor Shao Zhong dijo que CertiK se compromete a verificar los mecanismos clave de la Web3.0 para proporcionar productos y servicios de ciclo completo que apoyen mejor las estrategias de desarrollo a largo plazo de las empresas y los ecosistemas de la Web3. Al final del discurso, el profesor Shao Zhong enfatizó: "Una pila de protocolos de red confiable, segura y verificable será el camino clave hacia un futuro verdaderamente descentralizado. ”
El contenido es solo de referencia, no una solicitud u oferta. No se proporciona asesoramiento fiscal, legal ni de inversión. Consulte el Descargo de responsabilidad para obtener más información sobre los riesgos.
El cofundador de CertiK, el profesor Shao Zhong, asistió a la Cumbre de Académicos de Web3 y presentó públicamente el modelo LiDO por primera vez.
El 8 de abril, durante la Conferencia de Académicos Web3 2025 celebrada en Hong Kong, el profesor del Departamento de Ciencias de la Computación de la Universidad de Yale y cofundador de CertiK, Zhao Zhong, pronunció una conferencia titulada "Seguridad y prueba de actividad de protocolos de consenso refinados: LiDO y su extensión", donde presentó por primera vez el modelo LiDO desarrollado por su equipo y el marco de extensión LiDO-DAG. Este logro revolucionario tiene como objetivo proporcionar pruebas de seguridad y actividad verificables mecánicamente para protocolos de consenso complejos de Tolerancia Byzantine a fallos (BFT), sentando así las bases tecnológicas para la fiabilidad y el desarrollo a gran escala del ecosistema Web3.
En esta charla, el profesor Shao Zhong señaló que, aunque los protocolos de consenso existentes (como PBFT y Jolteon) se utilizan ampliamente, a menudo ocultan vulnerabilidades potenciales debido a su compleja implementación. Para resolver este problema, el modelo LiDO propone de forma innovadora un marco de verificación detallado de tres capas:
Capa de abstracción de seguridad: Mapea el protocolo a una máquina de estados linealizada, asegurando la consistencia de los registros (seguridad);
Capa de garantía activa: Introduce el mecanismo "Pacemaker" para resolver el problema de la latencia en la red a través de la difusión de 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 de consenso sin líder.
Actualmente, LiDO se ha aplicado con éxito en el protocolo industrial Jolteon (BFT de dos etapas) y en múltiples protocolos DAG, completando la mecanización de más de diez mil líneas de código Coq, con una verificación de seguridad y actividad de 4000 y 1700 líneas, respectivamente. "Actualmente, los protocolos de consenso PoS enfrentan el dilema de no poder lograr simultáneamente seguridad, actividad y descentralización", señaló el profesor Shao Zhong en su discurso. "El modelo LiDO es un plan de diseño sistémico propuesto precisamente para romper este dilema."
El CertiKOS, desarrollado por el profesor Shao Zhong y su equipo, 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 establece las bases tecnológicas de la empresa de seguridad CertiK, sino que también destaca su profunda acumulación en el campo de la seguridad de sistemas. En los últimos años, el profesor Shao Zhong ha estado profundamente involucrado en la seguridad de blockchain, y en 2017 cofundó CertiK con su alumno, el profesor Gu Ronghui, introduciendo la tecnología de verificación formal en la seguridad de contratos inteligentes y protocolos en cadena, protegiendo así la seguridad de activos criptográficos por valor de miles de millones de dólares.
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 públicas y protocolos descentralizados. El profesor Shao Zhong dijo que CertiK se compromete a verificar los mecanismos clave de la Web3.0 para proporcionar productos y servicios de ciclo completo que apoyen mejor las estrategias de desarrollo a largo plazo de las empresas y los ecosistemas de la Web3. Al final del discurso, el profesor Shao Zhong enfatizó: "Una pila de protocolos de red confiable, segura y verificable será el camino clave hacia un futuro verdaderamente descentralizado. ”