Cross-chain Smart Contracts and dApps Verification by Static Analysis: Limits and Challenges

The increasing demand for interoperability, security, and reliability among various blockchain ecosystems has necessitated the development of cross-chain verification techniques. Static analysis, a powerful tool in software development, offers a promising approach to identify bugs, vulnerabilities, and inconsistencies in cross-chain software during its early stages. By detecting these issues proactively, static analysis can significantly reduce development costs, time-to-market, and the risk of deploying immutable, buggy smart contracts. However, providing adequate verification for cross-chain software is not straightforward. It involves analyzing diverse components, understanding complex program behaviors, interpreting different instruction semantics, and navigating the intricacies of various programming languages. This paper aims to provide a comprehensive overview of interoperability in the blockchain context. We delve into the state-of-the-art regarding verification tools specifically designed for cross-chain software and explore the known issues that these tools can effectively detect. Furthermore, we highlight potential pitfalls and challenges associated with static analysis in this domain, offering insights into the complexities and limitations of this approach.