No cimeira dos académicos de Web3, o professor de Yale revelou pela primeira vez o modelo LiDO
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 fez uma apresentação intitulada "Segurança e prova de atividade de protocolos de consenso refinados: LiDO e sua extensão", onde apresentou 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 de tolerância a falhas bizantinas complexos (BFT), estabelecendo uma base técnica para a confiabilidade e desenvolvimento em larga escala do ecossistema Web3.
O professor Shao Zhong apontou em sua palestra 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:
Camada de abstração de segurança: mapeia o protocolo para uma máquina de estados linearizada, garantindo a consistência dos logs (segurança);
Camada de Garantia de Atividade: Introduz o mecanismo "Pacemaker" para resolver o problema de latência da rede através da difusão de tempo limite e sincronização de rodadas;
Camada de extensão DAG: suporta protocolos DAG emergentes como Narwhal e Bullshark, realizando validação eficiente sem liderança.
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 código Coq com prova mecanizada, sendo que a quantidade de código para verificação de segurança e atividade atinge respectivamente 4000 linhas e 1700 linhas. O Professor Shao Zhong enfatizou em sua palestra: "Atualmente, os protocolos de consenso PoS enfrentam universalmente a dificuldade de equilibrar segurança, atividade e descentralização. O modelo LiDO é uma solução sistemática proposta para superar esse gargalo."
Vale a pena mencionar que o Professor Shao Zhong liderou uma equipe que desenvolveu o primeiro sistema operacional "sem vulnerabilidades" do mundo, CertiKOS, através de validação formal, sendo elogiado pela indústria como um "marco na segurança de sistemas ciberfísicos". Essa conquista não apenas demonstra a profunda acumulação de conhecimento da sua equipe na área de segurança de sistemas, mas também estabelece uma base sólida para pesquisas futuras. Nos últimos anos, o Professor Shao Zhong mudou seu foco de pesquisa para a segurança de blockchain e, em 2017, co-fundou uma empresa de segurança em blockchain com parceiros, dedicada a aplicar 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.
O modelo LiDO já foi completado em termos de design e verificação formal, e começou a explorar a possibilidade de integração com blockchains principais e protocolos descentralizados. O professor Shao Zhong afirmou que estão dedicados a verificar os mecanismos-chave no Web3.0, a fim de fornecer produtos e serviços de ciclo completo, apoiando melhor as estratégias de desenvolvimento a longo prazo de empresas e ecossistemas Web3. No final da palestra, o professor Shao Zhong enfatizou: "Construir uma pilha de protocolos de rede confiável, segura e verificável será o caminho chave para um futuro verdadeiramente descentralizado."
Esta página pode conter conteúdos de terceiros, que são fornecidos apenas para fins informativos (sem representações/garantias) e não devem ser considerados como uma aprovação dos seus pontos de vista pela Gate, nem como aconselhamento financeiro ou profissional. Consulte a Declaração de exoneração de responsabilidade para obter mais informações.
Professor da Yale revela LiDO: superando o gargalo da verificação de segurança do consenso protocolo
No cimeira dos académicos de Web3, o professor de Yale revelou pela primeira vez o modelo LiDO
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 fez uma apresentação intitulada "Segurança e prova de atividade de protocolos de consenso refinados: LiDO e sua extensão", onde apresentou 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 de tolerância a falhas bizantinas complexos (BFT), estabelecendo uma base técnica para a confiabilidade e desenvolvimento em larga escala do ecossistema Web3.
O professor Shao Zhong apontou em sua palestra 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:
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 código Coq com prova mecanizada, sendo que a quantidade de código para verificação de segurança e atividade atinge respectivamente 4000 linhas e 1700 linhas. O Professor Shao Zhong enfatizou em sua palestra: "Atualmente, os protocolos de consenso PoS enfrentam universalmente a dificuldade de equilibrar segurança, atividade e descentralização. O modelo LiDO é uma solução sistemática proposta para superar esse gargalo."
Vale a pena mencionar que o Professor Shao Zhong liderou uma equipe que desenvolveu o primeiro sistema operacional "sem vulnerabilidades" do mundo, CertiKOS, através de validação formal, sendo elogiado pela indústria como um "marco na segurança de sistemas ciberfísicos". Essa conquista não apenas demonstra a profunda acumulação de conhecimento da sua equipe na área de segurança de sistemas, mas também estabelece uma base sólida para pesquisas futuras. Nos últimos anos, o Professor Shao Zhong mudou seu foco de pesquisa para a segurança de blockchain e, em 2017, co-fundou uma empresa de segurança em blockchain com parceiros, dedicada a aplicar 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.
O modelo LiDO já foi completado em termos de design e verificação formal, e começou a explorar a possibilidade de integração com blockchains principais e protocolos descentralizados. O professor Shao Zhong afirmou que estão dedicados a verificar os mecanismos-chave no Web3.0, a fim de fornecer produtos e serviços de ciclo completo, apoiando melhor as estratégias de desenvolvimento a longo prazo de empresas e ecossistemas Web3. No final da palestra, o professor Shao Zhong enfatizou: "Construir uma pilha de protocolos de rede confiável, segura e verificável será o caminho chave para um futuro verdadeiramente descentralizado."