Description
Ethereum Smart Contracts are executable programs with immutable code,
deployed on a Peer-to-Peer Network. Once deployed, the contract code
cannot be changed to fix bugs. As smart contracts can hold large amounts
of Ether, the electronic currency used in Ethereum, they are popular
targets for exploitation to extract funds.
Ensuring that smart contracts are free of vulnerabilities is thus of
utmost importance and developers must be supported in writing bug-free
code in an easy and understandable way. Formal verification approaches
fail to do so, as they require developers to be experts in formal
constraint definitions and theorem proving. Existing static analysis
approaches, on the other hand, miss many vulnerabilities as they fail to
sufficiently capture the developer's intentions and cannot cope with the
interaction between contracts.
This thesis thus makes a twofold contribution: it provides a concolic
execution framework called "Annotary" and a plugin for the Sublime
editor that first allows developers to state the expected program
behavior in the form of simple annotations within the Solidity contract
code. Second, Annotary applies as symbolic execution approach to analyze
contract code for possible vulnerabilities and unexpected behavior with
respect to the annotations.
In contrast to other scientific work, Annotary correctly captures
interactions with other contracts (inter-contract), and by other
contracts (inter-transactional), and assumes concrete values only when
they can be reasonably trusted. Constraint violations are reported
within the editor with a severity level reflecting the certainty that
the expected behavior can be violated. The proposed annotations are less
expressive than a generic formal verification approach, but focus on
avoiding typical vulnerabilities and security anti-patterns in smart
contracts. The runtime of the analysis is kept to an amount that allows
to use the Annotary framework during the code-compile-test cycle during
development.
|
Thesis topic in co-operation with the Fraunhofer Institute for Applied and Integrated Security AISEC, Garching