Analyzing Safety and Security of Solidity Smart Contracts via Semantics-Preserving Transcompilation

Analyzing Safety and Security of Solidity Smart Contracts via Semantics-Preserving Transcompilation

연구 분야: Analysis

학회: Innovations in Systems and Software Engineering

Solidity is a dominant programming language for developing smart contracts on the Ethereum blockchain, playing a crucial role in today’s decentralized applications. Given the rising frequency of security breaches, the verification of Solidity contracts is becoming increasingly essential. Traditionally, vulnerability assessment and formal methods mostly leverage off-the-shelf tools designed for languages other than Solidity by transcompiling the Solidity code into compatible languages. However, Java, known for its comprehensive suite of verification and analysis tools, has seen limited exploration in the context of Solidity. In this paper, we present a semantics-preserving transcompilation of the Solidity language into an equivalent Java counterpart, capturing behavioral aspects of both common and unique Solidity features. We validate the effectiveness of our approach using a set of real Solidity contracts, sourced from OpenZeppelin and Google BigQuery. Further, we showcase the practical benefits of this transcompilation by employing renowned Java testing and analysis tools on the transcompiled code, confirming the potential of integrating Solidity with Java’s robust verification ecosystem.