Foundational Verification of Smart Contracts through Verified Compilation
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913350311477248 |
|---|---|
| author | Sjöberg, Vilhelm Dave, Kinnari Britten, Daniel Schett, Maria A Sun, Xinyuan Wang, Qinshi Anderson, Sean Noble Reeves, Steve Shao, Zhong |
| author_facet | Sjöberg, Vilhelm Dave, Kinnari Britten, Daniel Schett, Maria A Sun, Xinyuan Wang, Qinshi Anderson, Sean Noble Reeves, Steve Shao, Zhong |
| contents | Programs executed on a blockchain - smart contracts - have high financial stakes; their correctness is crucial. We argue, that this correctness needs to be foundational: correctness needs to be based on the operational semantics of their execution environment. In this work we present a foundational system - the DeepSEA system - targeting the Ethereum blockchain as the largest smart contract platform. The DeepSEA system has a small but sufficiently rich programming language amenable for verification, the DeepSEA language, and a verified DeepSEA compiler. Together they enable true end-to-end verification for smart contracts. We demonstrate usability through two case studies: a realistic contract for Decentralized Finance and contract for crowdfunding. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_08348 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Foundational Verification of Smart Contracts through Verified Compilation Sjöberg, Vilhelm Dave, Kinnari Britten, Daniel Schett, Maria A Sun, Xinyuan Wang, Qinshi Anderson, Sean Noble Reeves, Steve Shao, Zhong Programming Languages F.3.1; F.3.2 Programs executed on a blockchain - smart contracts - have high financial stakes; their correctness is crucial. We argue, that this correctness needs to be foundational: correctness needs to be based on the operational semantics of their execution environment. In this work we present a foundational system - the DeepSEA system - targeting the Ethereum blockchain as the largest smart contract platform. The DeepSEA system has a small but sufficiently rich programming language amenable for verification, the DeepSEA language, and a verified DeepSEA compiler. Together they enable true end-to-end verification for smart contracts. We demonstrate usability through two case studies: a realistic contract for Decentralized Finance and contract for crowdfunding. |
| title | Foundational Verification of Smart Contracts through Verified Compilation |
| topic | Programming Languages F.3.1; F.3.2 |
| url | https://arxiv.org/abs/2405.08348 |