sVerify: Verifying Smart Contracts Through Lazy Annotation and Learning

Bo Gao; Ling Shi; Jiaying Li; Jialiang Chang; Jun Sun; Zijiang Yang

doi:10.1007/978-3-030-89159-6_28

sVerify: Verifying Smart Contracts Through Lazy Annotation and Learning

Bo Gao
, Ling Shi
, Jiaying Li
, Jialiang Chang
, Jun Sun
, Zijiang Yang

电子与信息学部

Singapore University of Technology and Design
Singapore Management University
Western Michigan University

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

3 引用（Scopus）

摘要

Smart contracts have recently attracted much attention from industry as they aim to assure anonymous distributed secure transactions. It also becomes clear that they are not immune to code vulnerabilities. As smart contracts cannot be patched once deployed, it is crucial to verify their correctness before deployment. Existing approaches mainly focus on testing and bounded verification which do not guarantee the correctness of smart contracts. In this work, we develop a formal verifier called sVerify for Solidity smart contracts based on a combination of lazy annotation and automatic loop invariant learning techniques. The latter is essential as explicit or implicit loops (due to fallback function calls) are common in smart contracts. Patterns and features which are specific to smart contracts are used to facilitate invariant learning. sVerify has been evaluated with 4670 Solidity smart contracts, and the evaluation result shows that sVerify is effective and reasonably efficient for verifying smart contracts.

源语言	英语
主期刊名	Leveraging Applications of Formal Methods, Verification and Validation - 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Proceedings
编辑	Tiziana Margaria, Tiziana Margaria, Bernhard Steffen
出版商	Springer Science and Business Media Deutschland GmbH
页	453-469
页数	17
ISBN（印刷版）	9783030891589
DOI	https://doi.org/10.1007/978-3-030-89159-6_28
出版状态	已出版 - 2021
活动	10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021 - Rhodes, 希腊期限: 17 10月 2021 → 29 10月 2021

出版系列

姓名	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
卷	13036 LNCS
ISSN（印刷版）	0302-9743
ISSN（电子版）	1611-3349

会议

会议	10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021
国家/地区	希腊
市	Rhodes
时期	17/10/21 → 29/10/21

访问文件

10.1007/978-3-030-89159-6_28

其它文件与链接

链接到 Scopus 的出版物

引用此

Gao, B., Shi, L., Li, J., Chang, J., Sun, J., & Yang, Z. (2021). sVerify: Verifying Smart Contracts Through Lazy Annotation and Learning. 在 T. Margaria, T. Margaria, & B. Steffen (编辑), Leveraging Applications of Formal Methods, Verification and Validation - 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Proceedings (页码 453-469). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 卷 13036 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-89159-6_28

Gao, Bo ; Shi, Ling ; Li, Jiaying 等. / sVerify : Verifying Smart Contracts Through Lazy Annotation and Learning. Leveraging Applications of Formal Methods, Verification and Validation - 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Proceedings. 编辑 / Tiziana Margaria ; Tiziana Margaria ; Bernhard Steffen. Springer Science and Business Media Deutschland GmbH, 2021. 页码 453-469 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{61c5ef84a26e4c949bab4088838a720f,

title = "sVerify: Verifying Smart Contracts Through Lazy Annotation and Learning",

abstract = "Smart contracts have recently attracted much attention from industry as they aim to assure anonymous distributed secure transactions. It also becomes clear that they are not immune to code vulnerabilities. As smart contracts cannot be patched once deployed, it is crucial to verify their correctness before deployment. Existing approaches mainly focus on testing and bounded verification which do not guarantee the correctness of smart contracts. In this work, we develop a formal verifier called sVerify for Solidity smart contracts based on a combination of lazy annotation and automatic loop invariant learning techniques. The latter is essential as explicit or implicit loops (due to fallback function calls) are common in smart contracts. Patterns and features which are specific to smart contracts are used to facilitate invariant learning. sVerify has been evaluated with 4670 Solidity smart contracts, and the evaluation result shows that sVerify is effective and reasonably efficient for verifying smart contracts.",

keywords = "Loop invariant learning, Smart contracts, Verification",

author = "Bo Gao and Ling Shi and Jiaying Li and Jialiang Chang and Jun Sun and Zijiang Yang",

note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021 ; Conference date: 17-10-2021 Through 29-10-2021",

year = "2021",

doi = "10.1007/978-3-030-89159-6\_28",

language = "英语",

isbn = "9783030891589",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "453--469",

editor = "Tiziana Margaria and Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation - 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Proceedings",

}

