Cimeira de Académicos Web3: Professor da Universidade de Yale apresenta publicamente o modelo LiDO pela primeira vez

Na recente Cúpula de Acadêmicos Web3 de 2025, o Professor Shao Zhong do Departamento de Ciência da Computação da Universidade de Yale proferiu uma palestra intitulada "Prova de Segurança e Atividade de Protocolos de Consenso Refinados: LiDO e sua Expansão", apresentando ao público pela primeira vez o modelo LiDO desenvolvido por sua equipe e a estrutura de expansão LiDO-DAG. Este resultado inovador visa fornecer provas de segurança e atividade verificáveis mecanicamente para protocolos de consenso tolerantes a falhas bizantinas (BFT) complexos, estabelecendo uma base técnica importante para a confiabilidade e o desenvolvimento em escala do ecossistema Web3.

O professor Shao Zhong destacou em sua palestra que, embora os protocolos de consenso existentes (como PBFT, Jolteon) tenham sido amplamente aplicados, sua complexidade de implementação muitas vezes resulta em potenciais vulnerabilidades de segurança. Para resolver esse problema, o modelo LiDO propôs uma estrutura de verificação refinada em três camadas inovadora:

1. Camada de abstração de segurança: mapeia o protocolo como uma máquina de estados linearizada, garantindo a consistência dos logs para assegurar a segurança;
2. Camada de Garantia Ativa: Introdução do mecanismo "Pacemaker" para resolver problemas de latência de rede através de difusão de tempo limite e sincronização de rondas;
3. Camada de extensão DAG: suporta protocolos DAG emergentes como Narwhal e Bullshark, permitindo uma verificação eficiente de consenso sem líderes.

Atualmente, o LiDO foi aplicado com sucesso no protocolo industrial Jolteon (BFT de duas fases) e em vários protocolos DAG, completando mais de dez mil linhas de provas mecanizadas em Coq, onde a quantidade de código para verificação de segurança e vivacidade alcançou respectivamente 4000 linhas e 1700 linhas. O Professor Shao Zhong enfatizou em sua palestra: "Atualmente, os protocolos de consenso PoS enfrentam amplamente a dificuldade de garantir segurança, vivacidade e descentralização simultaneamente. O modelo LiDO foi proposto como uma solução de design sistemático para superar essa limitação."

Vale a pena mencionar que o sistema CertiKOS, desenvolvido anteriormente pela equipe liderada pelo Professor Shao Zhong, é o primeiro sistema operacional "sem falhas" do mundo a ser validado formalmente, sendo considerado um "marco na segurança de sistemas ciberfísicos". Esta conquista não só demonstra a profunda acumulação de conhecimentos da sua equipe na área de segurança de sistemas, mas também estabelece uma base sólida para pesquisas futuras em segurança de blockchain.

O modelo LiDO foi atualmente projetado e verificado formalmente, e começou a explorar a possibilidade de integração com as principais blockchains e protocolos descentralizados. O Professor Shao Zhong afirmou que estão empenhados em validar os mecanismos-chave da Web3.0, a fim de fornecer produtos e serviços de ciclo completo, melhorando o suporte às estratégias de desenvolvimento a longo prazo das empresas e ecossistemas Web3.

No final da palestra, o Professor Shao Zhong enfatizou: "Um stack de protocolos de rede confiável, seguro e verificável será o caminho chave para um futuro verdadeiramente descentralizado." Esta visão destaca o papel importante do modelo LiDO no avanço da tecnologia Web3, proporcionando novas ideias e métodos para a segurança e confiabilidade dos sistemas descentralizados no futuro.