The recent growth of the blockchain technology market puts its main cryptocurrencies in the spotlight. Among them, Ethereum stands out due to its virtual machine (EVM) supporting smart contracts, i.e., distributed programs that control the flow of the digital currency Ether. Being written in a Turing complete language, Ethereum smart contracts allow for expressing a broad spectrum of financial applications. The price for this expressiveness, however, is a significant semantic complexity, which increases the risk of programming errors. Recent attacks exploiting bugs in smart contract implementations call for the design of formal verification techniques for smart contracts. This, however, requires rigorous semantic foundations, a formal characterization of the expected security properties, and dedicated abstraction techniques tailored to the specific EVM semantics. This work will overview the state-of-the-art in smart contract verification, covering formal semantics, security definitions, and verification tools. We will then focus on EtherTrust , a framework for the static analysis of Ethereum smart contracts which includes the first complete small-step semantics of EVM bytecode, the first formal characterization of a large class of security properties for smart contracts, and the first static analysis for EVM bytecode that comes with a proof of soundness.
This paper focuses on the smart contract of Ethereum, which indirectly controls ETH. Ethereum smart contracts are written in a Turing complete language, so it's complex at the semantic level. This paper discussed in detail the foundations of EtherTrust, it’s the first sound static analyzer for EVM bytecode. In my opinion, this paper plays an important role in learning the security of smart contracts.
As we all know, smart contracts are extremely important for Ethereum. In this paper, it first overviewed the formal verification approvals, then presented a systematization of the state-of-the-art in Ethereum smart contract verification and outlined the open challenges in this field, and it discussed in detail the foundations of EtherTrust, it also reviewed how the small-step semantics presented. Finally it presented how single-entrancy a relevant smart contract security property is expressed in terms of queries, which can be then automatically solved leveraging the power of an SMT solver. This paper has made a great contribution to the security of smart contracts.