Cross-contract invocations (CCIs) in blockchain are essential as they are the backbone mechanism for the communication and cooperation between different smart contracts, allowing the creation of advanced features and increasing the potentiality for decentralized applications. However, a naive implementation may lead to critical pitfalls in permissioned blockchain platforms such as Hyperledger Fabric, where the modular architecture further complicates the analysis of these interactions. In particular, Hyperledger Fabric supports not only CCIs but also the creation of subnetworks within channels, introducing cross-channel CCIs (CCHIs) that could lead to unexpected behaviors and a lack of traceability within the blockchain ecosystem. This paper discusses how to leverage static analysis techniques to design and implement a semantic-based static analysis to detect potential risks related to CCIs in cross-channel scenarios.

Hyperledger Fabric (HF) is currently the one that made blockchain and smart contracts accessible to industries, providing highly customizable solutions for many enterprise use cases. Despite this, programmers are often discouraged from implementing smart contracts due to the high learning curve and security risks of naive smart contract implementations. At the same time, the advent of Large Language Models (LLMs) for code generation led to new possible scenarios such as creating new smart contract applications starting from natural language, allowing to reduce costs and development times. This paper investigates the maturity of LLMs for the code generation of HF smart contracts. In particular, we (i) generate smart contracts written in Go for HF starting from natural language descriptions, (ii) select state-of-the-art static analyzers of Go program, and (iii) perform a quality and security assessment of the generated smart contracts. Our empirical results show current LLMs do not produce high-quality smart contracts, and a relevant effort to debug and patch contracts containing bugs and possible vulnerabilities.

Once deployed in blockchain, smart contracts become immutable: Attackers can exploit bugs and vulnerabilities in their code that cannot be replaced with a bug-free version. For this reason, the verification of smart contracts before they are deployed in blockchain is important. However, the development of verification tools is not easy, especially if one wants to obtain guarantees by using formal methods. This article describes the development, from scratch, of a static analyzer based on abstract interpretation for the verification of real-world Tezos smart contracts. The analyzer is generic with respect to the property under analysis. This article shows taint analysis as a concrete instantiation of the analyzer, at different levels of precision, to detect untrusted cross-contract invocations.

Ethereum enables the creation and execution of decentralized applications through smart contracts, that are compiled to Ethereum Virtual Machine (EVM) bytecode. Once deployed in the blockchain, the bytecode is immutable; hence, ensuring that smart contracts are bug-free before their deployment is of utmost importance. A crucial preliminary step for any effective static analysis of EVM bytecode is the extraction of the control-flow graph (CFG): this presents significant challenges due to potentially statically unknown jump destinations. In this paper we present a novel approach, based on abstract interpretation, aiming at building a sound CFG from EVM bytecode smart contracts. Our analysis, which is implemented in our static analyzer EVMLiSA, is based on a parametric abstract domain that approximates concrete execution stacks at each program point as an l-sized set of abstract stacks of maximal height h; the results of the analysis are then used to resolve the jump destinations at jump nodes. In our preliminary experiments, by fine-tuning the analysis parameters, EVMLiSA builds sound CFGs for all smart contracts where permanent storage-related opcodes do not influence jump destinations.

Abstract Blockchain technology has created a new software development context, with its own peculiarities, mainly due to the guarantees that the technology must satisfy, that is, immutability, distributability, and decentralization of data. Its rapid evolution over the last decade implied a lack of adequate verification tools, exposing developers and users to critical vulnerabilities and bugs. This paper clarifies the extent of block chain-oriented software (BoS), that goes well beyond smart contracts. Moreover, it provides an overview of the challenges related to software verification in the blockchain context, encompassing smart contracts, blockchain layers, cross-chain applications, and, more generally, BoS. This study aims to highlight the shortcomings of the state-of-art and of the state-of-practice of software verification in that context and identify, at the same time, new research directions.

Software security vulnerabilities and leakages of private information are two of the main issues in modern software systems. Several different approaches, ranging from design techniques to run-time monitoring, have been applied to prevent, detect and isolate such vulnerabilities. Static taint analysis has been particularly successful in detecting injection vulnerabilities at compile time. However, its extension to detect leakages of sensitive data has been only partially investigated. In this paper, we introduce BackFlow, a backward flow reconstructor that, starting from the results of a generic taint analysis engine, reconstructs the flow of tainted data. If successful, BackFlow provides full information about the flow that such data (e.g. private information or user input) traversed inside the program before reaching a sensitive point (e.g. Internet communication or execution of an SQL query). Such information is needed to extend taint analysis to privacy analyses, since in such a scenario it is important to know which exact type of sensitive data flows to what type of communication channels. BackFlow has been implemented in Julia (an industrial static analyzer for Java, Android and .NET programs), and applied to WebGoat and different benchmarks to detect both injections and privacy issues. The experimental results prove that BackFlow is able to reconstruct the flow of tainted data for most of the true positives, it scales up to industrial applications, and it can be effectively applied to privacy analysis, such as the detection of sensitive data leaks or compliance with a data regulation.