Developing Secure Bitcoin Contracts with BitML

被引：21

作者：

Atzei, Nicola ^{[1
]}

Bartoletti, Massimo ^{[1
]}

Lande, Stefano ^{[1
]}

Yoshida, Nobuko ^{[2
]}

Zunino, Roberto ^{[3
]}

机构：

[1] Univ Cagliari, Cagliari, Italy

[2] Imperial Coll London, London, England

[3] Univ Trento, Trento, Italy

来源：

ESEC/FSE'2019: PROCEEDINGS OF THE 2019 27TH ACM JOINT MEETING ON EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING | 2019年

基金：

英国工程与自然科学研究理事会;

关键词：

Bitcoin; smart contracts; verification;

D O I：

10.1145/3338906.3341173

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We present a toolchain for developing and verifying smart contracts that can be executed on Bitcoin. The toolchain is based on BitML, a recent domain-specific language for smart contracts with a computationally sound embedding into Bitcoin. Our toolchain automatically verifies relevant properties of contracts, among which liquidity, ensuring that funds do not remain frozen within a contract forever. A compiler is provided to translate BitML contracts into sets of standard Bitcoin transactions: executing a contract corresponds to appending these transactions to the blockchain. We assess our toolchain through a benchmark of representative contracts.

引用

页码：1124 / 1128

页数：5

共 40 条

[11]

Bartoletti Massimo, 2017, Financial Cryptography and Data Security. FC 2017 International Workshops WAHC, BITCOIN, VOTING, WTSC, and TA. Revised Selected Papers: LNCS 10323, P231, DOI 10.1007/978-3-319-70278-0_15

[12]

Bartoletti Massimo, 2019, Principles of Security and Trust. 8th International Conference, POST 2019. Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019. Proceedings: Lecture Notes in Computer Science (11426), P222, DOI 10.1007/978-3-030-17138-4_10

[13]

Bartoletti Massimo, 2018, Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice. 8th International Symposium, ISoLA 2018. Proceedings: Lecture Notes in Computer Science (LNCS 11247), P432, DOI 10.1007/978-3-030-03427-6_32

[14] BitML: A Calculus for Bitcoin Smart Contracts [J].

Bartoletti, Massimo ;

Zunino, Roberto .

PROCEEDINGS OF THE 2018 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (CCS'18), 2018, :83-100

[15]

Bentov I, 2014, LECT NOTES COMPUT SC, V8617, P421, DOI 10.1007/978-3-662-44381-1_24

[16] 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

[17]

Biryukov Alex, 2017, Financial Cryptography and Data Security. FC 2017 International Workshops WAHC, BITCOIN, VOTING, WTSC, and TA. Revised Selected Papers: LNCS 10323, P453, DOI 10.1007/978-3-319-70278-0_28

[18] Maude:: Specification and programming in rewriting logic [J].

Clavel, M ;

Durán, F ;

Eker, S ;

Lincoln, P ;

Martí-Oliet, N ;

Meseguer, J ;

Quesada, JF .

THEORETICAL COMPUTER SCIENCE, 2002, 285 (02) :187-243

[19]

Crary K, 2015, ACM SIGPLAN NOTICES, V50, P479, DOI [10.1145/2737924.2737997, 10.1145/2813885.2737997]

[20] A fair protocol for data trading based on Bitcoin transactions [J].

Delgado-Segura, Sergi ;

Perez-Sola, Cristina ;

Navarro-Arribas, Guillermo ;

Herrera-Joancomarti, Jordi .

FUTURE GENERATION COMPUTER SYSTEMS-THE INTERNATIONAL JOURNAL OF ESCIENCE, 2020, 107 :832-840

← 1 2 3 4 →