Security Analysis of Smart Contracts: From Formal Methods to Machine Learning

Gli smart contract su blockchain sono programmi immutabili che spesso gestiscono asset di elevato valore, rendendo le vulnerabilità di sicurezza una problematica cruciale. Gli errori introdotti al momento del deploy non possono essere facilmente corretti e possono causare gravi conseguenze finanziarie e operative. Questa tesi studia tecniche automatiche per l’analisi e il rilevamento di vulnerabilità negli smart contract, con particolare attenzione ai contratti Ethereum scritti in Solidity e ai sistemi blockchain permissioned. Il contributo principale consiste in una valutazione sistematica dell’uso dei Large Language Models (LLM) per l’analisi della sicurezza degli smart contract, confrontando approcci basati su prompt engineering e in-context learning con strategie di fine-tuning specifiche per il compito. In scenari realistici di rilevamento multi-label, in cui un singolo contratto può presentare più vulnerabilità simultanee, i modelli fine-tuned dimostrano prestazioni significativamente superiori rispetto anche alle tecniche di prompt engineering più avanzate. Vengono analizzati diversi paradigmi di prompting, inclusi approcci Chain-of-Thought. Oltre al rilevamento delle vulnerabilità, la tesi affronta aspetti più ampi della correttezza del software blockchain, come l’uso di linguaggi di programmazione general-purpose per lo sviluppo di smart contract e l’analisi di anomalie di concorrenza, quali le phantom reads in Hyperledger Fabric, mediante tecniche di verifica formale. Il lavoro fornisce infine linee guida pratiche per l’uso affidabile degli LLM nella sicurezza blockchain.

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.