ZEUS: Analyzing Safety of Smart Contracts

被引：363

作者：

Kalra, Sukrit ^{[1
]}

Goel, Seep ^{[1
]}

Dhawan, Mohan ^{[1
]}

Sharma, Subodh ^{[2
]}

机构：

[1] IBM Res, New Delhi, India

[2] IIT Delhi, New Delhi, India

来源：

25TH ANNUAL NETWORK AND DISTRIBUTED SYSTEM SECURITY SYMPOSIUM (NDSS 2018) | 2018年

关键词：

D O I：

10.14722/ndss.2018.23082

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

A smart contract is hard to patch for bugs once it is deployed, irrespective of the money it holds. A recent bug caused losses worth around $50 million of cryptocurrency. We present ZEUS-a framework to verify the correctness and validate the fairness of smart contracts. We consider correctness as adherence to safe programming practices, while fairness is adherence to agreed upon higher-level business logic. ZEUS leverages both abstract interpretation and symbolic model checking, along with the power of constrained horn clauses to quickly verify contracts for safety. We have built a prototype of ZEUS for Ethereum and Fabric blockchain platforms, and evaluated it with over 22.4K smart contracts. Our evaluation indicates that about 94.6% of contracts (containing cryptocurrency worth more than $0.5 billion) are vulnerable. ZEUS is sound with zero false negatives and has a low false positive rate, with an order of magnitude improvement in analysis time as compared to prior art.

引用

页数：15

共 23 条

[1]

Barnat J, CAV 13

[2]

Bauer L, PLDI 05

[3] Formal Verification of Smart Contracts Short Paper [J].

Bhargavan, Karthikeyan ;

Delignat-Lavaud, Antoine ;

Fournet, Cedric ;

Gollamudi, Anitha ;

Gonthier, Georges ;

Kobeissi, Nadim ;

Kulatova, Natalia ;

Rastogi, Aseem ;

Sibut-Pinote, Thomas ;

Swamy, Nikhil ;

Zanella-Beguelin, Santiago .

PROCEEDINGS OF THE 2016 ACM WORKSHOP ON PROGRAMMING LANGUAGES AND ANALYSIS FOR SECURITY (PLAS'16), 2016, :91-96

[4]

Bjorner N, SMT 12

[5]

Bradely A. R, VMCAI 2011

[6] Practical byzantine fault tolerance and proactive recovery [J].

Castro, M ;

Liskov, B .

ACM TRANSACTIONS ON COMPUTER SYSTEMS, 2002, 20 (04) :398-461

[7] Step by Step Towards Creating a Safe Smart Contract: Lessons and Insights from a Cryptocurrency Lab [J].

Delmolino, Kevin ;

Arnett, Mitchell ;

Kosba, Ahmed ;

Miller, Andrew ;

Shi, Elaine .

FINANCIAL CRYPTOGRAPHY AND DATA SECURITY, FC 2016, 2016, 9604 :79-94

[8] IRM enforcement of Java']Java stack inspection [J].

Erlingsson, U ;

Schneider, FB .

2000 IEEE SYMPOSIUM ON SECURITY AND PRIVACY, PROCEEDINGS, 2000, :246-255

[9] Flexible policy-directed code safety [J].

Evans, D ;

Twyman, A .

PROCEEDINGS OF THE 1999 IEEE SYMPOSIUM ON SECURITY AND PRIVACY, 1999, :32-45

[10]

Gurfinkel A., CAV 15

← 1 2 3 →