A CertiK lançou recentemente um relatório de verificação formal avançado sobre o módulo Cosmos SDK Bank, que, até onde sabemos, é a primeira tentativa bem-sucedida de verificação formal do Cosmos SDK. A verificação formal é uma técnica que utiliza lógica matemática para garantir que um sistema esteja em conformidade com as especificações, de modo que se comporte conforme o esperado sob todas as entradas e condições possíveis. Neste artigo, apresentaremos as etapas específicas para verificar formalmente o módulo Cosmos SDK Bank, bem como alguns resultados da verificação.
O que é o Cosmos SDK?
O Cosmos Software Development Kit (SDK) é uma estrutura que permite aos desenvolvedores construir aplicativos blockchain personalizados. Usando o Cosmos SDK, os desenvolvedores podem facilmente iniciar seu próprio blockchain de Camada 1 sem se preocupar com o design e a implementação da camada de consenso até a camada de aplicativo. O Cosmos SDK fornece módulos principais padrão que podem ser importados diretamente e usados por qualquer cadeia, como módulos de piquetagem, autenticação, gov e mint.
fonte:
Módulo banco
O módulo do banco no Cosmos SDK é responsável por todas as funções relacionadas ao gerenciamento de tokens, como a transferência de tokens nativos. O envio de tokens precisa atender a muitas restrições e condições. Por exemplo, a conta deve ter tokens disponíveis suficientes, excluindo os tokens que foram apostados, bloqueados ou em processo de desagregação. Com o suporte de módulos como staking e auth, o módulo do banco gerencia todo o processo de envio de tokens. Embora o módulo banco dependa de vários outros módulos, por não estarem no escopo desta verificação formal, fizemos algumas suposições sobre sua funcionalidade para simplificar o processo.
O módulo bancário do SDK consiste em vários submódulos, incluindo guardião e tipos, que são componentes principais que definem o comportamento do módulo e os tipos de dados. Vamos nos concentrar no submódulo keeper, pois ele cobre as principais funções e recursos do módulo.
O submódulo keeper possui dois componentes principais: visualizar e enviar. O guardião da visualização é responsável por gerenciar contas e saldos, enquanto o guardião do envio é responsável por alterar os saldos das contas, como transferir e apostar tokens bloqueados ou desbloqueados. O fluxo do módulo do banco é mostrado na figura abaixo. As setas indicam a direção dos componentes para funções ou Keepers.
fonte:
Método de autenticação
Conforme mencionado anteriormente, o escopo desta verificação está limitado ao módulo banco. Antes de começar a verificação, primeiro formulamos especificações formais para os tipos de dados no módulo do banco. Por exemplo, existe uma estrutura de dados de token no módulo do banco, que contém a denominação do tipo string e a quantidade do tipo big.Int, que é definida no código-fonte da seguinte forma:
Essa estrutura é muito simples, usamos Coq (nossa linguagem de modelagem e verificação formal) para defini-la da seguinte forma:
Com base nesta definição, primeiro provamos algumas propriedades sobre as operações básicas da moeda para estabelecer as bases para a integridade funcional do módulo do banco, pois requer modificação e manipulação frequentes do tipo de moeda. Por exemplo:
Este lema prova uma invariância fundamental: subtrair duas moedas não altera a sua denominação, nem causa um saldo negativo.
Semelhante ao exemplo anterior, os componentes subjacentes de cada transição de estado são modelados em Coq. Esses componentes incluem KV Store, GasMeter, Error Handling e Context.
Para especificações detalhadas dos tipos de dados e sua verificação, consulte:
Modele o goleiro
Depois de concluir a modelagem dos componentes básicos, podemos modelar o núcleo do módulo do banco para descrever a função do módulo. O depositário do banco possui duas interfaces, uma para acesso somente leitura aos dados do token e outra para transferência de token e manutenção de suprimentos.
O View Keeper é responsável por lidar com o acesso somente leitura aos saldos das contas e contém quatro funções para calcular os saldos das contas:
GetBalance: Consulta o saldo da conta de uma denominação específica através do endereço. Considera dois casos: uma sequência de bytes nulos e uma sequência de bytes não nulos. A verificação formal garante que a função GetBalance produza resultados corretos em ambos os casos.
LockedCoins: Retorna todos os tokens não consumíveis da conta correspondente a um endereço. Devido a restrições de tempo, fizemos suposições sobre algumas implementações do módulo auth.
GetAllBalances: Retorna todos os saldos de contas no endereço especificado.
GetAccountsBalances: Retorna todos os saldos de contas do armazenamento e toma os campos BAddress e BCoins como registros.
O gerenciador de envio lida com transferências e fornecimento de tokens. Durante o processo de transferência, mantém o fornecimento de tokens para que nenhum novo token seja cunhado.
SetBalance: Defina o saldo do token da conta através do endereço. Esta função considera dois casos: saldos zerados e saldos zerados. Em ambos os casos, a correção do SetBalance é comprovada.
subUnlockedCoin: Deduza o valor especificado (token) de um endereço. A função recursiva subUnlockedCoins faz o mesmo para um conjunto de tokens. As propriedades relevantes destas funções são tratadas como suposições axiomáticas.
addCoin: Adicione a quantidade especificada (tokens) a um endereço. A função recursiva addCoins executa a mesma operação em um conjunto de moedas. As propriedades relevantes destas funções são consideradas suposições axiomáticas.
SendCoins: Envie dinheiro de um endereço de conta para outro endereço de conta, para que o ouro em ambos os endereços seja atualizado. Caso o destinatário não exista, será criada uma nova conta para ele.
Usando o modelo acima dos componentes principais, podemos começar a verificação.
Processo de verificação
Nossa verificação é feita descrevendo formalmente as propriedades invariantes dessas funções e provando-as em um sistema auxiliar de prova, focando principalmente na funcionalidade central do "View Keeper" e do "Send Keeper".
Por exemplo, a especificação e o lema setBalance_ok provam a correção da função setBalance do módulo BaseSendKeeper, provando especificamente as seguintes propriedades:
Quando send.setBalance retorna ao estado "Ok", há um newMultiStore. Neste momento, o ambiente uctx atualizado é derivado do ambiente antigo original ctx atualizando newMultiStore.
O saldo que está sendo definido é um token válido (possui as propriedades exigidas de um token no sistema).
O relacionamento setBalance_prop é mantido para garantir que a função atualize o saldo em newMultiStore da maneira esperada e gere o ambiente atualizado uctx.
Depois que a configuração do saldo for concluída, use o endereço da conta e a denominação balance.(Denom) para chamar view.GetBalance no ambiente atualizado uctx, e o mesmo saldo definido por send.setBalance será retornado.
Essas propriedades são descritas na linguagem de especificação Coq da seguinte forma:
Para código Coq de outra natureza, acesse:
Carreira futura
A base desta verificação assenta em vários pressupostos e axiomas, que podemos verificar mais profundamente para ampliar o âmbito da verificação. O trabalho futuro centra-se nas seguintes áreas:
Verificação de suposições: A verificação atual baseia-se numa série de suposições como base para a prova. Essas suposições podem ser testadas no futuro para garantir que reflitam com precisão o comportamento e as propriedades esperados do sistema.
Verificação do módulo de autenticação: Este módulo é responsável pelo gerenciamento dos dados da conta e do mecanismo de assinatura e é o componente principal do Cosmos SDK. No futuro, pode ser verificado de forma totalmente formal para garantir que a implementação do módulo e a interação com outros módulos sejam precisas.
Mais teoremas sobre delegação, cunhagem e venda de moedas: Expandir o âmbito da verificação e introduzir mais teoremas sobre delegação, cunhagem e venda de moedas ajudará a compreender o mecanismo de funcionamento do sistema de forma mais abrangente. Esses teoremas podem ser combinados com a verificação do módulo de autenticação para garantir a consistência geral e a correção do sistema.
Expandir toda a infraestrutura do Cosmos SDK: o trabalho de verificação nesta fase concentra-se principalmente no módulo do banco e seus componentes relacionados. No futuro, o processo de verificação formal poderá ser estendido a toda a infraestrutura do Cosmos SDK, melhorando assim a precisão geral, a segurança e a estabilidade da plataforma e proporcionando um ambiente mais estável e confiável para desenvolvedores e usuários.
Integração com outros módulos: Como o Cosmos SDK inclui vários módulos interconectados, é benéfico explorar as interações e dependências entre eles. Isto requer a verificação da exatidão das interações entre os módulos e a garantia de que quaisquer alterações em um módulo não afetem negativamente outros módulos.
Modelagem e verificação de mecanismos de incentivo: o Cosmos SDK também integra mecanismos de incentivo, como staking e distribuição de recompensas. A investigação futura irá modelar e validar estes mecanismos para garantir que sejam correctos e consistentes com os incentivos económicos esperados.
Este artigo demonstra o primeiro caso bem-sucedido de verificação formal avançada do módulo Cosmos SDKbank, realizando um trabalho eficaz para construir a base de segurança e confiabilidade do ecossistema blockchain. O trabalho futuro expandirá essa conquista validando suposições, validando outros módulos e cobrindo toda a infraestrutura do Cosmos SDK, construindo, em última análise, uma plataforma mais sólida e confiável para desenvolvedores e usuários.
Ver original
Esta página pode conter conteúdo de terceiros, que é fornecido apenas para fins informativos (não para representações/garantias) e não deve ser considerada como um endosso de suas opiniões pela Gate nem como aconselhamento financeiro ou profissional. Consulte a Isenção de responsabilidade para obter detalhes.
Explique detalhadamente a verificação formal dos módulos padrão do Cosmos SDK
/ Web3 Complete Software Stack Verificação formal avançada/
A CertiK lançou recentemente um relatório de verificação formal avançado sobre o módulo Cosmos SDK Bank, que, até onde sabemos, é a primeira tentativa bem-sucedida de verificação formal do Cosmos SDK. A verificação formal é uma técnica que utiliza lógica matemática para garantir que um sistema esteja em conformidade com as especificações, de modo que se comporte conforme o esperado sob todas as entradas e condições possíveis. Neste artigo, apresentaremos as etapas específicas para verificar formalmente o módulo Cosmos SDK Bank, bem como alguns resultados da verificação.
O que é o Cosmos SDK?
O Cosmos Software Development Kit (SDK) é uma estrutura que permite aos desenvolvedores construir aplicativos blockchain personalizados. Usando o Cosmos SDK, os desenvolvedores podem facilmente iniciar seu próprio blockchain de Camada 1 sem se preocupar com o design e a implementação da camada de consenso até a camada de aplicativo. O Cosmos SDK fornece módulos principais padrão que podem ser importados diretamente e usados por qualquer cadeia, como módulos de piquetagem, autenticação, gov e mint.
fonte:
Módulo banco
O módulo do banco no Cosmos SDK é responsável por todas as funções relacionadas ao gerenciamento de tokens, como a transferência de tokens nativos. O envio de tokens precisa atender a muitas restrições e condições. Por exemplo, a conta deve ter tokens disponíveis suficientes, excluindo os tokens que foram apostados, bloqueados ou em processo de desagregação. Com o suporte de módulos como staking e auth, o módulo do banco gerencia todo o processo de envio de tokens. Embora o módulo banco dependa de vários outros módulos, por não estarem no escopo desta verificação formal, fizemos algumas suposições sobre sua funcionalidade para simplificar o processo.
O módulo bancário do SDK consiste em vários submódulos, incluindo guardião e tipos, que são componentes principais que definem o comportamento do módulo e os tipos de dados. Vamos nos concentrar no submódulo keeper, pois ele cobre as principais funções e recursos do módulo.
O submódulo keeper possui dois componentes principais: visualizar e enviar. O guardião da visualização é responsável por gerenciar contas e saldos, enquanto o guardião do envio é responsável por alterar os saldos das contas, como transferir e apostar tokens bloqueados ou desbloqueados. O fluxo do módulo do banco é mostrado na figura abaixo. As setas indicam a direção dos componentes para funções ou Keepers.
fonte:
Método de autenticação
Conforme mencionado anteriormente, o escopo desta verificação está limitado ao módulo banco. Antes de começar a verificação, primeiro formulamos especificações formais para os tipos de dados no módulo do banco. Por exemplo, existe uma estrutura de dados de token no módulo do banco, que contém a denominação do tipo string e a quantidade do tipo big.Int, que é definida no código-fonte da seguinte forma:
Essa estrutura é muito simples, usamos Coq (nossa linguagem de modelagem e verificação formal) para defini-la da seguinte forma:
Com base nesta definição, primeiro provamos algumas propriedades sobre as operações básicas da moeda para estabelecer as bases para a integridade funcional do módulo do banco, pois requer modificação e manipulação frequentes do tipo de moeda. Por exemplo:
Este lema prova uma invariância fundamental: subtrair duas moedas não altera a sua denominação, nem causa um saldo negativo.
Semelhante ao exemplo anterior, os componentes subjacentes de cada transição de estado são modelados em Coq. Esses componentes incluem KV Store, GasMeter, Error Handling e Context.
Para especificações detalhadas dos tipos de dados e sua verificação, consulte:
Modele o goleiro
Depois de concluir a modelagem dos componentes básicos, podemos modelar o núcleo do módulo do banco para descrever a função do módulo. O depositário do banco possui duas interfaces, uma para acesso somente leitura aos dados do token e outra para transferência de token e manutenção de suprimentos.
O View Keeper é responsável por lidar com o acesso somente leitura aos saldos das contas e contém quatro funções para calcular os saldos das contas:
GetBalance: Consulta o saldo da conta de uma denominação específica através do endereço. Considera dois casos: uma sequência de bytes nulos e uma sequência de bytes não nulos. A verificação formal garante que a função GetBalance produza resultados corretos em ambos os casos.
LockedCoins: Retorna todos os tokens não consumíveis da conta correspondente a um endereço. Devido a restrições de tempo, fizemos suposições sobre algumas implementações do módulo auth.
GetAllBalances: Retorna todos os saldos de contas no endereço especificado.
GetAccountsBalances: Retorna todos os saldos de contas do armazenamento e toma os campos BAddress e BCoins como registros.
O gerenciador de envio lida com transferências e fornecimento de tokens. Durante o processo de transferência, mantém o fornecimento de tokens para que nenhum novo token seja cunhado.
SetBalance: Defina o saldo do token da conta através do endereço. Esta função considera dois casos: saldos zerados e saldos zerados. Em ambos os casos, a correção do SetBalance é comprovada.
subUnlockedCoin: Deduza o valor especificado (token) de um endereço. A função recursiva subUnlockedCoins faz o mesmo para um conjunto de tokens. As propriedades relevantes destas funções são tratadas como suposições axiomáticas.
addCoin: Adicione a quantidade especificada (tokens) a um endereço. A função recursiva addCoins executa a mesma operação em um conjunto de moedas. As propriedades relevantes destas funções são consideradas suposições axiomáticas.
SendCoins: Envie dinheiro de um endereço de conta para outro endereço de conta, para que o ouro em ambos os endereços seja atualizado. Caso o destinatário não exista, será criada uma nova conta para ele.
Usando o modelo acima dos componentes principais, podemos começar a verificação.
Processo de verificação
Nossa verificação é feita descrevendo formalmente as propriedades invariantes dessas funções e provando-as em um sistema auxiliar de prova, focando principalmente na funcionalidade central do "View Keeper" e do "Send Keeper".
Por exemplo, a especificação e o lema setBalance_ok provam a correção da função setBalance do módulo BaseSendKeeper, provando especificamente as seguintes propriedades:
Quando send.setBalance retorna ao estado "Ok", há um newMultiStore. Neste momento, o ambiente uctx atualizado é derivado do ambiente antigo original ctx atualizando newMultiStore.
O saldo que está sendo definido é um token válido (possui as propriedades exigidas de um token no sistema).
O relacionamento setBalance_prop é mantido para garantir que a função atualize o saldo em newMultiStore da maneira esperada e gere o ambiente atualizado uctx.
Depois que a configuração do saldo for concluída, use o endereço da conta e a denominação balance.(Denom) para chamar view.GetBalance no ambiente atualizado uctx, e o mesmo saldo definido por send.setBalance será retornado.
Essas propriedades são descritas na linguagem de especificação Coq da seguinte forma:
Para código Coq de outra natureza, acesse:
Carreira futura
A base desta verificação assenta em vários pressupostos e axiomas, que podemos verificar mais profundamente para ampliar o âmbito da verificação. O trabalho futuro centra-se nas seguintes áreas:
Verificação de suposições: A verificação atual baseia-se numa série de suposições como base para a prova. Essas suposições podem ser testadas no futuro para garantir que reflitam com precisão o comportamento e as propriedades esperados do sistema.
Verificação do módulo de autenticação: Este módulo é responsável pelo gerenciamento dos dados da conta e do mecanismo de assinatura e é o componente principal do Cosmos SDK. No futuro, pode ser verificado de forma totalmente formal para garantir que a implementação do módulo e a interação com outros módulos sejam precisas.
Mais teoremas sobre delegação, cunhagem e venda de moedas: Expandir o âmbito da verificação e introduzir mais teoremas sobre delegação, cunhagem e venda de moedas ajudará a compreender o mecanismo de funcionamento do sistema de forma mais abrangente. Esses teoremas podem ser combinados com a verificação do módulo de autenticação para garantir a consistência geral e a correção do sistema.
Expandir toda a infraestrutura do Cosmos SDK: o trabalho de verificação nesta fase concentra-se principalmente no módulo do banco e seus componentes relacionados. No futuro, o processo de verificação formal poderá ser estendido a toda a infraestrutura do Cosmos SDK, melhorando assim a precisão geral, a segurança e a estabilidade da plataforma e proporcionando um ambiente mais estável e confiável para desenvolvedores e usuários.
Integração com outros módulos: Como o Cosmos SDK inclui vários módulos interconectados, é benéfico explorar as interações e dependências entre eles. Isto requer a verificação da exatidão das interações entre os módulos e a garantia de que quaisquer alterações em um módulo não afetem negativamente outros módulos.
Modelagem e verificação de mecanismos de incentivo: o Cosmos SDK também integra mecanismos de incentivo, como staking e distribuição de recompensas. A investigação futura irá modelar e validar estes mecanismos para garantir que sejam correctos e consistentes com os incentivos económicos esperados.
Este artigo demonstra o primeiro caso bem-sucedido de verificação formal avançada do módulo Cosmos SDKbank, realizando um trabalho eficaz para construir a base de segurança e confiabilidade do ecossistema blockchain. O trabalho futuro expandirá essa conquista validando suposições, validando outros módulos e cobrindo toda a infraestrutura do Cosmos SDK, construindo, em última análise, uma plataforma mais sólida e confiável para desenvolvedores e usuários.