Elimine erros de contratos inteligentes com TLA+

Em junho de 2016, havia grande entusiasmo pelo fato de “The DAO”, construído na blockchain Ethereum, estar prestes a se tornar o primeiro fundo de investimento descentralizado e totalmente digital do mundo.
Mas em poucas semanas, ele se tornou o garoto-propaganda dos hacks de DeFi depois que os invasores roubaram dele US$ 50 milhões em Ether.
Para quebrar o DAO, o invasor explorou a chamada vulnerabilidade de reentrada, uma vulnerabilidade de simultaneidade na qual um método de um contrato inteligente específico é chamado enquanto outro método ainda está em execução, e o DAO é apenas parte do desenvolvimento de longo prazo do contrato inteligente. O primeiro sofre desses erros.
Sucessores proeminentes incluem Uniswap/Lendf.Me, que teve US$ 25 milhões roubados em 2020, CREAM, que teve US$ 18 milhões roubados em 2021, e Fei, que teve US$ 80 milhões roubados em 2022.
A razão pela qual esses bugs persistem é que eles podem envolver interações de código inesperadas espalhadas por todo o contrato inteligente, às vezes até mesmo em contratos inteligentes diferentes. O número dessas interações de código pode ser muito grande, tornando difícil para os humanos detectar e eliminar contratos inteligentes não intencionais. código necessário.
Além disso, estas interações são muitas vezes difíceis de testar de forma automática e sistemática.
TLA+: O Exterminador
Entra em cena a Lógica Temporal de Ações (TLA+), uma linguagem para especificar e validar sistemas complexos. O TLA+ não apenas encontra erros, mas também verifica sua existência.
Como isso é possível, você pergunta? O TLA+ vem com um conjunto de ferramentas para verificação formal leve na forma da chamada verificação de modelo. Através da verificação de modelo, ele explora exaustivamente todas as possíveis interações simultâneas do modelo de código – as mesmas áreas que são difíceis de testar – e encontra bugs.
Imagine um exterminador que ilumina todos os cantos para expor e eliminar pragas indesejadas que se escondem naqueles cantos escuros que muitas vezes passam despercebidos ou são ignorados. É importante ressaltar que, após a construção do modelo de código, a verificação do modelo quase não requer intervenção humana para ser executada, o que a torna altamente econômica.
Para ilustrar com alguns números inventados: se as práticas padrão da indústria, como testes e análises de segurança, eliminam 80% dos bugs, e a verificação formal “pesada” elimina 99%, o uso do TLA+ elimina 90% com apenas um pequeno número de esforços de verificação pesada.
TLA+ e computadores para Internet
Nossa equipe de engenharia usa o TLA+ para analisar todos os aspectos da computação na Internet, incluindo os contratos inteligentes críticos para a segurança executados na plataforma. Embora os computadores Ethereum e Internet tenham modelos de execução diferentes, erros de reentrada podem aparecer em contratos inteligentes em ambas as blockchains.
Na verdade, devido ao seu alto rendimento, os computadores da Internet permitem múltiplas chamadas simultâneas para um único contrato inteligente, o que exige que os autores dos contratos inteligentes sejam mais cuidadosos para eliminar interações simultâneas indesejadas. Como a segurança é crítica para o sucesso dos computadores na Internet, o TLA+ é usado em muitos contratos inteligentes para detectar erros durante a fase de desenvolvimento.
Um contêiner de análise TLA+ (contratos inteligentes para computadores na internet) foi recentemente conduzido no recém-lançado Chain-Key Bitcoin (ckBTC), cujos resultados compartilharei abaixo.
Contrato inteligente ckBTC
Para falar sobre a análise TLA+ do ckBTC, vamos começar com uma visão geral de alto nível do ckBTC. ckBTC é um token nativo de computador da Internet apoiado com segurança por Bitcoin (BTC) na proporção de 1:1.
O livro-razão ckBTC é um contrato inteligente de contêiner no blockchain do computador da Internet que rastreia quanto ckBTC cada usuário final possui. Este mesmo livro-razão permite que os usuários finais transfiram seus ckBTC para outros usuários finais de forma mais rápida e barata do que transferir BTC na rede Bitcoin.
Para converter ckBTC em BTC e vice-versa, os usuários finais interagem com um contrato inteligente diferente, o minter ckBTC.
Em alto nível, a operação de conversão de BTC para ckBTC é assim:
Passos para obter ckBTC:
1. O usuário final primeiro transfere alguns BTC para um endereço de depósito Bitcoin específico do usuário, todos os endereços de depósito são totalmente controlados pelo código do contêiner inteligente ckBTC minter devido à assinatura ECDSA da chave da cadeia, que cria um novo UTXO de propriedade do depósito endereço;
2. O usuário final notifica o contrato inteligente ckBTC mint sobre o UTXO recém-depositado, solicitando ao mint que atualize o saldo do usuário;
3. O contrato inteligente do minter então usa a integração Bitcoin de computadores da Internet para recuperar todos os UTXOs pertencentes ao endereço de depósito controlado pelo minter, mas específico do usuário. O minter então seleciona novos UTXOs da rede Bitcoin, enviando-lhes verificações cruzadas. sua lista contábil interna de UTXOs que processou;
4. Finalmente, o minter instrui o livro-razão a cunhar novos ckBTC para todos os novos UTXOs na proporção de 1:1 e, uma vez concluído, adiciona os UTXOs recém-descobertos à lista de UTXOs processados.
Isenção de responsabilidade: o processo acima omite o processo KYT (Know Your Transaction) para simplificar.
Contrato inteligente ckBTC atende TLA+
A imagem de alto nível apresentada acima, na verdade, esconde um problema sutil de simultaneidade, e a boa notícia é que podemos detectar o problema usando o kit de ferramentas TLA+.
Mas antes que o TLA+ possa detectar qualquer coisa, devemos primeiro fornecer duas coisas:
Crie um modelo do nosso sistema usando a linguagem TLA+
Especifique as propriedades TLA+ que esperamos que o sistema implemente
Este modelo é uma versão simplificada, mas ainda totalmente definida do sistema, que no nosso caso inclui o contrato inteligente minter, mas também todas as outras partes relevantes do sistema, nomeadamente o contrato razão e a rede Bitcoin.
Para cada componente, modelamos seu estado e como as ações relevantes que um usuário final pode realizar (ou seja, transferir BTC ou ckBTC, depositar BTC ou chamar diferentes ações expostas pelo minter) alteram o estado.
Todos esses elementos são um tanto simplificados no modelo, com partes nas quais a análise se concentra (por exemplo, o código minter) modeladas com mais detalhes, enquanto outras partes (por exemplo, a rede Bitcoin) são modeladas com menos detalhes, na verdade, um modelo TLA+ é semelhante a uma especificação detalhada do projeto de um sistema.
Intuitivamente, o principal recurso que queremos implementar é garantir que nosso ckBTC seja totalmente suportado. Em outras palavras, nenhum usuário final deve ser capaz de “gastar em dobro” seu BTC depositado para obter mais ckBTC do que depositou.
Mas para analisar tal propriedade, temos que tornar esta intuição muito precisa, expressando-a formalmente na linguagem TLA+. Nossa definição formal é que o fornecimento total de ckBTC (ou seja, a soma de todos os saldos de ckBTC do usuário final, conforme armazenado pelo razão ckBTC) não excede a quantidade total de BTC controlada pelo contêiner de cunhagem (ou seja, o valor de todos UTXOs pertencentes a um endereço de depósito).
Detectar e resolver problemas
Depois de criar o modelo e as propriedades, o kit de ferramentas TLA+ pode analisar o modelo. Para executar a análise, primeiro definimos as configurações para executar a análise. Por exemplo, nossa configuração para ckBTC inclui apenas dois usuários finais diferentes e uma pequena quantidade do fornecimento total de Bitcoin (por exemplo, 5 satoshis).
Embora este cenário seja muito limitado, estudos empíricos mostram que a grande maioria dos problemas em sistemas informáticos pode ser encontrada num pequeno número de entidades. A pequena configuração permite que a análise explore sistematicamente todas as sequências de ação possíveis definidas pelo modelo e verifique se as propriedades prescritas são válidas em qualquer sequência.
Além disso, a análise é executada de forma totalmente automática, ou seja, não requer nenhuma intervenção humana e, se essas propriedades não forem válidas, fornece-nos a sequência exata de operações que violam essa propriedade.
Por exemplo, a análise pode revelar que podemos violar nossa propriedade “no unsecured ckBTC” em um cenário como o mostrado abaixo:
aqui:
Os usuários finais depositam BTC, como antes;
No entanto, agora o usuário final instrui o minter ckBTC a atualizar o saldo duas vezes em rápida sucessão, e em um computador na Internet essas atualizações podem ser interagidas com outros contratos inteligentes simultaneamente;
Duas atualizações executadas simultaneamente solicitam à rede Bitcoin todos os UTXOs depositados pelo usuário final, e ambas recebem em resposta o mesmo UTXO depositado na etapa 1. Como o UTXO ainda não está na lista de "processados", ambas as atualizações pensam que o UTXO é novo;
Ambas as atualizações instruem o livro-razão a cunhar a quantidade correspondente de ckBTC na etapa 4.
Portanto, ao final da etapa 4, estamos em um estado onde o fornecimento de ckBTC é o dobro da soma dos UTXOs nos endereços de depósito, o que viola nossa propriedade “no unsupported ckBTC”.
Observe que esse erro ocorre apenas porque as atualizações no saldo do usuário final são executadas simultaneamente - na verdade, é um erro reentrante no mesmo estilo daquele que derrubou o DAO.
Uma maneira de resolver esse problema é evitar que as atualizações de saldo sejam executadas em paralelo para o mesmo usuário final. Podemos fazer isso fazendo com que o minter armazene o usuário final em uma lista de usuários "bloqueados" quando a atualização de saldo começar e os mantenha lá durante a lista de atualização para conseguir isso.
Se o usuário final tentar iniciar outra atualização de saldo simultânea, a atualização primeiro verificará e encontrará esse usuário final específico na lista de usuários bloqueados e, em seguida, abortará.
Observe que estamos simplificando um pouco o ataque aqui: o bloqueio é, na verdade, um padrão bastante comum para contratos inteligentes de IC, e os mineradores de ckBTC o implantaram desde o início. No entanto, o bloqueio executado incorretamente abre a porta para os ataques acima, que o TLA+ é capaz de detectar.
Além disso, encontramos alguns casos extremos que violavam “nenhum ckBTC não suportado” e outras propriedades importantes, e depois que aplicamos todas as correções, o TLA+ foi capaz de verificar e confirmar que não havia mais violações de propriedades em nossa configuração definida.
Você deve usar o TLA+ para seus contratos inteligentes?
Absolutamente! Ok, ok, talvez eu deva fornecer uma resposta mais sutil, que nossa equipe de P&D usa para contratos inteligentes críticos em computadores da Internet sempre que uma simultaneidade não trivial estiver envolvida.
Por exemplo, a análise do TLA+ descobriu bugs sutis de simultaneidade na governança de computadores da Internet e nos contêineres de razão que foram perdidos nas revisões manuais de segurança anteriores e poderiam ter levado a problemas, casos e pontos importantes – o TLA+ na descoberta de problemas tão espinhosos foi uma explosão absoluta.
É claro que há um preço a pagar em termos de aquisição do know-how e depois da construção do modelo, mas empiricamente o preço é razoável, especialmente dada a natureza de alto risco da segurança da blockchain.
Não se deve intimidar pela linguagem TLA+ em si, apesar do nome intimidante, o acesso aos seus poderosos recursos é bastante simples. Na verdade, uma folha de dicas do TLA+ descrevendo quase todos os recursos do TLA+ poderia caber aproximadamente em uma página:
mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html
Além do mais, o esforço necessário para construir o modelo é comparável às revisões de segurança manuais padrão. Por exemplo, para um minerador ckBTC, levaria um total de cerca de 3 semanas para que uma pessoa entendesse o design, criasse o modelo inicial e as propriedades.
O modelo TLA+ resultante é muito mais simples que a implementação, tanto porque é mais simples que o código quanto devido à natureza de alto nível do TLA+. O modelo para o minter ckBTC requer cerca de 250 linhas de código em comparação com as milhares de linhas de implementação do Rust. Talvez surpreendentemente, uma das partes mais difíceis em termos de esforço é especificar as propriedades necessárias, já que muitas vezes encontramos lacunas nas especificações intuitivas.
Assim que o modelo for concluído, a análise (verificação do modelo) será concluída automaticamente. A análise pode levar muito tempo para ser executada – por exemplo, para ckBTC, demorou mais de 20 horas para ser concluída. Finalmente, outro benefício do TLA é que a modelagem e a análise podem ser feitas na fase de design, antes da implementação do código, o que ajuda a eliminar grandes refatorações devido a erros de design posteriormente.
Onde TLA+ é inútil
Do lado negativo, o TLA+ é menos útil para programas sequenciais complexos, em oposição a programas simultâneos, e também não é bom para lidar com protocolos criptográficos complexos, para os quais existem outras ferramentas (por exemplo, Tamarin) que são mais úteis.
Finalmente, há a questão de manter o modelo TLA+ e a implementação real sincronizados, pois à medida que o código de implementação evolui ao longo do tempo, ele pode não estar mais em conformidade com o modelo, o que pode ser difícil de detectar sem o suporte de ferramentas.
Na verdade, nossa equipe de P&D está tentando resolver esse problema – espero que possamos compartilhar algumas ferramentas com você em breve!
Espero que esta visão geral tenha despertado seu interesse em usar o TLA+ para seus próprios contratos inteligentes críticos e, em caso afirmativo, fique atento – uma postagem de acompanhamento com um tutorial mais aprofundado sobre como usar o TLA+ para contratos inteligentes será lançada em breve, e em anexo está um modelo TLA+ real desenvolvido por nossa equipe de P&D.
Conteúdo IC que lhe interessa
Progresso Tecnológico | Informações do Projeto |
Colete e siga o canal IC Binance
Mantenha-se atualizado com as informações mais recentes