SolCMC: Solidity Compiler's Model Checker

被引：18

作者：

Alt, Leonardo ^{[1
]}

Blicha, Martin ^{[2
,3
]}

Hyvarinen, Antti E. J. ^{[2
]}

Sharygina, Natasha ^{[2
]}

机构：

[1] Ethereum Fdn, Berlin, Germany

[2] Univ Svizzera Italiana, Lugano, Switzerland

[3] Charles Univ Prague, Prague, Czech Republic

来源：

COMPUTER AIDED VERIFICATION (CAV 2022), PT I | 2022年 / 13371卷

基金：

瑞士国家科学基金会;

关键词：

Ethereum; Solidity; Symbolic model checking; Constrained Horn clauses; Satisfiability modulo theories;

D O I：

10.1007/978-3-031-13185-1_16

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Formally verifying smart contracts is important due to their immutable nature, usual open source licenses, and high financial incentives for exploits. Since 2019 the Ethereum Foundation's Solidity compiler ships with a model checker. The checker, called SolCMC, has two different reasoning engines and tracks closely the development of the Solidity language. We describe SolCMC's architecture and use from the perspective of developers of both smart contracts and tools for software verification, and show how to analyze nontrivial properties of real life contracts in a fully automated manner.

引用

页码：325 / 338

页数：14

共 39 条

[1]

[Anonymous], ACT 0 1 RELEASED

[2] cvc5: A Versatile and Industrial-Strength SMT Solver [J].

Barbosa, Haniel ;

Barrett, Clark ;

Brain, Martin ;

Kremer, Gereon ;

Lachnitt, Hanna ;

Mann, Makai ;

Mohamed, Abdalrhman ;

Mohamed, Mudathir ;

Niemetz, Aina ;

Notzli, Andres ;

Ozdemir, Alex ;

Preiner, Mathias ;

Reynolds, Andrew ;

Sheng, Ying ;

Tinelli, Cesare ;

Zohar, Yoni .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT I, 2022, 13243 :415-442

[3]

Bernardi T., 2020, WIP: finding bugs automatically in smart contracts with parameterized invariants

[4] Horn Clause Solvers for Program Verification [J].

Bjorner, Nikolaj ;

Gurfinkel, Arie ;

McMillan, Ken ;

Rybalchenko, Andrey .

FIELDS OF LOGIC AND COMPUTATION II: ESSAYS DEDICATED TO YURI GUREVICH ON THE OCCASION OF HIS 75TH BIRTHDAY, 2015, 9300 :24-51

[5]

BLASS A, 1987, LECT NOTES COMPUT SC, V270, P20

[6] Verification of the Incremental Merkle Tree Algorithm with Dafny [J].

Cassez, Franck .

FORMAL METHODS, FM 2021, 2021, 13047 :445-462

[7] Z3: An efficient SMT solver [J].

de Moura, Leonardo ;

Bjorner, Nikolaj .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 :337-340

[8]

ethereum, ERC20 DOC

[9]

ethereum, ERC777 DOC

[10]

ethereum, SYMB EX HEVM

← 1 2 3 4 →