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

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. [ABSTRACT FROM AUTHOR]

Copyright of Innovations in Systems & Software Engineering is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)