Security Analysis of Smart Contracts: From Formal Methods to Machine Learning
Badaruddin Chachar · ARCA (Università Ca' Foscari Venezia)
Blockchain smart contracts are immutable programs that often manage high-value assets, making security vulnerabilities a critical concern. Errors introduced at deployment time cannot be easily corrected and may lead to severe financial and operational consequences. This thesis investigates automated techniques for analyzing and detecting vulnerabilities in blockchain smart contracts, with a primary focus on Solidity-based Ethereum contracts and permissioned blockchain systems. The main contribution of this work is a systematic evaluation of Large Language Models (LLMs) for smart contract security analysis, comparing prompt engineering–based in-context learning approaches with task-specific fine-tuning strategies. In realistic multi-label vulnerability detection scenarios—where a single contract may contain multiple concurrent flaws—the thesis shows that fine-tuned models consistently and significantly outperform even advanced prompt engineering techniques, providing higher reliability across vulnerability classes. Multiple prompting paradigms, including Chain-of-Thought–based approaches, are analyzed to highlight their benefits and limitations. Beyond vulnerability detection, the thesis examines broader aspects of blockchain software correctness, including the use of general-purpose programming languages for smart contract development and the detection of concurrency anomalies such as phantom reads in Hyperledger Fabric through formal verification techniques. Overall, this work clarifies when LLMs can be effectively applied to blockchain security and provides practical guidelines for building reliable and reproducible analysis pipelines.