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

Na Cimeira dos Académicos de Web3 de 2025, o professor Shao Zhong do Departamento de Ciências da Computação da Universidade de Yale fez uma palestra intitulada "Prova de Segurança e Atividade de Protocolos de Consenso Refinados: LiDO e suas Extensões", apresentando ao público pela primeira vez o modelo LiDO desenvolvido por sua equipe e a estrutura de extensã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 para a fiabilidade e o desenvolvimento em larga escala do ecossistema Web3.

O Professor Shao Zhong destacou em sua palestra que, embora os protocolos de consenso existentes (como PBFT, Jolteon) sejam amplamente utilizados, sua alta 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 Ativa: Introduz o mecanismo "Pacemaker" para resolver problemas de latência na rede através da transmissão de tempo limite e sincronização de rodadas.
3. Camada de extensão DAG: suporta novos protocolos DAG como Narwhal, Bullshark, permitindo uma validação eficiente de 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 provas mecanizadas em Coq, das quais as linhas de código para verificação de segurança e atividade atingem 4000 e 1700 linhas, respectivamente. O professor Shao Zhong enfatizou em sua apresentação: "Atualmente, os protocolos de consenso PoS enfrentam a dificuldade de garantir simultaneamente segurança, atividade e descentralização. O modelo LiDO foi proposto como uma solução de design sistemático para superar essa dificuldade."

A equipe liderada pelo Professor Shao Zhong desenvolveu o CertiKOS, o primeiro sistema operacional "sem vulnerabilidades" do mundo validado formalmente, considerado um "marco na segurança de sistemas ciberfísicos". Essa conquista não apenas estabeleceu as bases para as tecnologias relacionadas, mas também demonstrou a profunda acumulação do time na área de segurança de sistemas. Nos últimos anos, o Professor Shao Zhong se aprofundou na pesquisa de segurança em blockchain e, em 2017, co-fundou uma empresa de segurança com colegas, introduzindo a tecnologia de validação formal na segurança de contratos inteligentes e protocolos on-chain, proporcionando proteção de segurança para ativos criptográficos avaliados em 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 as principais blockchains e protocolos descentralizados. O professor Shao Zhong afirmou que estão dedicados a validar 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 de 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."