论文标题

分析智能合约:从EV​​M到声音控制图

Analyzing Smart Contracts: From EVM to a sound Control-Flow Graph

论文作者

Albert, Elvira, Correas, Jesús, Gordillo, Pablo, Román-Díez, Alejandro Hernández-Cerezo Guillermo, Rubio, Albert

论文摘要

EVM语言是一种简单的基于堆栈的语言,单词为256位,在EVM和其他虚拟机语言之间具有一个重要的差异(例如Java bytecode或for .NET程序):使用堆栈来保存跳跃地址,而不是在跳高说明的代码中阐明它。静态分析仪需要EVM程序的完整控制流程图(CFG),以便能够表示其所有执行路径。本报告解决了通过静态分析获得精确而完整的堆栈敏感CFG的问题,克隆可能使用执行堆栈的不同状态执行的块。证明了分析的健全性。

The EVM language is a simple stack-based language with words of 256 bits, with one significant difference between the EVM and other virtual machine languages (like Java Bytecode or CLI for .Net programs): the use of the stack for saving the jump addresses instead of having it explicit in the code of the jumping instructions. Static analyzers need the complete control flow graph (CFG) of the EVM program in order to be able to represent all its execution paths. This report addresses the problem of obtaining a precise and complete stack-sensitive CFG by means of a static analysis, cloning the blocks that might be executed using different states of the execution stack. The soundness of the analysis presented is proved.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源