Scholarlink

<p>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.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

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

  • 期刊论文

  • 发表日期：

    2025年8月29日

查看全文
  • Kartik Kaushik,
  • Raju Halder,
  • Samrat Mondal

摘要

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.