Cimeira de Académicos Web3: Professor de Yale revela modelo LiDO, ajudando a melhorar a segurança do protocolo de consenso

Na cimeira de académicos Web3 de 2025, o professor Shao Zhong do Departamento de Ciência da Computação da Universidade de Yale fez uma apresentação intitulada "Prova de segurança e atividade de protocolos de consenso refinados: LiDO e sua extensão", onde apresentou pela primeira vez o modelo LiDO desenvolvido pela sua equipe e a estrutura de extensão LiDO-DAG. Este resultado inovador visa fornecer provas de segurança e atividade mecanicamente verificáveis para protocolos de consenso de tolerância a falhas bizantinas (BFT) complexos, estabelecendo uma base técnica para o desenvolvimento da fiabilidade e escalabilidade do ecossistema Web3.

O Professor Shao Zhong apontou em sua palestra que, embora os protocolos de consenso existentes (como PBFT, Jolteon) sejam amplamente utilizados, devido à sua complexidade de implementação, frequentemente existem vulnerabilidades de segurança potenciais. 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 (segurança).
2. Camada de garantia de atividade: Introduz o mecanismo "Pacemaker" para resolver o problema de latência da rede através de transmissão em atraso e sincronização de rodadas.
3. Camada de expansão DAG: suporta novos protocolos DAG emergentes como Narwhal e Bullshark, permitindo a validação eficiente do 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 10.000 linhas de provas mecânicas de código Coq, nas quais a quantidade de código para verificação de segurança e de vitalidade atingiu, respectivamente, 4.000 linhas e 1.700 linhas. O professor Shao Zhong enfatizou em sua palestra: "Atualmente, os protocolos de consenso PoS enfrentam amplamente a dificuldade de alcançar segurança, vitalidade e descentralização ao mesmo tempo. O modelo LiDO é uma proposta de design sistemático para quebrar esse impasse."

Vale a pena mencionar que o Professor Shao Zhong liderou anteriormente uma equipe que desenvolveu o CertiKOS, o primeiro sistema operacional "sem falhas" do mundo que passou por verificação formal, sendo considerado um "marco na segurança de sistemas ciberfísicos". Esta conquista não só consolidou seu profundo conhecimento na área de segurança de sistemas, mas também forneceu uma base sólida para pesquisas futuras na segurança de blockchain. Em 2017, o Professor Shao Zhong, juntamente com seu aluno, o Professor Gu Ronghui, introduziram a tecnologia de verificação formal na área de segurança de contratos inteligentes e protocolos em cadeia, proporcionando proteção de segurança para ativos criptográficos no valor de bilhões de dólares.

O modelo LiDO já completou o design e a verificação formal, e está explorando a possibilidade de integração com as principais blockchains públicas e protocolos descentralizados. O professor Shao Zhong afirmou que eles estão empenhados em validar os mecanismos-chave no Web3.0, para fornecer produtos e serviços de ciclo completo, apoiando melhor a estratégia de desenvolvimento a longo prazo das empresas e ecossistemas Web3.

No final da palestra, o professor Shao Zhong enfatizou: "Um protocolo de rede confiável, seguro e verificável será o caminho chave para um verdadeiro futuro descentralizado." Esta opinião destaca a importância do modelo LiDO no avanço da tecnologia Web3 e na garantia de segurança.