A carregar...
Publicação
Mechanisms for Modeling and Validation of Smart Contracts
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 1.82 MB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
The characterization of a Smart Contract consists of describing agreements between
multiple parties involved, which can be autonomously upheld without the need of a trusted
intermediary. SCs are stored and executed on the Blockchain, a decentralized, digital
ledger designed to log transactions in a secure and transparent manner. It operates across
a network of computers, where each node retains a copy of the ledger and transactions
are validated through consensus protocols.
One of the key features of SCs and blockchains is their immutability: once they have
been deployed, the contracts and blocks of the blockchain can not be changed (although it
is technically possible, it necessitates extreme measures such as hard forking or obtaining
cooperation of a substantial portion of the network nodes in a blockchain).
However, vulnerabilities can still exist in the code of SCs, potentially resulting in
exploitable bugs that may lead to the loss of valuable assets. To address these issues
domain-specific languages (DSLs) are under development to offer safety assurances to
programmers. However, none of these languages can offer absolute proof of contract
correctness, leaving room for improvement in the development of SCs.
This thesis aims to contribute to the process of elaborating SCs by introducing a
language designed to capture their behavior. In addition to this language, suitable tool
mechanisms were also developed to perform static validations on the behavior of existing
Daml SCs, ensuring alignment with the intended outcomes of the contracts and ultimately
bolstering the auditability of SCs.
A caracterização de um SC consiste em descrever acordos entre várias partes envolvidas, que podem ser mantidos autonomamente sem a necessidade de um intermediário de confiança. Os SCs são armazenados e executados na Blockchain, uma digital ledger descentralizada tendo como função registar transações de maneira segura e transparente. A blockchain opera numa rede de computadores, onde cada nó mantém uma própria cópia e as transações são validadas por protocolos de consenso. Uma das principais características dos SCs e das blockchains é a sua imutabilidade: assim que levarem deploy, os contratos e os blocos da blockchain não podem ser alterados (tecnicamente é possível, mas para tal requere-se medidas extremas, como um fork na blockchain ou a obtenção da cooperação de uma parte substancial dos nós da rede de uma blockchain). No entanto, vulnerabilidades ainda podem existir no código dos SCs, potencialmente resultando em falhas que podem levar à perda de valores. Para lidar com estes problemas, domain-specific languages (DSLs) estão em desenvolvimento para oferecer garantias de segurança aos programadores. No entanto, nenhuma dessas linguagens pode oferecer prova absoluta da correção do contrato, deixando em aberto vários caminhos melhorias no desenvolvimento de SCs. Esta tese tem como objetivo contribuir para o processo de elaboração de SCs, intro- duzindo uma linguagem cuja finalidade é capturar o comportamento destes. Além dessa linguagem, também foram desenvolvidos mecanismos de ferramentas capazes de realizar validações estáticas sobre o comportamento dos SCs existentes, garantindo alinhamento com os efeitos pretendidos do contrato , reforçando assim a auditabilidade dos SCs.
A caracterização de um SC consiste em descrever acordos entre várias partes envolvidas, que podem ser mantidos autonomamente sem a necessidade de um intermediário de confiança. Os SCs são armazenados e executados na Blockchain, uma digital ledger descentralizada tendo como função registar transações de maneira segura e transparente. A blockchain opera numa rede de computadores, onde cada nó mantém uma própria cópia e as transações são validadas por protocolos de consenso. Uma das principais características dos SCs e das blockchains é a sua imutabilidade: assim que levarem deploy, os contratos e os blocos da blockchain não podem ser alterados (tecnicamente é possível, mas para tal requere-se medidas extremas, como um fork na blockchain ou a obtenção da cooperação de uma parte substancial dos nós da rede de uma blockchain). No entanto, vulnerabilidades ainda podem existir no código dos SCs, potencialmente resultando em falhas que podem levar à perda de valores. Para lidar com estes problemas, domain-specific languages (DSLs) estão em desenvolvimento para oferecer garantias de segurança aos programadores. No entanto, nenhuma dessas linguagens pode oferecer prova absoluta da correção do contrato, deixando em aberto vários caminhos melhorias no desenvolvimento de SCs. Esta tese tem como objetivo contribuir para o processo de elaboração de SCs, intro- duzindo uma linguagem cuja finalidade é capturar o comportamento destes. Além dessa linguagem, também foram desenvolvidos mecanismos de ferramentas capazes de realizar validações estáticas sobre o comportamento dos SCs existentes, garantindo alinhamento com os efeitos pretendidos do contrato , reforçando assim a auditabilidade dos SCs.