[Back]

I. Grishchenko, C. Schneidewind, M. Maffei:
"A Semantic Framework for the Security Analysis of Ethereum smart contracts.";
in: "Principles of Security and Trust", LNCS 10804; issued by: Springer Link; Springer Open, Schwitzerland, 2018, ISBN: 978-3-319-89721-9, 243 - 269.

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-
icated language resembling JavaScript, and shipped over the blockchain
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.

http://dx.doi.org/10.1007/978-3-319-89722-6_10

https://publik.tuwien.ac.at/files/publik_270458.pdf