Cimeira de Académicos Web3 Foca na Nova Estrutura de Verificação de Segurança do Protocolo de Consenso

Na recente Cimeira 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 Protocolo de Consenso Refinado: LiDO e suas Expansões", onde apresentou pela primeira vez o modelo LiDO e a estrutura de expansão LiDO-DAG desenvolvidos por sua equipe. Este resultado inovador visa fornecer provas de segurança e atividade que possam ser verificadas mecanicamente para protocolos de consenso de Tolerância a Falhas Bizantinas (BFT), estabelecendo uma base técnica sólida para a fiabilidade e desenvolvimento em larga escala do ecossistema Web3.

O Professor Shao Zhong, durante sua palestra, destacou que, apesar dos protocolos de consenso existentes (como PBFT, Jolteon) serem amplamente utilizados, a complexidade de implementação muitas vezes oculta vulnerabilidades potenciais. Para resolver esse problema, o modelo LiDO propôs de forma inovadora uma estrutura de verificação refinada em três camadas:

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", que resolve o problema de latência da rede através de broadcast de tempo limite e sincronização de rondas;
3. Camada de extensão DAG: suporta protocolos DAG emergentes como Narwhal e Bullshark, permitindo uma validação eficiente do consenso sem líder.

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 prova mecânica de código Coq, onde a quantidade de código de verificação de segurança e de vivacidade atingiu 4000 linhas e 1700 linhas, respectivamente. O Professor Shao Zhong enfatizou: "Atualmente, os protocolos de consenso PoS enfrentam geralmente a dificuldade de equilibrar segurança, vivacidade e descentralização. O modelo LiDO foi proposto como uma solução de design sistêmico para romper esse gargalo."

Como líder de pesquisa no desenvolvimento do CertiKOS, o primeiro sistema operacional "sem falhas" validado formalmente no mundo, o Professor Shao Zhong e sua equipe acumularam uma profunda competência técnica na área de segurança de sistemas. Este feito não apenas estabeleceu uma base sólida para suas pesquisas subsequentes, mas também demonstrou suas contribuições extraordinárias no campo da segurança de sistemas. Nos últimos anos, o Professor Shao Zhong direcionou seu foco de pesquisa para a segurança de blockchain, dedicando-se a aplicar tecnologias de validação formal na proteção de segurança de contratos inteligentes e protocolos em cadeia, proporcionando segurança para ativos criptográficos no valor de bilhões de dólares.

O modelo LiDO foi projetado e validado formalmente, e começou a explorar a possibilidade de integração com as principais blockchains e protocolos descentralizados. O professor Shaozhong afirmou que eles estão dedicados a validar 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. Ao final da palestra, o professor Shaozhong enfatizou: "Uma pilha de protocolos de rede confiável, segura e verificável será o caminho chave para um verdadeiro futuro descentralizado."