Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

4-2020

Abstract

Smart contracts can be regarded as one of the most popular blockchain-based applications. The decentralized nature of the blockchain introduces vulnerabilities absent in other programs. Furthermore, it is very difficult, if not impossible, to patch a smart contract after it has been deployed. Therefore, smart contracts must be formally verified before they are deployed on the blockchain to avoid attacks exploiting these vulnerabilities. There is a recent surge of interest in analyzing and verifying smart contracts. While most of the existing works either focus on EVM bytecode or translate Solidity contracts into programs in intermediate languages for analysis and verification, we believe that a direct executable formal semantics of the high-level programming language of smart contracts is necessary to guarantee the validity of the verification. In this work, we propose a generalized formal semantic framework based on a general semantic model of smart contracts. Furthermore, this framework can directly handle smart contracts written in different high-level programming languages through semantic extensions and facilitates the formal verification of security properties with the generated semantics.

Keywords

Blockchain, Smart contracts, Generalized semantic

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of 23rd International Conference on Fundamental Approaches to Software Engineering, FASE 2020, Dublin, Ireland, April 25-30

First Page

75

Last Page

96

Identifier

10.1007%2F978-3-030-45234-6_4

Publisher

Springer

City or Country

Dublin, Ireland

Download

Share

COinS