SSCalc: A Calculus for Solidity Smart Contracts

被引：1

作者：

Marmsoler, Diego ^{[1
]}

Thornton, Billy ^{[1
]}

机构：

[1] Univ Exeter, Exeter, Devon, England

来源：

SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2023 | 2023年 / 14323卷

关键词：

Smart Contracts; Solidity; Program Verification; Isabelle/Solidity;

D O I：

10.1007/978-3-031-47115-5_11

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Smart contracts are programs stored on the blockchain, often developed in a high-level programming language, the most popular of which is Solidity. Smart contracts are used to automate financial transactions and thus bugs can lead to large financial losses. With this paper, we address this problem by describing a verification environment for Solidity in Isabelle/HOL. To this end, we first describe a calculus to reason about Solidity smart contracts. The calculus is formalized in Isabelle/HOL and its soundness is mechanically verified. Then, we describe a Verification Condition Generator to automate the use of the calculus. Our approach can be used to verify the functional correctness of Solidity smart contracts. To demonstrate this, we use it to verify a simple token implemented in Solidity. Our results show that the framework has the potential to significantly reduce the verification effort compared to verifying directly from the semantics.

引用

页码：184 / 204

页数：21

共 44 条

[1] Functional Verification of Smart Contracts via Strong Data Integrity [J].

Ahrendt, Wolfram ;

Bubel, Ralf .

LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: APPLICATIONS, ISOLA 2020, PT III, 2020, 12478 :9-24

[2] Verification of smart contracts: A survey [J].

Almakhour, Mouhamad ;

Sliman, Layth ;

Samhat, Abed Ellatif ;

Mellouk, Abdelhamid .

PERVASIVE AND MOBILE COMPUTING, 2020, 67

[3]

[Anonymous], 2002, Isabelle / HOL: A Proof Assistant for Higher-Order Logic

[4]

Apt K.R., 2009, Texts in Computer Science, V3rd, DOI [DOI 10.1007/978-1-84882-745-5, 10.1007/978-1-84882-745-5]

[5] A Survey of Attacks on Ethereum Smart Contracts (SoK) [J].

Atzei, Nicola ;

Bartoletti, Massimo ;

Cimoli, Tiziana .

PRINCIPLES OF SECURITY AND TRUST (POST 2017), 2017, 10204 :164-186

[6] MedRec: Using Blockchain for Medical Data Access and Permission Management [J].

Azaria, Asaph ;

Ekblaw, Ariel ;

Vieira, Thiago ;

Lippman, Andrew .

PROCEEDINGS 2016 2ND INTERNATIONAL CONFERENCE ON OPEN AND BIG DATA - OBD 2016, 2016, :25-30

[7]

Bahrynovska T., 2017, History of Ethereum Security Vulnerabilities, Hacks and Their Fixes

[8] A Minimal Core Calculus for Solidity Contracts [J].

Bartoletti, Massimo ;

Galletta, Letterio ;

Murgia, Maurizio .

DATA PRIVACY MANAGEMENT, CRYPTOCURRENCIES AND BLOCKCHAIN TECHNOLOGY, 2019, 11737 :233-243

[9]

Batra G., Blockchain 2.0: What's in store for the two ends?

[10]

Berghofer S, 1999, LECT NOTES COMPUT SC, V1690, P19

← 1 2 3 4 5 →