【Author】
Grishchenko, Ilya; Maffei, Matteo; Schneidewind, Clara
【Source】COMPUTER AIDED VERIFICATION (CAV 2018), PT I
【Abstract】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 [1], 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.
【摘要】区块链技术市场最近的增长使其主要加密货币成为人们关注的焦点。其中，以太坊因其支持智能合约的虚拟机(EVM)而脱颖而出，即控制数字货币Ether流动的分布式程序。以太坊智能合约是用图灵完整语言编写的，允许表达广泛的金融应用程序。然而，这种表达性的代价是语义的显著复杂性，这增加了编程错误的风险。最近的攻击利用了智能合约实现中的漏洞，要求设计智能合约的形式化验证技术。然而，这需要严格的语义基础、预期安全属性的形式化描述，以及针对特定EVM语义的专用抽象技术。本工作将概述智能合约验证的最新技术，包括形式语义、安全定义和验证工具。然后我们将关注EtherTrust[1]，这是一个静态分析以太坊智能合约的框架，其中包括EVM字节码的第一个完整的小步骤语义，智能合约的一大类安全属性的第一个正式表征，以及第一个对EVM字节码的静态分析，它提供了一个健全的证明。
评论