IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
复制标题
IELE：严格设计的区块链语言和工具生态系统
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Grigore Roşu
中科院分区：
文献类型：
--
作者：
T. Kasampalis;Dwight Guth;Brandon M. Moore;Traian;Y. Zhang;Daniele Filaretti;V. Serbanuta;Ralph E. Johnson;Grigore Roşu
本文提出了IELE，一种LLVM风格的语言，以及一个用于在区块链上实现和正式推理智能合约的工具生态系统。IELE是通过在K框架中形式化地描述其语义来设计的。它的实现，IELE虚拟机（VM），以及IELE智能合约的正式验证工具，都是从正式规范中自动生成的。自动生成的正式验证工具允许我们正式验证智能合约，而验证者和实际VM之间没有任何差距。从Solidity（智能合约的主要高级语言）到IELE的编译器也已经（手动）实现，因此以太坊合约现在也可以在IELE上执行。
This paper proposes IELE, an LLVM-style language, together with a tool ecosystem for implementing and formally reasoning about smart contracts on the blockchain. IELE was designed by specifying its semantics formally in the K framework. Its implementation, a IELE virtual machine (VM), as well as a formal verification tool for IELE smart contracts, were automatically generated from the formal specification. The automatically generated formal verification tool allows us to formally verify smart contracts without any gap between the verifier and the actual VM. A compiler from Solidity, the predominant high-level language for smart contracts, to IELE has also been (manually) implemented, so Ethereum contracts can now also be executed on IELE.