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.

Sound static analysis allows one to overapproximate all possible program executions to infer various properties. However, it requires quite some effort to formalize and prove the soundness of program semantics. Most software applications developed nowadays are distributed systems in which different [micro]services communicate through synchronous and asynchronous mechanisms. These applications are composed of programs developed in many programming languages and rely on many technologies. However, sound static analysis might be particularly promising in distributed architectures, where exhaustively (or even partially) testing such systems is often prohibitive. This paper presents our ongoing work on applying LiSA (Library for Static Analysis) to microservices. So far, our effort has focused on one programming language (Python), a few libraries (ROS2, pika, FastAPI, Django), and the architectural reconstruction of distributed applications. However, it already shows some promising results and general patterns that might be followed to develop such analyses.

Cybersecurity in mission-critical robotic applications is a necessity to scale deployments securely. ROS2 builds upon DDS-Security specs in ROS Client Library (RCL) to implement its security features. Utilizing SROS2, developers have access to a set of utilities to help set up security in a way RCL can use. Through SROS2, security deployment is eased for developers. However, while access control is handled by DDS and consequently based on the SROS2-generated permission artifacts, the necessary authorization policies are manually generated by developers. This requires an entire system exercise to be sampled via live extraction and, per each node, list all the necessary Topics, Services, and Actions, which is a daunting and laborious process. Developers first have to generate tests. Then, they obtain a ’snapshot’ of the system for each test. Later, these snapshots must be collected and grouped into a policy by a minimum set of rules. All this procedure is quite error-prone. This paper introduces LiSA4ROS2, a tool for automatically extract the ROS2 computational graph via static analysis to derive a minimal correct configuration for ROS2 security policies. Our approach relies on the abstract interpretation theory to statically overapproximate all possible executions to extract a minimal and complete configuration per node. We evaluate our approach with minimal examples covering all the main communication patterns in ROS2 tutorials and all publicly available real-world ROS2 Python systems extracted from GitHub. The results of the minimal examples show that LiSA4ROS2 precisely supports all the main communication patterns. The extensive evaluation underlines that our prototype implementation of the analysis in LiSA4ROS2 is already able to precisely analyze 66% of existing repositories, automatically producing detailed computational graphs and access policies. All the results of the analysis, as well as a Docker artifact to reproduce them, are publicly available.

Abstract In this paper, we introduce Tarsis, a new abstract domain based on the abstract interpretation theory that approximates string values through finite state automata. The main novelty of Tarsis is that it works over an alphabet of strings instead of single characters. On the one hand, such an approach requires a more complex and refined definition of the lattice operators and of the abstract semantics of string operators. On the other hand, it is in position to obtain strictly more precise results than state‐of‐the‐art approaches. We compare Tarsis both with simpler domains and with the standard automata model, targeting case studies containing standard yet challenging string manipulations. The performance gain w.r.t. the standard automata model is also assessed, measuring the speed‐up gained by Tarsis. Experiments confirm that Tarsis can obtain precise results without incurring in excessive computational costs.

Robot Operating System 2 (ROS 2) is the de-facto standard framework for developing distributed robotic applications. However, ensuring the correctness and security of these applications remains a significant challenge. This paper presents a novel approach to statically analyze ROS 2 applications using abstract interpretation. By extracting the architecture graph of the application, our method derives minimal access control policies that can be used to leverage security. We implemented our approach using the Library for Static Analysis (LiSA), providing a toolset that facilitates the development of sound static analyzers for ROS 2. The results demonstrate the effectiveness of our approach in enhancing the security of ROS 2 applications.