Destaques da Cúpula de Acadêmicos Web3: Modelo de Verificação de Segurança de Novo Protocolo de Consenso Revelado pela Primeira Vez

No recente Cimeira de Académicos Web3 de 2025, um professor do Departamento de Ciência da Computação da Universidade de Yale fez uma apresentação intitulada "Segurança e Prova de Atividade de Protocolos de Consenso Refinados: LiDO e sua Extensão", apresentando ao público pela primeira vez o modelo LiDO e a estrutura de extensão LiDO-DAG desenvolvidos por sua equipe. Este resultado inovador visa fornecer segurança e prova de atividade verificáveis mecanicamente para protocolos de consenso tolerantes a falhas bizantinas (BFT) complexos, estabelecendo uma base técnica para o desenvolvimento da fiabilidade e escalabilidade do ecossistema Web3.

Na palestra, o professor apontou que, apesar de os protocolos de consenso existentes (como PBFT, Jolteon) serem amplamente utilizados, devido à alta complexidade de implementação, frequentemente existem potenciais riscos de segurança. 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 Ativa: Introdução do mecanismo "Pacemaker", que resolve o problema de latência na rede através da difusão de tempo limite e sincronização de rodadas;
3. Camada de expansão DAG: suporta protocolos DAG emergentes como Narwhal e Bullshark, permitindo uma 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 mecanizadas de código Coq, onde a quantidade de código para validação de segurança e atividade atingiu respectivamente 4.000 linhas e 1.700 linhas. O palestrante enfatizou: "Atualmente, os protocolos de consenso PoS enfrentam geralmente a difícil situação de não conseguir segurança, atividade e descentralização simultaneamente. O modelo LiDO é uma proposta de design sistêmico para superar essa limitação."

Este professor liderou uma equipe que desenvolveu o primeiro sistema operacional "sem falhas" CertiKOS, verificado formalmente, sendo considerado um "marco na segurança de sistemas ciber-físicos". Esta conquista não apenas lançou as bases tecnológicas para a empresa de segurança que ele fundou posteriormente, mas também demonstrou seu profundo acúmulo na área de segurança de sistemas. Nos últimos anos, ele tem direcionado sua pesquisa para a segurança de blockchain, dedicando-se a aplicar técnicas de verificação formal na segurança de contratos inteligentes e protocolos em cadeia, proporcionando proteção de segurança para ativos criptográficos de centenas de bilhões de dólares.

LiDO já completou o design do modelo e a verificação formal, e começou a explorar a possibilidade de integração com cadeias públicas mainstream e protocolos descentralizados. O palestrante afirmou que estão dedicados a validar os mecanismos-chave no Web3.0, a fim de 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, ele enfatizou: "Uma pilha de protocolos de rede confiável, segura e verificável será o caminho chave para um futuro verdadeiramente descentralizado."