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, ofers 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 diferent 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 efectively detect. Furthermore, we highlight potential pitfalls and challenges associated with static analysis in this domain, ofering insights into the complexities and limitations of this approach.
The rapid digital expansion of recent years has led to a surge in cyber challenges and threats
worldwide [
A blockchain is a decentralized and distributed digital ledger shared among a network that securely records transactions across multiple peers. It operates without a central authority and ensures transparency, anti-tampering, and data immutability. Smart contracts are computer programs that can be deployed, typically in an immutable way, and executed within the blockchain. Decentralized applications (dApps) are applications that run on blockchain and leverage smart contracts to provide decentralized, transparent, and trustless services.
Achieving cross-blockchain interoperability is a non-trivial task due to the heterogeneous
difusion of blockchain solutions and the lack of regulatory standards and unified communication
protocols [
Static analysis allows one to verify software without executing its code, i.e., statically [
The blockchain operates in a trustless environment where blockchain peers and users do not necessarily trust each other. Hence, most blockchains allow the deployment of smart contracts only in an immutable way. Consequently, code fixing and patching may not always be feasible or might be dificult to apply. Thus, static analysis takes a crucial role in the blockchain context. Static analysis helps avoid the immutable deployment of buggy smart contracts by catching issues early. This also minimizes the risk of exploiting vulnerabilities and critical failures of live dApps in blockchain systems. This, in turn, helps to reduce the cost of re-deployment in case of fee-based blockchains.
In this paper, we investigate the current state of verification in cross-chain software. We highlight existing approaches, their limitations, and potential areas for improvement related to static analysis. Furthermore, it briefly overviews cross-chain properties (e.g. bugs, vulnerabilities, and inconsistencies) that can be detected with static analysis.
Paper Structure The rest of the paper is structured as follows. Section 2 ofers an overview of cross-chain environments and the diferent kinds of blockchain interoperability. Section 3 discusses the state-of-art and limitations of the existing verification tools for cross-chain solutions. Section 4 deals with a sound representation of code during analysis. Section 5 investigates interesting properties for cross-chain verification. Finally, Section 6 concludes the paper.
Blockchain interoperability allows diferent blockchain networks to communicate, share data,
and exchange assets with each other. However, achieving seamless interoperability poses
several challenges. In fact, not all blockchains were initially designed for interaction with other
ecosystems. Early blockchains like Bitcoin [
In blockchain, interoperability can be divided into two categories: homogeneous and heterogeneous. The first case means interoperability between blockchains with similar or identical architectures. These blockchains typically share common protocols, consensus mechanisms, or environments, making communicating or sharing data and assets easier. For instance, homogeneous interoperability solutions connect Ethereum-based blockchains such as Ethereum (main-net), Tron, and Polygon. Instead, heterogeneous interoperability refers to the ability of blockchains with diferent architectures, consensus mechanisms, and virtual machines to interact. These blockchains were often built with distinct goals and structures, making cross-chain communication more complex, suitable, and flexible. For instance, heterogeneous interoperability solutions are those that connect Ethereum with Bitcoin, Cosmos, etc.
In recent years, the verification of smart contracts has matured significantly, evolving from rudimentary techniques involving only syntactic checks to sophisticated methodologies that enhance security and reliability by modelling program behaviours and instruction semantics.
Although smart contract verification has moved beyond its infancy, currently, the tools are
mainly focused on individual and mainstream blockchains, making a gap on the less “popular”
ones [18]. According to [
In general, verifying individual components prevents local issues and domain-specific vulnerabilities, but there are issues which could not be discovered by analyzing each program in isolation only [20]. Indeed, this is not suficient also in cross-chain settings where contracts interact with other blockchains and software components outside the blockchain where they are deployed.
To the best of our knowledge, only a few recent studies deal with verifying interoperable
blockchain solutions. Focusing on static analysis, as reported in Table 1, state-of-the-art is
currently limited to homogenous interoperability between Ethereum-based blockchains, and
they consider only events from bridge solutions as cross-chain connectors. No heterogeneous
interoperability and other external solutions are currently covered. For instance, XGuard [21]
extracts and analyzes the semantic information and the source/destination blockchains of
bridging operations from Ethereum-based bridge contracts written in Solidity, a high-level
language for the development of Ethereum smart contracts. To do that, it exploits under the
woods the static analyzer Slither [24] and then provides additional verification modules to
detect inconsistent behaviours. Also, SmartAxe [22] identifies vulnerabilities in cross-chain
bridge smart contracts but written EVM bytecode, a low-level language of Ethereum smart
contracts. It performs control-flow and data-flow analyses to detect issues such as access control
incompleteness and semantic inconsistencies. However, the main drawback of these tools do not
provide guarantees about findings because they sufer from both false positives (i.e. spurious,
not real results) and false negatives (i.e. real results not detected). The reason is that they lack
to properly apply formal methods that allow one to achieve soundness (i.e. absence of false
negatives) or completeness (i.e. absence of false positives) [
Static analysis can also be adopted to support artificial intelligence (AI) approaches. In
particular, according to Ressi et al. [25, 26], static analysis is widely involved in the training
of machine-learning (ML) models to build graph-based representations of the code, such as
the control-flow graphs (CFGs) [
The main step for any efective static analysis is the extraction of an intermediate representation
(IR) from the software to analyse that provides an abstracted form of code that is easier for
analysis tools to work with and typically represents complex programming constructs, structures, and
semantics in a way that is agnostic from the programming language of the software to analyze.
Then, it can be analyzed to infer code properties and to detect bugs, issues, and vulnerabilities.
For instance, the CFG is one of the most used IR in blockchain software verification [
Blockchain B (a) without considering external solutions
BlocAkPAcIshain
Connector
Logic
BlocAkPBcIshain Blockchain A
Blockchain B (b) considering the software of external solutions respect to what one want to analyze, (ii) the IRs are both compatible with the chosen analysis engine, that (iii) the merge points are known, and that (iv) they are soundly computed.
A correct representation of the cross-chain ecosystem is crucial for conducting an efective and reliable analysis. However, cross-chain ecosystems rely on various mechanisms which can increase the complexity of analysis. Omitting non-critical or irrelevant code can improve the performance and eficiency of static analysis by reducing processing time and resource consumption. It can help focus on specific components or high-risk code areas, making the analysis more targeted and manageable. Furthermore, ignoring certain generated or third-party code can prevent unnecessary noise and false positive alerts in the analysis results. However, on the other hand, omitting code may lead to incomplete analysis, potentially missing critical issues or errors. Dependencies and interactions between omitted and analyzed code might be overlooked, leading to incorrect assumptions about the behaviors of the overall system. Then, it is of primary importance to make correct assumptions before to represent the system to analyze.
A typical example of this is whether or not to consider the code of external solutions in the
analyses (see Figure 1). For instance, in a token transfer scenario, diferent blockchains often use
distinct data structures and formats. According to [
Regarding homogeneous interoperability, blockchains typically have the same instruction set, instruction semantics, data types, and code that runs on them, which is also written in the same target blockchain language. Analyzing this type of system is less dificult, as single existing verification tools can be adapted to support the analysis of the entire software and consider the cross-chain bindings and constraints.
This happens diferently if the interoperability is homogeneous but applied by external
solutions (e.g. bridges, relayers, . . . ) or if it is heterogeneous interoperability. In these cases, the
analysis engine is typically required to support and handle diferent components, behaviours,
and programming languages. Indeed, using single tools and merging the tool results is imprecise
and could lead to unsound approaches as well as be potentially unfeasible due to compatibility
issues and technical limitations of the analysis engines. Furthermore, according to [
Interactions to ensure interoperability between diferent blockchains can occur in diferent
ways [
From a program analysis perspective, this may require instrumentations, additional
components, and supporting analytics to correctly extract, compute, and model the merging points.
For instance, the functions called between one contract and another of a cross-chain interaction,
parameters, addresses, and the information exchanged are typically values that can be
hardcoded or declared within the code. However, these values can be manipulated and modified by
instructions and program behaviours depending on the code execution, such as by mathematical
(e.g. addition, subtraction, . . . ) and string (e.g. concatenation, substring, . . . ) operations. Then,
supporting analyses on diferent value domains (e.g. for numbers [
Another aspect to consider is the automation of merging point detection. Given the growing
number of new blockchain frameworks and interoperable paradigms, applying standard models
to statically analyze their code could be potentially unsound and imprecise. However, modifying
or extending the analysis engine for every existing framework to provide automatic checks for
merging points is not sustainable because it may require heavy changes to the analysis engine.
In traditional verification, this problem is similar to that of third-party library support, which is
generally solved by applying specification frameworks [
The computation of an accurate IR is a key point of every static analysis because when it is partial or inaccurate, the analysis results will also be. Indeed, in the worst cases, the analysis might miss properties existing in the real code, leaving potential bugs, issues, and vulnerabilities undetected.
Analyze all possible execution paths and ensure the absence of false negatives means pursuing
the soundness [
In the interoperability settings, it is also necessary to ensure that merging points are computed soundly by approximating potential points in case of lack of information or unknown values. Soundness is typically achieved following a conservative approach where over-approximations on the computations are applied. Although over-approximations may have diferent levels of precision, this approach can introduce spurious results, which lead to false positives, i.e. behaviours that seem possible according to the analysis but which, in reality, cannot occur in any concrete execution of the software. However, in critical contexts such as the blockchain one, it is advisable to have false positives in static analysis rather than to miss the detection of vulnerabilities that, once deployed, may become immutable and pose significant long-term security risks.
Once an adequate representation is achieved, specific analyses can be tailored to detect
crosschain bugs, vulnerabilities, and inconsistencies. A few examples of properties that can be
analyzed statically in cross-chain contexts are reported below:
• Reachability property. It refers to the ability to determine whether a particular state or
condition in a program can be reached during its execution. This property is crucial
in verifying the correctness and security of smart contracts, as well as for cross-chain
software. It helps understand if a code execution from a blockchain can lead to the code
execution in another blockchain and detect potential issues like unauthorized access or
unintended states.
• Data and Numerical properties. The exchange of data is critical in cross-chain blockchain
ecosystems because it may involve diferent blockchains, smart contracts, and
programming languages. Hence, this may lead to diferent data types that require conversions
or modifications to be digested during the cross-chain interactions. In particular,
numerical values are widely adopted for balances, token quantities, transaction counts,
and other numerical attributes. Hence, numerical values may lead to critical issues with
also economic impacts, such as truncation errors due to type conversions or numerical
overflows/underflow [
For instance, time lock mechanisms are widely involved to ensure that both parties
complete their part of the exchange within a set period. Contrary to what happens
for individual smart contracts or cross-contract operations within the same blockchain,
interactions in cross-chains are not possible using the traditional methods to get the
timestamp or block height of the blockchain because they are local with respect to the
blockchain where the code is executed, and they may give diferent results depending
to the blockchain. This may lead to unexpected behaviours and problems. For instance,
in the case of unsynchronized time windows, the payment for a token whose trading
has already expired may occur, which means spending the money without receiving the
token. Then, it is necessary to ensure that the code adopts a trusted oracle that yields
the same value to all the blockchains involved in the cross-chain transfer. The oracle is
typically provided by the external component acting as the connector for the cross-chain
interaction.
• Confidentiality and privacy properties . They may investigate to detect data leakages. For
instance, developers could be interested in detecting the unintentional sharing of sensitive
data in a cross-chain iteration between private and public blockchains. This can be a
classic use case for information flow analysis [
The verification of cross-chain solutions is still in an early stage, presenting numerous challenges and opportunities for improvement. Static analysis can be applied to detect issues and inconsistencies during the software development process, ofering significant advantages by reducing the time and economic costs associated with identifying and fixing bugs. For instance, static analysis tools can detect vulnerabilities in smart contracts or misalignments in crosschain software before they are deployed and before code immutability. However, an efective verification requires a comprehensive approach that considers the entire ecosystem, including homogeneous and heterogeneous interoperabilities among diferent blockchains. It is insuficient to focus solely on individual components or smart contracts with similar characteristics, as the interactions and connections between distinct blockchains are critical to ensuring system and dApps reliability.
To achieve this, the intermediate representations must be computed adequately and soundly, encompassing all potential execution paths, program behaviors, and instruction semantics of the cross-chain software. This allows the analysis to accurately reflects the complexity of cross-chain environments, where minor discrepancies can lead to significant issues in real-world scenarios.
Furthermore, in the evolving cross-chain landscape, there is an urgent need for the establishment of standards and the development of libraries for cross-chain interactions. Such advancements would enable verification tools to identify merging points and interoperability junctions in an automated way. By facilitating the analysis process, these tools could significantly reduce human efort and minimize the risk of oversight, which is particularly valuable given the complexity of cross-chain systems.
In addition to static analysis, formal methods may be employed during the detection of cross-chain properties to provide stronger guarantees such as the soundness.
Work partially supported by SERICS (PE00000014 - CUP H73C2200089001) and iNEST (ECS00000043 – CUP H43C22000540006) projects funded by PNRR NextGeneration EU.
During the preparation of this work, the authors used AI-based tools (Grammarly, ChatGPT ) in order to: Grammar and spelling check, Paraphrase and reword. After using this tool/service, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content. [14] Interchain Foundation., Cosmos network, 2024. https://cosmos.network/ Accessed 09/2024. [15] Web3 Foundation, Polkadot network, 2024. https://polkadot.network/ Accessed 09/2024. [16] I. A. Qasse, M. Abu Talib, Q. Nasir, Inter blockchain communication: A survey, in: Proceedings of the ArabWIC 6th Annual International Conference Research Track, ArabWIC 2019, Association for Computing Machinery, New York, NY, USA, 2019. URL: https://doi.org/10.1145/3333165.3333167. doi:10.1145/3333165.3333167. [17] DefiLlama, Total value locked all chains, 2024. https://defillama.com/chains Accessed 10/2024. [18] L. Olivieri, F. Tagliaferro, V. Arceri, M. Ruaro, L. Negrini, A. Cortesi, P. Ferrara, F. Spoto, E. Talin, Ensuring determinism in blockchain software with golisa: an industrial experience report, SOAP 2022, Association for Computing Machinery, New York, NY, USA, 2022, p. 23–29. doi:10.1145/3520313.3534658, https://doi.org/10.1145/3520313.3534658. [19] P. Ferrara, L. Negrini, V. Arceri, A. Cortesi, Static analysis for dummies: experiencing lisa, in: Proceedings of the 10th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, SOAP 2021, Association for Computing Machinery, New York, NY, USA, 2021, p. 1–6. doi:10.1145/3460946.3464316, https://doi.org/10.1145/3460946. 3464316. [20] A. Mandal, P. Ferrara, Y. Khlyebnikov, A. Cortesi, F. Spoto, Cross-program taint analysis for iot systems, in: Proceedings of the 35th Annual ACM Symposium on Applied Computing, SAC ’20, Association for Computing Machinery, New York, NY, USA, 2020, p. 1944–1952.
URL: https://doi.org/10.1145/3341105.3373924. doi:10.1145/3341105.3373924. [21] K. Wang, Y. Li, C. Wang, J. Gao, Z. Guan, Z. Chen, Xguard: Detecting inconsistency behaviors of crosschain bridges, in: Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, FSE 2024, Association for Computing Machinery, New York, NY, USA, 2024, p. 612–616. URL: https: //doi.org/10.1145/3663529.3663809. doi:10.1145/3663529.3663809. [22] Z. Liao, Y. Nan, H. Liang, S. Hao, J. Zhai, J. Wu, Z. Zheng, Smartaxe: Detecting cross-chain vulnerabilities in bridge smart contracts via fine-grained static analysis, Proc. ACM Softw.
Eng. 1 (2024). URL: https://doi.org/10.1145/3643738. doi:10.1145/3643738. [23] T.-D. Tran, K. A. Vo, D. T. Phan, C. N. Tan, V.-H. Pham, Chainsniper: A machine learning approach for auditing cross-chain smart contracts, in: Proceedings of the 2024 9th International Conference on Intelligent Information Technology, ICIIT ’24, Association for Computing Machinery, New York, NY, USA, 2024, p. 223–230. URL: https://doi.org/10.1145/3654522.3654577. doi:10.1145/3654522.3654577. [24] J. Feist, G. Grieco, A. Groce, Slither: A static analysis framework for smart contracts, in: 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), 2019, pp. 8–15. doi:10.1109/WETSEB.2019.00008. [25] D. Ressi, A. Spanò, L. Benetollo, C. Piazza, M. Bugliesi, S. Rossi, Vulnerability detection in ethereum smart contracts via machine learning: A qualitative analysis, arXiv preprint arXiv:2407.18639 (2024). [26] D. Ressi, R. Romanello, C. Piazza, S. Rossi, Ai-enhanced blockchain technology: A review of advancements and opportunities, Journal of Network and Computer Applications 225 (2024) 103858. URL: https://www.sciencedirect.com/science/article/pii/S1084804524000353. doi:https://doi.org/10.1016/j.jnca.2024.103858.