FenixEdu™

Dissertação

Extending the Concert Framework to Verify Solana Programs EVALUATED

Detalhes: Smart Contracts são programas guardados numa blockchain que ajuda o acordo entre dois participantes sem envolvimento de um terceiro confiável. Uma vez que, Smart Contracts contêm enormes quantidades de criptomoedas e não podem ser modificados uma vez enviados para a blockchain é crucial assegurar o seu correto funcionamento e que e estes não possuem bugs nem vulnerabilidades. Solana é uma blockchain recente que possui a funcionalidade de Smart Contracts. Esta blockchain apresenta um crescimento rápido em consequência da sua velocidade e baixa taxa de transação. Nesta tese, adaptamos e estendemos a framework de verificação de Smart Contracts em Coq, ConCert. A nossa extensão permite a escrita de contratos Solana introduzindo ao modelo existente conceitos de Solana. É também possível extrair Smart Contracts escritos em Coq para Rust e, uma vez extraídos, e após pequenas correções estão prontos para ser enviados para a blockchain Solana. O ConCert estendido permite a verificação de contratos Solana existentes e o desenvolvimento de contratos verificados. A framework estendida foi avaliada através da avaliação das provas conseguidas no modelo, avaliando a complexidade dos contratos que a framework conseguiu representar e extrair, o tempo de extração e o overhead obtido na extração. Verificou-se que, devido à expressividade do nosso modelo, contratos complexos não são possíveis representar e, por consequência, não foram verificados nem extraídos. Contudo, contratos mais simples fora representados e extraídos. Desta forma, esta dissertação introduza possibilidade de escrever contratos verificados em Coq e extraí-los para a blockchain Solana.
Keywords: Blockchain, Smart Contracts, Solana, Verificação Formal, ConCert, Coq

Discussão: novembro 25, 2022, 10:30