Foundational Verification of Smart Contracts through Verified Compilation
Abstract
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.
Keywords
Cite
@article{arxiv.2405.08348,
title = {Foundational Verification of Smart Contracts through Verified Compilation},
author = {Vilhelm Sjöberg and Kinnari Dave and Daniel Britten and Maria A Schett and Xinyuan Sun and Qinshi Wang and Sean Noble Anderson and Steve Reeves and Zhong Shao},
journal= {arXiv preprint arXiv:2405.08348},
year = {2024}
}
Comments
27 pages, 6 figures