Gao, B, Shi, L, Li, J, Chang, J, Sun, J & Yang, Z 2021, sVerify: Verifying Smart Contracts Through Lazy Annotation and Learning. 在 T Margaria, T Margaria & B Steffen (编辑), Leveraging Applications of Formal Methods, Verification and Validation - 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 卷 13036 LNCS, Springer Science and Business Media Deutschland GmbH, 页码 453-469, 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Rhodes, 希腊, 17/10/21. https://doi.org/10.1007/978-3-030-89159-6_28

sVerify: Verifying Smart Contracts Through Lazy Annotation and Learning. / Gao, Bo; Shi, Ling; Li, Jiaying 等.
Leveraging Applications of Formal Methods, Verification and Validation - 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Proceedings. 编辑 / Tiziana Margaria; Tiziana Margaria; Bernhard Steffen. Springer Science and Business Media Deutschland GmbH, 2021. 页码 453-469 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 卷 13036 LNCS).

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

TY - GEN

T1 - sVerify

T2 - 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021

AU - Gao, Bo

AU - Shi, Ling

AU - Li, Jiaying

AU - Chang, Jialiang

AU - Sun, Jun

AU - Yang, Zijiang

PY - 2021

Y1 - 2021

N2 - Smart contracts have recently attracted much attention from industry as they aim to assure anonymous distributed secure transactions. It also becomes clear that they are not immune to code vulnerabilities. As smart contracts cannot be patched once deployed, it is crucial to verify their correctness before deployment. Existing approaches mainly focus on testing and bounded verification which do not guarantee the correctness of smart contracts. In this work, we develop a formal verifier called sVerify for Solidity smart contracts based on a combination of lazy annotation and automatic loop invariant learning techniques. The latter is essential as explicit or implicit loops (due to fallback function calls) are common in smart contracts. Patterns and features which are specific to smart contracts are used to facilitate invariant learning. sVerify has been evaluated with 4670 Solidity smart contracts, and the evaluation result shows that sVerify is effective and reasonably efficient for verifying smart contracts.

AB - Smart contracts have recently attracted much attention from industry as they aim to assure anonymous distributed secure transactions. It also becomes clear that they are not immune to code vulnerabilities. As smart contracts cannot be patched once deployed, it is crucial to verify their correctness before deployment. Existing approaches mainly focus on testing and bounded verification which do not guarantee the correctness of smart contracts. In this work, we develop a formal verifier called sVerify for Solidity smart contracts based on a combination of lazy annotation and automatic loop invariant learning techniques. The latter is essential as explicit or implicit loops (due to fallback function calls) are common in smart contracts. Patterns and features which are specific to smart contracts are used to facilitate invariant learning. sVerify has been evaluated with 4670 Solidity smart contracts, and the evaluation result shows that sVerify is effective and reasonably efficient for verifying smart contracts.

KW - Loop invariant learning

KW - Smart contracts

KW - Verification

UR - https://www.scopus.com/pages/publications/85118126945

U2 - 10.1007/978-3-030-89159-6_28

DO - 10.1007/978-3-030-89159-6_28

M3 - 会议稿件

AN - SCOPUS:85118126945

SN - 9783030891589

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 453

EP - 469

BT - Leveraging Applications of Formal Methods, Verification and Validation - 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Proceedings

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer Science and Business Media Deutschland GmbH

Y2 - 17 October 2021 through 29 October 2021

ER -

Gao B, Shi L, Li J, Chang J, Sun J, Yang Z. sVerify: Verifying Smart Contracts Through Lazy Annotation and Learning. 在 Margaria T, Margaria T, Steffen B, 编辑, Leveraging Applications of Formal Methods, Verification and Validation - 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Proceedings. Springer Science and Business Media Deutschland GmbH. 2021. 页码 453-469. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-89159-6_28

sVerify: Verifying Smart Contracts Through Lazy Annotation and Learning

摘要

出版系列

会议

访问文件

其它文件与链接

学术指纹

引用此