Semantic Properties of Ethereum Bytecode based on Static Analysis

Abstract

Blockchain has gained significant attention in recent years, with smart contracts enabling automated and trustless financial interactions such as decentralized exchanges, tokenized assets, and on-chain governance. Because these programs often control assets of substantial value, a large body of research has focused on detecting security vulnerabilities in smart contracts. However, beyond security, understanding the actual behavior of a contract remains challenging, particularly when source code is unavailable. This work addresses the identification of semantic properties, defined as behavior-level characteristics that describe a contract's purpose based on its state changes and interactions. Detecting such properties can support applications such as regulatory analysis of relevant contracts and the simplification of contract logic by filtering semantically uninformative boilerplate code. The work focuses on static analysis approaches utilizing Datalog.The methodology first includes a systematic literature review to identify existing approaches for the static analysis of Ethereum bytecode using Datalog, as well as related work on semantic properties. The review indicates that Gigahorse is currently the most prominent tool in this category; consequently, it was selected as the basis for the following analysis.Based on this foundation, several function-level properties are defined, including authenticated functions as well as different types of setter and getter functions. In addition, a contract-level property representing a simple token contract is defined. Detection mechanisms for these properties are implemented in Datalog and subsequently evaluated. The results indicate that Gigahorse is generally well-suited for detecting such semantic properties, although practical limitations were encountered, particularly in the form of limited or missing documentation.