  Ethereum smart contracts are distributed programs running on top of the
Ethereum blockchain. Since program flaws can cause significant monetary losses
and can hardly be fixed due to the immutable nature of the blockchain, there is
a strong need of automated analysis tools which provide formal security
guarantees. Designing such analyzers, however, proved to be challenging and
error-prone. We review the existing approaches to automated, sound, static
analysis of Ethereum smart contracts and highlight prevalent issues in the
state of the art. Finally, we overview eThor, a recent static analysis tool
that we developed following a principled design and implementation approach
based on rigorous semantic foundations to overcome the problems of past works.
