A carregar...
Publicação
Smart Types for Smart Contracts Validation
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 6.9 MB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
The notion of Smart Contracts consist in describing agreements between two or more
parties that can be automatically enforced without a trusted intermediary. Smart Con-
tracts run on a very specific network of peers called Blockchain, a a digitally distributed,
decentralized, public ledger that exists across a network. Potential conflicts are resolved
by the network’s consensus protocol.
The Blockchain [26] is immutable, this means that once a Smart Contract is deployed
on the Blockchain it cannot be amended. This immutability (despite being one important
selling point of Smart Contracts) leave no room for mistakes in their implementation.
Many contracts are hard to implement correctly and bugs and vulnerabilities can be
exploited for erroneous or even fraudulent behaviour.
The countless advantages and applications of Smart contracts are constantly increas-
ing their popularity. This added to the fact that Smart Contracts manipulate resources
with monetary value is bringing a lot of attention to attackers. There are a lot of infamous
Smart Contracts attacks, the DAO Attack per example drained millions of dollars in Ether
(cryptocurrency of Ethereum).
Mainstream tools used to develop distributed Smart Contracts do not address these
requirements. Consequently, many vulnerabilities of these contracts are known and can
be exploited.
In order to help developers to design safer contracts that follow their protocols and
specifications we propose a language integrated with assertions and a static behavioural
type system able of protecting resources and enforce usage protocols to ensure the safety
and soundness in Smart Contracts execution.
Since proof assistants are too demanding for most developers, there is a need for
automatic tools well integrated with programming languages. Therefore, we joined our
language with a model-checker to discharge to it the quantitative assertions during the
compilation process. In short, we provided a translation of the types and assertions to an
automaton in the format of Cubicle’s (model checker) input language and used this one
to conduct Software Verification.
Descrição
Palavras-chave
Smart Contracts Blockchain programming Languages safety Soundness Typechecking