Cimeira dos Académicos Web3 Foca na Segurança do Protocolo de Consenso e na Prova de Atividade

Na recente Cimeira de Académicos Web3 de 2025, um conhecido professor de ciência da computação apresentou uma palestra intitulada "Segurança e Prova de Atividade de Protocolo de Consenso Refinado: LiDO e sua Expansão", onde revelou pela primeira vez o modelo LiDO e a estrutura de expansão LiDO-DAG desenvolvidos pela sua equipe. Este resultado inovador visa fornecer provas de segurança e atividade verificáveis mecanicamente para protocolos de consenso de Tolerância a Falhas Bizantinas (BFT) complexos, estabelecendo uma base tecnológica para a confiabilidade e desenvolvimento em grande escala do ecossistema Web3.

Na palestra, o professor apontou que os protocolos de consenso existentes (como PBFT, Jolteon) são amplamente utilizados, mas devido à sua complexidade de implementação, muitas vezes escondem 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 por meio de 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 a validação eficiente de consenso sem líder.

Atualmente, o LiDO foi aplicado com sucesso em protocolos industriais como o Jolteon (BFT de duas fases) e vários protocolos DAG, completando a prova mecanizada de mais de 10.000 linhas de código Coq, com a quantidade de código de verificação de segurança e vivacidade alcançando 4.000 e 1.700 linhas, respectivamente. "Atualmente, os protocolos de consenso PoS enfrentam a dificuldade de garantir segurança, vivacidade e descentralização ao mesmo tempo," apontou o professor em sua palestra. "O modelo LiDO é uma proposta de design sistemático criada precisamente para romper essa dificuldade."

Este professor liderou uma equipe que desenvolveu o primeiro sistema operativo "sem falhas" do mundo através de verificação formal, sendo considerado um "marco na segurança de sistemas ciberfísicos". Esta conquista não apenas estabeleceu a base técnica da empresa de segurança que fundou, mas também destacou seu profundo conhecimento na área de segurança de sistemas. Nos últimos anos, o professor tem se aprofundado na segurança de blockchain, introduzindo a tecnologia de verificação formal na garantia de segurança de contratos inteligentes e protocolos em cadeia, protegendo a segurança de ativos criptográficos de bilhões de dólares.

A LiDO já completou o design do modelo e a verificação formal, e começou a explorar a possibilidade de integração com principais blockchains e protocolos descentralizados. O professor afirmou que estão empenhados em validar os mecanismos-chave no Web3.0 para fornecer produtos e serviços ao longo do ciclo, apoiando melhor a estratégia de desenvolvimento de longo prazo das empresas e ecossistemas Web3. No final da palestra, o professor enfatizou: "Um stack de protocolos de rede confiáveis, seguros e verificáveis será o caminho chave para um verdadeiro futuro descentralizado."