A Certora verifica formalmente a atualização do P-Token da Solana como equivalente ao Token SPL

Mesmo que o P-Token liberte até 98% mais unidades de computação, a Certora prova que continua a oferecer compatibilidade byte a byte com o SPL Token sem que sejam encontradas vulnerabilidades.

Pablo

Publicado:
Editado:

A atualização do P-Token recentemente implantada pela Solana representa uma das mudanças de infraestrutura mais significativas na história da rede. A atualização reduz drasticamente os recursos de computação necessários para as operações de token, preservando a compatibilidade com o programa SPL Token existente.

Para validar essa afirmação, a Fundação Solana contratou a Certora para realizar uma verificação formal para provar a equivalência comportamental entre a implementação do SPL Token legado e o novo programa P-Token baseado em Pinocchio. A empresa de pesquisa e desenvolvimento Anza descreveu anteriormente a verificação formal como "a garantia mais forte" da equivalência do P-Token, e os resultados da Certora fornecem uma validação adicional para o papel do P-Token como um substituto "drop-in" para um dos programas mais amplamente utilizados da Solana.

Por que o programa Token é importante

O programa SPL Token está no centro da economia de tokens de Solana. Ele lida com a criação de moeda, gerenciamento de contas de token, transferências, queimaduras e delegação para a grande maioria dos ativos na rede. Como quase todas as transações sem direito a voto em Solana interagem com tokens de alguma forma, qualquer alteração no programa de tokens traz amplas implicações para o ecossistema.

O P-Token apresenta uma nova implementação construída na biblioteca Pinocchio Rust. A atualização oferece melhorias substanciais de desempenho, reduzindo o consumo de computação em aproximadamente 95-98% para muitas operações comuns. As transferências de token padrão, por exemplo, caem de 4.645 unidades de computação para apenas 76, enquanto as instruções transfer_checked diminuem de 6.200 unidades de computação para 105.

Esses ganhos de eficiência podem liberar cerca de 12-13% do espaço de bloco em toda a rede, criando capacidade adicional sem aumentar os limites de bloco.

O desafio de provar uma substituição "drop-in

Embora as melhorias de desempenho atraiam a atenção, a compatibilidade continua sendo o requisito mais importante para uma atualização de infraestrutura dessa escala. As carteiras, dApps, protocolos e contratos inteligentes existentes dependem do comportamento do programa SPL Token. Qualquer desvio inesperado pode causar problemas de integração ou representar riscos para os programadores e utilizadores.

P Token

O P-Token não copia simplesmente a base de código original. A nova implementação adopta uma arquitetura diferente, incluindo acesso à conta de cópia zero, caminhos de execução optimizados e funcionalidade adicional. Como resultado, os desenvolvedores não puderam confiar apenas em testes convencionais para estabelecer a compatibilidade.

Em vez disso, a Certora usou técnicas de verificação formal para analisar matematicamente se os dois programas se comportam da mesma maneira em todas as entradas possíveis dentro do escopo de verificação definido.

O que a equivalência significa para o P-Token?

A estrutura de verificação da Certora avaliou três categorias de resultados para cada instrução analisada.

Primeiro, nenhum programa deve entrar em pânico durante a execução; ou seja, o programa nunca deve falhar ou abortar devido a um bug, caso extremo, etc.
Segundo, se o programa SPL Token processar com sucesso uma instrução e retornar Ok(()), o P-Token também deve retornar Ok(()). Nesses casos, ambos os programas devem deixar os dados da conta num estado idêntico byte a byte após a execução.
Em terceiro lugar, se P-Token devolver um erro, o programa SPL Token deve devolver o mesmo erro sob as mesmas condições.

A estrutura da Certora garante que, para cada estado e instrução possíveis da conta de entrada, o programa seja bem-sucedido (Ok(())) ou falhe graciosamente (Err(e)), mas nunca falhe internamente. A implementação do P-Token foi concebida como um superconjunto da funcionalidade do SPL Token, o que significa que qualquer operação aceite pelo SPL Token deve também ser aceite pelo P-Token.

O esforço de verificação identificou várias diferenças deliberadas entre os dois programas. O P-Token permite a auto-revogação do delegado, permitindo que um delegado revogue a sua própria autoridade sem exigir que o proprietário da conta do token assine a transação. O SPL Token exige a assinatura do proprietário para a mesma ação.

O P-Token também expande o suporte para autoridades multisig Token-2022. Enquanto o SPL Token rejeita essas contas, o P-Token aceita-as.

Uma terceira diferença envolve o tratamento de erros quando os dados de conta malformados contêm etiquetas COption não canónicas. O SPL Token rejeita imediatamente essas contas com um erro InvalidAccountData. O processo optimizado de carregamento de contas do P-Token vai mais fundo na lógica da instrução antes de gerar um erro, o que pode produzir resultados diferentes dependendo da instrução que está a ser executada.

Como essas diferenças eram intencionais e documentadas, a Certora incorporou suposições em partes do processo de verificação para manter a análise focada no limite de compatibilidade acordado.

Como a verificação funcionou

O Prover da Certora analisa o código fonte após a compilação para uma representação intermédia de baixo nível. Os engenheiros escrevem então especificações formais usando a Linguagem de Verificação da Certora para Rust, conhecida como CVLR.

O sistema de verificação criou cópias idênticas de informações de conta e dados de instrução, permitindo que o provador compare os dois programas sob as mesmas condições. Usando técnicas de Satisfiability Modulo Theories, o sistema avaliou todas as entradas possíveis simultaneamente, em vez de confiar em uma coleção limitada de casos de teste.

O âmbito incluiu todas as instruções partilhadas entre SPL Token e P-Token, excluindo AmountToUiAmount e UiAmountToAmount. A revisão também excluiu as três novas instruções específicas do P-Token: batch, unwrap_lamports e withdraw_excess_lamports.

Ao longo de todo o processo, o provador gerou uma prova de correção ou produziu contra-exemplos concretos que destacavam diferenças de comportamento que exigiam revisão.

Constatações e resultados

A Certora informou que não surgiram vulnerabilidades exploráveis durante o esforço de verificação. A análise confirmou que as propriedades No Panics e Equivalence on Ok são válidas para todas as instruções dentro do escopo sem exigir suposições adicionais. A propriedade Equivalência em Erro também se mantém em todo o conjunto de instruções partilhadas ao contabilizar as três diferenças comportamentais intencionais identificadas anteriormente.

Mais importante ainda, a verificação demonstrou que sempre que ambos os programas processam com sucesso a mesma entrada, eles produzem estados de conta pós-operação idênticos byte a byte. O processo também destacou como a verificação formal pode revelar casos extremos que os testes tradicionais podem deixar passar.

Um marco significativo para a Infraestrutura Solana

Os resultados da verificação chegam logo após a implantação do P-Token na rede principal, proporcionando confiança adicional em uma das atualizações de infraestrutura mais importantes de Solana.

Ao combinar grandes economias de computação com equivalência comportamental formalmente verificada, a atualização busca melhorar a eficiência da rede sem interromper os aplicativos e ativos que dependem do programa de token todos os dias.