Contributions to Proceedings:
I. Grishchenko, C. Schneidewind, M. Maffei:
"A Semantic Framework for the Security Analysis of Ethereum smart contracts.";
in: "Principles of Security and Trust",
issued by: Springer Link;
Smart contracts are programs running on cryptocurrency
(e.g., Ethereum) blockchains, whose popularity stem from the possibility
to perform financial transactions, such as payments and auctions, in a
distributed environment without need for any trusted third party. Given
their financial nature, bugs or vulnerabilities in these programs may
lead to catastrophic consequences, as witnessed by recent attacks. Unfor-
tunately, programming smart contracts is a delicate task that requires
strong expertise: Ethereum smart contracts are written in Solidity, a ded-
in the EVM bytecode format. In order to rigorously verify the security of
smart contracts, it is of paramount importance to formalize their seman-
tics as well as the security properties of interest, in particular at the level
of the bytecode being executed.
In this paper, we present the first complete small-step semantics of
EVM bytecode, which we formalize in the F* proof assistant, obtain-
ing executable code that we successfully validate against the official
Ethereum test suite. Furthermore, we formally define for the first time
a number of central security properties for smart contracts, such as call
integrity, atomicity, and independence from miner controlled parameters.
This formalization relies on a combination of hyper- and safety proper-
ties. Along this work, we identified various mistakes and imprecisions in
existing semantics and verification tools for Ethereum smart contracts,
thereby demonstrating once more the importance of rigorous semantic
foundations for the design of security verification techniques.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.