【Author】
Bhargavan, Karthikeyan; Delignat-Lavaud, Antoine; Fournet, Cedric; Gollamudi, Anitha; Gonthier, Georges; Kobeissi, Nadim; Kulatova, Natalia; Rastogi, Aseem; Sibut-Pinote, Thomas; Swamy, Nikhil; Zanella-Beguelin, Santiago
【Source】PROCEEDINGS OF THE 2016 ACM WORKSHOP ON PROGRAMMING LANGUAGES AND ANALYSIS FOR SECURITY (PLAS'16)
【Abstract】Ethereum is a framework for cryptocurrencies which uses blockchain technology to provide an open global computing platform, called the Ethereum Virtual Machine (EVM). EVM executes bytecode on a simple stack machine. Programmers do not usually write EVM code; instead, they can program in a JavaScript-like language, called Solidity, that compiles to bytecode. Since the main purpose of EVM is to execute smart contracts that manage and transfer digital assets (called Ether), security is of paramount importance. However, writing secure smart contracts can be extremely difficult: due to the openness of Ethereum, both programs and pseudonymous users can call into the public methods of other programs, leading to potentially dangerous compositions of trusted and untrusted code. This risk was recently illustrated by an attack on TheDAO contract that exploited subtle details of the EVM semantics to transfer roughly $50M worth of Ether into the control of an attacker. In this paper, we outline a framework to analyze and verify both the runtime safety and the functional correctness of Ethereum contracts by translation to F*, a functional programming language aimed at program verification.
【摘要】以太坊是一个加密货币框架，使用区块链技术提供一个开放的全球计算平台，称为以太坊虚拟机(EVM)。EVM在一个简单的堆栈机器上执行字节码。程序员通常不写EVM代码;相反，他们可以用一种类似javascript的、被称为solid的语言编程，这种语言可以编译成字节码。由于EVM的主要目的是执行管理和转移数字资产(称为Ether)的智能合约，因此安全性至关重要。然而，编写安全的智能合约可能非常困难:由于以太坊的开放性，程序和匿名用户都可以调用其他程序的公共方法，导致可信和不可信代码的潜在危险组合。最近对TheDAO合同的攻击说明了这一风险，该攻击利用EVM语义的微妙细节将价值约5000万美元的Ether转移到攻击者的控制中。在本文中，我们概述了一个框架，通过转换为F*(一种旨在进行程序验证的函数式编程语言)来分析和验证以太坊合约的运行时安全性和功能正确性。
评论