Provas de Coerência Transacional para Smart Contracts em Blockhains

Blockchain technology is an emergent topic based on decentralization and immutability, enabling mutually untrusting parties to fairly exchange assets without the need of a central authority. Recently, the addition of blockchain programs, known as smart contracts, enabled the technology to expand upon a variety of industry sectors, already known to traditional software. Many organizations and corporates saw a growth opportunity, extending their businesses into this domain — now, though, with the blockchain twist. However, the inclusion of computation exposed a weak link in the overall blockchain security, due to carrying not only traditional software bugs, but also never before seen ones. That way, smart contracts, especially valuable ones, became enticing for hackers to exploit, which resulted in a set of tragedies where funds were stolen, among other consequences. Soon after, smart contract security became a most valuable topic of research among blockchain platforms. The Tezos blockchain is a relatively new platform whose stance values security by construct infrastructure, in consequence of the past incidents. While many smart contract security solutions were devised over the years, these have not been properly adapted nor adopted for the average developer in the community. Due to various reasons, but for one, seamless integration with the smart contract development processes is one of them. This dissertation approaches the blockchain security problem through an indirect approach, providing the developer with better accessibility and conditions for working on one of Tezos’s state-of-the-art security tools. Although it is unorthodox, it is hoped for the solution to inspire and appeal other blockchain communities by shedding some light in this unknown direction.A tecnologia blockchain é um tópico emergente baseado na descentralização e imutabilidade, permitindo que entidades desconhecidas e não confiáveis consigam trocar bens e valores digitais de forma justa sem necessitarem uma entidade central. Recentemente, a adição de programas na blockchain, designados de smart contracts, permitiu que tal se expandisse sobre uma variedade de sectores industriais já explorada por programas tradicionais. Contudo, muitas empresas viram uma oportunidade de negócio bastante lucrativa, estendendo o seu negócio para este ambiente, agora incutindo as regras da blockchain. Embora oportunidades lucrativas tenham aparecido, problemas relativos aos programas tradicionais, bem como outros novos ainda não descobertos, também. Os smart contracts revelaram-se como um elo mais fraco para a segurança da blockchain e, tendo estes a capacidade de reter bastante valor monetário, tornaram-se um alvo aliciante para hackers. Não muito depois, notícias espalharam-se pela internet a anunciar crimes por entidades anónimas — roubo e congelamento de fundos, entre outras consequências, na blockchain. Após o primeiro grande incidente, a segurança na blockchain começou a ser um tópico bastante estudado por peritos e investigadores das várias comunidades. A blockchain da Tezos é uma plataforma relativamente recente, com uma postura relativa à segurança bastante madura, resultado dos incidentes passados. Enquanto várias soluções foram alcançadas para a segurança de smart contracts, estas não seriam ainda bem incorporadas pela comunidade, ou pelo menos para o engenheiro de contratos comum. Existem várias razões, porém, acessibilidade nos vários aspetos das ferramentas de segurança é uma delas. O trabalho realizado por esta dissertação passa por solucionar este problema, mais especificamente, solucionar o problema para uma ferramenta de segurança de programas na blockchain da Tezos. Este tipo de solução não é comum na literatura, contudo, espera-se que o trabalho realizado sirva de inspiração para que as comunidades possa explorar esta vertente mais indireta de segurança na blockchain