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.
Wed 17 Jul
| 16:00 - 16:10 Talk | Cong WangTsinghua University, Jian GaoSchool of Software, Tsinghua University, Yu Jiang, Zhenchang XingAustralia National University, Huafeng Zhang, Weiliang Ying , Ming GuTsinghua University, Jiaguang Sun | |||||||||||||||||||||||||||||||||||||||||
| 16:10 - 16:20 Talk | ||||||||||||||||||||||||||||||||||||||||||
| 16:20 - 16:30 Talk | Li ChiTsinghua University, Min ZhouTsinghua University, Zuxing GuSchool of Software, Tsinghua University, Guang Chen, Yuexing Wang, Jiecheng WuTsinghua University, Ming GuTsinghua University | |||||||||||||||||||||||||||||||||||||||||
| 16:30 - 16:40 Talk | ||||||||||||||||||||||||||||||||||||||||||
| 16:40 - 16:50 Talk | ||||||||||||||||||||||||||||||||||||||||||
| 16:50 - 17:00 Talk | Linjie PanInstitute of Software, Chinese Academy of Sciences, Baoquan Cui, Jiwei YanInstitute of Software, Chinese Academy of Sciences, Xutong Ma, Jun YanInstitute of Software, Chinese Academy of Sciences, Jian ZhangBeihang University | |||||||||||||||||||||||||||||||||||||||||
| 17:00 - 17:10 Talk | Rohan PadhyeUniversity of California, Berkeley, Caroline LemieuxUniversity of California, Berkeley, Koushik SenUniversity of California, Berkeley | |||||||||||||||||||||||||||||||||||||||||
| 17:10 - 17:20 Talk | Renaud Rwemalika, Marinos Kintis, Mike PapadakisUniversity of Luxembourg, Yves Le TraonUniversity of Luxembourg, Pierre Lorrach | |||||||||||||||||||||||||||||||||||||||||
| 17:20 - 17:30 Talk | Yuying LiState Key Laboratory for Novel Software Technology, Nanjing University, Rui HaoNanjing University, China, Yang FengUniversity of California, Irvine, James JonesUniversity of California, Irvine, Xiaofang Zhang, Zhenyu ChenNanjing University | |||||||||||||||||||||||||||||||||||||||||