No dia 8 de abril, durante a Conferência de Acadêmicos Web3 2025, realizada em Hong Kong, o professor do Departamento de Ciência da Computação da Universidade de Yale e cofundador da CertiK, Shao Zhong, deu uma palestra intitulada "Segurança e Provas 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 que possam ser verificadas mecanicamente para protocolos de consenso complexos com tolerância a falhas bizantinas (BFT), estabelecendo uma base técnica para a confiabilidade e o desenvolvimento em grande escala do ecossistema Web3.
Na sua apresentação, o Professor Shao Zhong apontou que os atuais protocolos de consenso (como PBFT, Jolteon), embora amplamente utilizados, muitas vezes escondem vulnerabilidades potenciais devido à sua complexidade de implementação. Para resolver esse problema, o modelo LiDO propôs de forma inovadora uma estrutura de verificação refinada em três camadas:
Security Abstraction Layer: Mapeamento de protocolos como máquinas de estado linearizadas para garantir a consistência do log (segurança);
Camada de Garantia Ativa: Introduz o mecanismo "Pacemaker", que resolve o problema de latência da rede através de difusão por tempo limite e sincronização de rodadas;
Camada de extensão DAG: suporta protocolos DAG emergentes como Narwhal e Bullshark, permitindo a validação eficiente do consenso sem líder.
Atualmente, o LiDO tem sido aplicado com sucesso ao protocolo de nível industrial Jolteon (BFT de dois estágios) e múltiplos protocolos DAG, completando a prova mecanizada de mais de 10.000 linhas de código Coq, com 4.000 linhas de segurança e 1.700 linhas de código de verificação de atividade. "Atualmente, os protocolos de consenso PoS geralmente enfrentam o dilema de segurança, viabilidade e descentralização", apontou o professor Shao Zhong em seu discurso. "O modelo LiDO é uma solução de design sistemático para quebrar esse dilema."
O CertiKOS, desenvolvido pelo Professor Shao Zhong e sua equipe, é o primeiro sistema operacional "livre de vulnerabilidade" do mundo que passou por verificação formal e foi saudado como um "marco na segurança do sistema ciber-físico". Esta conquista não só estabelece a base para a tecnologia da empresa de segurança CertiK, mas também demonstra sua profunda experiência no campo da segurança de sistemas. Nos últimos anos, o Professor Shao Zhong esteve profundamente envolvido na segurança blockchain e cofundou a CertiK com seu discípulo Professor Gu Ronghui em 2017, introduzindo a tecnologia de verificação formal na segurança de contratos inteligentes e protocolos on-chain, e escoltando a segurança de centenas de bilhões de dólares em criptoativos.
LiDO já completou o design do modelo e a validação formal, e começou a explorar a possibilidade de integração com principais blockchains e protocolos descentralizados. O Professor Shao Zhong afirmou que a CertiK se dedica 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, 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."
O conteúdo serve apenas de referência e não constitui uma solicitação ou oferta. Não é prestado qualquer aconselhamento em matéria de investimento, fiscal ou jurídica. Consulte a Declaração de exoneração de responsabilidade para obter mais informações sobre os riscos.
O professor Shao Zhong, co-fundador da CertiK, participou da Cimeira de Académicos Web3, apresentando pela primeira vez o modelo LiDO.
No dia 8 de abril, durante a Conferência de Acadêmicos Web3 2025, realizada em Hong Kong, o professor do Departamento de Ciência da Computação da Universidade de Yale e cofundador da CertiK, Shao Zhong, deu uma palestra intitulada "Segurança e Provas 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 que possam ser verificadas mecanicamente para protocolos de consenso complexos com tolerância a falhas bizantinas (BFT), estabelecendo uma base técnica para a confiabilidade e o desenvolvimento em grande escala do ecossistema Web3.
Na sua apresentação, o Professor Shao Zhong apontou que os atuais protocolos de consenso (como PBFT, Jolteon), embora amplamente utilizados, muitas vezes escondem vulnerabilidades potenciais devido à sua complexidade de implementação. Para resolver esse problema, o modelo LiDO propôs de forma inovadora uma estrutura de verificação refinada em três camadas:
Security Abstraction Layer: Mapeamento de protocolos como máquinas de estado linearizadas para garantir a consistência do log (segurança);
Camada de Garantia Ativa: Introduz o mecanismo "Pacemaker", que resolve o problema de latência da rede através de difusão por tempo limite e sincronização de rodadas;
Camada de extensão DAG: suporta protocolos DAG emergentes como Narwhal e Bullshark, permitindo a validação eficiente do consenso sem líder.
Atualmente, o LiDO tem sido aplicado com sucesso ao protocolo de nível industrial Jolteon (BFT de dois estágios) e múltiplos protocolos DAG, completando a prova mecanizada de mais de 10.000 linhas de código Coq, com 4.000 linhas de segurança e 1.700 linhas de código de verificação de atividade. "Atualmente, os protocolos de consenso PoS geralmente enfrentam o dilema de segurança, viabilidade e descentralização", apontou o professor Shao Zhong em seu discurso. "O modelo LiDO é uma solução de design sistemático para quebrar esse dilema."
O CertiKOS, desenvolvido pelo Professor Shao Zhong e sua equipe, é o primeiro sistema operacional "livre de vulnerabilidade" do mundo que passou por verificação formal e foi saudado como um "marco na segurança do sistema ciber-físico". Esta conquista não só estabelece a base para a tecnologia da empresa de segurança CertiK, mas também demonstra sua profunda experiência no campo da segurança de sistemas. Nos últimos anos, o Professor Shao Zhong esteve profundamente envolvido na segurança blockchain e cofundou a CertiK com seu discípulo Professor Gu Ronghui em 2017, introduzindo a tecnologia de verificação formal na segurança de contratos inteligentes e protocolos on-chain, e escoltando a segurança de centenas de bilhões de dólares em criptoativos.
LiDO já completou o design do modelo e a validação formal, e começou a explorar a possibilidade de integração com principais blockchains e protocolos descentralizados. O Professor Shao Zhong afirmou que a CertiK se dedica 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, 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."