一句话：提出 SAFEVM，将 Solidity/EVM 智能合约翻译为 C 程序，借助现有 C 验证引擎验证安全断言与数组访问。
以太坊智能合约公开、不可变且分布，开发者的编程错误容易引入漏洞。本文提出 SAFEVM，一个以太坊智能合约验证工具：它接受 Solidity 源码或编译后的 EVM 字节码，也可带 assert/require 验证注解，并输出验证报告。除通用安全注解外，SAFEVM 还处理数组访问安全，自动生成 SV-COMP 验证断言，使 C 验证引擎能够证明数组访问的安全性。实验从 etherscan.io 收集超过 24,000 个合约，并分别以 CPAchecker、SeaHorn 和 VeryMax 作为后端验证器进行评估。
Ethereum smart contracts are public, immutable and distributed and, as such, they are prone to vulnerabilities sourcing from programming mistakes of developers. This paper presents SAFEVM, a verification tool for Ethereum smart contracts that makes use of state-of-the-art verification engines for C programs. SAFEVM takes as input an Ethereum smart contract (provided either in Solidity source code, or in compiled EVM bytecode), optionally with assert and require verification annotations, and produces in the output a report with the verification results. Besides general safety annotations, SAFEVM handles the verification of array accesses: it automatically generates SV-COMP verification assertions such that C verification engines can prove safety of array accesses. Our experimental evaluation has been undertaken on all contracts pulled from etherscan.io (more than 24,000) by using as back-end verifiers CPAchecker, SeaHorn and VeryMax.
@inproceedings{paperbot5374,
title = {SAFEVM: a safety verifier for Ethereum smart contracts},
author = {Elvira Albert and Jesús Correas and Pablo Gordillo and Guillermo Román-Díez and Albert Rubio},
booktitle = {ISSTA},
year = {2019},
doi = {10.1145/3293882.3338999}
}