Jan Corazza, Ivan Gavran, Gabriela Moreira, Daniel Neider
When blockchain systems are said to be trustless, what this really means is that all the trust is put into software. Thus, there are strong incentives to ensure blockchain software is correct -- vulnerabilities here cost millions and break businesses. One of the most powerful ways of establishing software correctness is by using formal methods. Approaches based on formal methods, however, induce a significant overhead in terms of time and expertise required to successfully employ them. Our work addresses this critical disadvantage by automating the creation of a formal model -- a mathematical abstraction of the software system -- which is often a core task when employing formal methods. We perform model synthesis in three phases: we first transpile the code into model stubs; then we "fill in the blanks" using a large language model (LLM); finally, we iteratively repair the generated model, on both syntactical and semantical level. In this way, we significantly reduce the amount of time necessary to create formal models and increase accessibility of valuable software verification methods that rely on them. The practical context of our work was reducing the time-to-value of using formal models for correctness audits of smart contracts.
Decompiler is a specialized type of reverse engineering tool extensively employed in program analysis tasks, particularly in program comprehension and vulnerability detection. However, current Solidity smart contract decompilers face significant limitations in reconstructing the original source code. In particular, the bottleneck of SOTA decompilers lies in inaccurate function identification, incorrect variable type recovery, and missing contract attributes. These deficiencies hinder downstream tasks and understanding of the program logic. To address these challenges, we propose SmartHalo, a new framework that enhances decompiler output by combining static analysis (SA) and large language models (LLM). SmartHalo leverages the complementary strengths of SA’s accuracy in control and data flow analysis and LLM’s capability in semantic prediction. More specifically, SmartHalo constructs a new data structure - Dependency Graph (DG), to extract semantic dependencies via static analysis. Then, it takes DG to create prompts for LLM optimization. Finally, the correctness of LLM outputs is validated through symbolic execution and formal verification. Evaluation on a dataset consisting of 465 randomly selected smart contract functions shows that SmartHalo significantly improves the quality of the decompiled code, compared to SOTA decompilers (e.g., Gigahorse). Notably, integrating GPT-4o mini with SmartHalo further enhances its performance, achieving a precision of 91.32% and a recall of 87.38% for function boundaries, a precision of 90.40% and a recall of 88.82% for variable types, and a precision of 80.66% and a recall of 91.78% for contract attributes.
S M Mostaq Hossain, Amani Altarawneh, Jesse Roberts
As blockchain technology and smart contracts become widely adopted, securing them throughout every stage of the transaction process is essential. The concern of improved security for smart contracts is to find and detect vulnerabilities using classical Machine Learning (ML) models and fine-tuned Large Language Models (LLM). The robustness of such work rests on a labeled smart contract dataset that includes annotated vulnerabilities on which several LLMs alongside various traditional machine learning algorithms such as DistilBERT model is trained and tested. We train and test machine learning algorithms to classify smart contract codes according to vulnerability types in order to compare model performance. Having fine-tuned the LLMs specifically for smart contract code classification should help in getting better results when detecting several types of well-known vulnerabilities, such as Reentrancy, Integer Overflow, Timestamp Dependency and Dangerous Delegatecall. From our initial experimental results, it can be seen that our fine-tuned LLM surpasses the accuracy of any other model by achieving an accuracy of over 90%, and this advances the existing vulnerability detection benchmarks. Such performance provides a great deal of evidence for LLMs' ability to describe the subtle patterns in the code that traditional ML models could miss. Thus, we compared each of the ML and LLM models to give a good overview of each model's strengths, from which we can choose the most effective one for real-world applications in smart contract security. Our research combines machine learning and large language models to provide a rich and interpretable framework for detecting different smart contract vulnerabilities, which lays a foundation for a more secure blockchain ecosystem.
Smart contract security is a critical concern in the blockchain ecosystem, as vulnerabilities have resulted in billions of dollars in financial losses. This urgency has driven the development of numerous automated security tools; however, their effectiveness is tightly linked to the data on which they are trained and evaluated. In current research practice, datasets vary widely in structure, provenance, and quality, as they are often manually assembled from various sources to satisfy the specific needs of individual studies. Because obtaining verified, real-world vulnerabilities and exploits is challenging, many researchers supplement or replace real data with artificially injected or otherwise synthetic examples. These practices, collectively, lead to evaluation settings that do not fully capture the complexity, diversity, and exploitability of vulnerabilities found in contracts intended for real use. As a result, tool performance is frequently overestimated in academic benchmarks, contributing to a persistent gap between reported results and the practical needs of auditors and developers. This thesis addresses this gap by introducing PoPoC, a novel benchmark dataset built from real-world, verified Proof-of-Concept (PoC) exploits. We present a reproducible workflow for creating this dataset, which begins by scraping 4,770 audit reports from the Solodit platform, filtering for 1,053 reports that contain dedicated PoC sections. These candidates are then automatically enriched with quality metrics using a Large Language Model (LLM) and ranked via a custom priority-scoring heuristic. The core of this work involved a rigorous manual validation of the top 100 ranked audits. This process resulted in a curated dataset of 58 fully reproduced, executable exploits, with each reproduction packaged within a containerized environment to ensure reliability. Our analysis confirms that 100% of the entries in the PoPoC dataset are technically correct. However, we also found that the original PoCs often have inconsistent test oracle coverage (with only 28 of 58 having complete assertions) and that the dataset shows limited platform diversity, being sourced primarily from Code4Arena. The primary contributions of this thesis is the reproducible method to extract and validate exploit PoCs from raw audits, the curated PoPoC dataset, and its accompanying codebase containing PoC reproductions and the vulnerable source code. This work provides the first benchmark to systematically connect formal vulnerability descriptions and vulnerable source code with manually verified, proven, and runnable PoC exploits. PoPoC serves as a high-quality, reproducible foundation for benchmarking security tools, training auditors, and advancing future research in automated vulnerability detection.
Background: Large Language Models (LLMs) like ChatGPT-4 Turbo, Claude 4 Sonnet, and DeepSeek-V3 are foundational to modern AI applications. However, a significant gap exists in understanding the direct link between their technical performance and user engagement, their scalability under concurrent load, and the practical performance cost of emerging privacy-preserving technologies. Objectives: This thesis conducts a holistic evaluation of these three leading LLMs to: (1) Compare their performance across latency, accuracy, and client-side resource utilization, and establish the relationship between these metrics and qualitative user engagement scores in various conversational contexts (RQ1). (2) Determine their scalability limits under concurrent user loads and quantify the performance overhead of integrating a zero-knowledge proof privacy protocol (EZKL) (RQ2). Methods: A custom, containerized Python framework was used to systematically test the models. For RQ1, performance and engagement were evaluated in three structured contexts: multi-turn (testing memory), cohesive (testing consistency), and ethical (testing safety) sessions. For RQ2, scalability was measured using Locust to simulate 25 to 200 concurrent users in both a standard centralized setup and a privacy-enhanced EZKL configuration. Key metrics included throughput (RPS), error rates, latency (median and P99), client-side resource consumption, and ZKP generation/verification times. Results: For RQ1, ChatGPT-4 Turbo emerged as the top generalist, showing the best balance of low latency, high accuracy, and strong engagement scores in dynamic multi-turn sessions (e.g., 7.9 personalization score). Claude 4 Sonnet excelled in specialized tasks, achieving a perfect context-switching score (0.0) in cohesive sessions and the highest Harm Avoidance Score (8.0) in ethical sessions, albeit with higher resource usage. DeepSeek-V3 consistently showed the highest latency and resource consumption, negatively impacting its engagement scores. For RQ2, ChatGPT-4 Turbo was the most scalable, peaking at 210 RPS with the lowest error rate. The integration of the EZKL protocol resulted in a catastrophic performance collapse for all models, with throughput dropping to near-zero and latency increasing to hundreds of thousands of milliseconds, rendering it unviable for real-time applications. Conclusions: The study concludes that model selection is highly use-case dependent: ChatGPT-4 Turbo is optimal for scalable, general-purpose applications; Claude 4 Sonnet is superior for high-stakes tasks requiring safety and precision. The findings empirically demonstrate that superior technical performance is a direct enabler of higher user engagement. Finally, current zero-knowledge proof implementations impose a prohibitive performance cost for interactive, scalable AI systems.
Open access
Artificial Intelligence in Healthcare and Education
Smart contracts frequently fail due to transaction reverts, yet diagnosing the causes of these failures remains challenging. We present an analysis pipeline that automatically extracts and clusters invariants from on-chain reverted transactions, uncovering the underlying conditions that trigger failures. At the core of our approach is ReBERT, a custom embedding model fine-tuned on invariant data, which outperforms existing semantic similarity models in capturing subtle predicate relationships. Our analysis reveals meaningful clusters of failure causes—such as Access Control, Data Flow, and Status Checks—that highlight recurring vulnerabilities in smart contract execution. These findings advance understanding of failure patterns for Ethereum Smart Contracts.
Deep learning-based detectors have been widely proposed to predict vulnerabilities in smart contracts, yet their unreliable predictions pose severe security risks to financial transactions, making it critical to verify the reliability of vulnerability predictions. However, existing methods only produce prediction results, failing to provide an evidence chain to check whether these predicted vulnerabilities genuinely exist and deliver further guidance for fixing the vulnerabilities. Thus, making these vulnerability predictions verifiable remains an unexplored problem. In this paper, we propose SmartGuard, a novel verifiable vulnerability prediction framework for deep learning-based detectors and specifically designed for smart contracts. It integrates a deep learning-based detector with a symbolic prediction validator, where the latter acts as the backend formal engine to verify vulnerability predictions. Specifically, we present a graph-sequence multi-task learning model to detect vulnerabilities while generating transaction sequences that serve as evidence chains, explicitly revealing the triggering logic behind vulnerabilities. To bridge the gap between deep learning-based detectors and symbolic validators, we symbolically execute the generated transaction sequences against the verification conditions of vulnerability predictions. Furthermore, we propose a new metric, Vulnerability Prediction Suspiciousness (VPS), to evaluate the reliability of the predicted results. We implement SmartGuard on three representative types of vulnerabilities (Reentrancy, Ether-leaking, and Suicidal) to evaluate its performance in real-world scenarios. Our experimental results show that SmartGuard can effectively verify doubtful vulnerability predictions in real-world scenarios. It also outperforms state-of-the-art baselines by consistently reducing false reports by at least 15% across various Solidity versions. Case studies on complex contracts and DApps further demonstrate SmartGuard’s effectiveness in practice.
The rapid expansion of the digital economy heightens the need for privacy and trust in intellectual property transactions. Traditional centralised approaches to identifying legal conflicts in intellectual property contracts are prone to data leakage and fail to balance transparency with confidentiality. This paper proposes a self-identification method for legal conflicts in intellectual property contracts using zero-knowledge proofs. By combining a light gradient boosting machine learning model with the zero-knowledge succinct non-interactive argument of knowledge protocol, our approach allows verifiable detection of potential legal conflicts without revealing sensitive information. Experiments on the US patent and trademark office patent dataset demonstrate that the method achieves high performance in conflict prediction (area under the receiver operating characteristic curve = 0.872) and verification efficiency (<10 ms), providing a novel and practical framework for privacy-aware legal technology.
Mr.Sandeep Bhimrao Mohite, Mr. Ayush Katkar, M. S. Patil, Miss. Pallavi Powar · 5 authors
Abstract: The decentralized legal record management platform facilitates a seamless transition from centralized to decentralized systems by leveraging blockchain technology. Blockchain offers numerous benefits, including increased transparency, immutability, and efficiency in legal record management. This project report delves into the development and implementation of a Decentralized Legal Record Platform using blockchain Technology, aiming to address inefficiencies and lack of transparency in traditional legal record-keeping systems. By harnessing blockchain's decentralized architecture and cryptographic security features, the platform ensures tamper-proof documentation, transparent access, and improved accuracy of the data. The distributed ledger technology of blockchain reduces the need for intermediaries, which lowers the possibility of fraudulent activity thus providing a reliable audit trail for legal proceedings. Moreover, blockchain enhances efficiency by automating processes and enabling real-time access to legal records, fostering trust and accountability within the legal ecosystem. This project explores the technical aspects of blockchain integration and its implications for legal record-keeping, ultimately paving the path for an ecosystem of legal documents that is safer and more effective
Due to the inherent immutability of blockchain technology, smart contract updates require their deployment at new addresses rather than modifying existing ones, thus fragmenting version histories and creating critical blind spots for analyses. Indeed, for example, this fragmentation severely hinders security researchers ability to track vulnerability lifecycles across contract versions. While platforms like Etherscan provide detailed information about Ethereum smart contracts, they lack crucial functionality to trace predecessor-successor relationships within smart contract lineages, preventing systematic analysis of how vulnerabilities emerge, propagate, and potentially remain unresolved across versions.To address the challenge of tracing smart contract lineages, we adopt a Design Science Research (DSR) approach and introduce ContractTrace, an automated infrastructure that accurately identifies and links versions of smart contracts into coherent lineages. This tool enables the construction of lineageSet, an up-to-date, open-source dataset specifically designed to support security research on vulnerability, defect or any other property evolution patterns in smart contracts. Through a security-focused case study we demonstrate how ContractTrace reveals previously obscured vulnerability life-cycles within smart contract lineages, tracking whether critical security flaws persist or get resolved across versions. This capability is essential for understanding vulnerability propagation patterns and evaluating the effectiveness of security patches in blockchain environments. In the evaluation phase of our DSR approach, we validated our lineage detection methodology against an alternative approach using Locality-Sensitive Hashing (LSH) to cluster contract versions, confirming the security relevance and accuracy of our technique.
Xiaolin Wen, Tai D. Nguyen, Lun Zhang, Jun Sun · 5 authors
Smart contracts are the fundamental components of blockchain technology. They are programs to determine cryptocurrency transactions, and are irreversible once deployed, making it crucial for cryptocurrency investors to understand the cryptocurrency transaction behaviors of smart contracts comprehensively. However, it is a challenging (if not impossible) task for investors, as they do not necessarily have a programming background to check the complex source code. Even for investors with certain programming skills, inferring all the potential behaviors from the code alone is still difficult, since the actual behaviors can be different when different investors are involved. To address this challenge, we propose PrettiSmart, a novel visualization approach via execution simulation to achieve intuitive and reliable visual interpretation of smart contracts. Specifically, we develop a simulator to comprehensively capture most of the possible real-world smart contract behaviors, involving multiple investors and various smart contract functions. Then, we present PrettiSmart to intuitively visualize the simulation results of a smart contract, which consists of two modules: The Simulation Overview Module is a barcode-based design, providing a visual summary for each simulation, and the Simulation Detail Module is an augmented sequential design to display the cryptocurrency transaction details in each simulation, such as function call sequences, cryptocurrency flows, and state variable changes. It can allow investors to intuitively inspect and understand how a smart contract will work. We evaluate PrettiSmart through two case studies and in-depth user interviews with 12 investors. The results demonstrate the effectiveness and usability of PrettiSmart in facilitating an easy interpretation of smart contracts.
With the rapid growth of blockchain technology, smart contracts are now crucial to Decentralized Finance (DeFi) applications. Effective vulnerability detection is vital for securing these contracts against hackers and enhancing the accuracy and efficiency of security audits. In this paper, we present SimilarGPT, a unique vulnerability identification tool for smart contract, which combines Generative Pretrained Transformer (GPT) models with Code-based similarity checking methods. The main concept of the SimilarGPT tool is to measure the similarity between the code under inspection and the secure code from third-party libraries. To identify potential vulnerabilities, we connect the semantic understanding capability of large language models (LLMs) with Code-based similarity checking techniques. We propose optimizing the detection sequence using topological ordering to enhance logical coherence and reduce false positives during detection. Through analysis of code reuse patterns in smart contracts, we compile and process extensive third-party library code to establish a comprehensive reference codebase. Then, we utilize LLM to conduct an indepth analysis of similar codes to identify and explain potential vulnerabilities in the codes. The experimental findings indicate that SimilarGPT excels in detecting vulnerabilities in smart contracts, particularly in missed detections and minimizing false positives.
The immutability of blockchain systems makes the security of smart contracts particularly critical. This study presents SELLM, a novel smart contract vulnerability detection tool that integrates symbolic execution with large language models. SELLM leverages symbolic execution to identify vulnerability-prone paths, extracting control flow data, call sequences, and variable constraints, which are then structured into optimized prompts for LLM analysis. Experimental results using the SmartBugs dataset demonstrate that SELLM substantially outperforms baseline methods in terms of precision and recall, achieving a recall of 90.5% and precision of 89.4% with GPT-4o, particularly excelling in detecting vulnerabilities like arithmetic overflow, bad randomness, and reentrancy.
Smart contracts, one of the most prominent applications of blockchain, are changing the way sectors like finance and law operate. On the flip side, code vulnerabilities on smart contracts are bad news for all, even more for those that trade and resell large amounts of digital assets, since the possible consequences can be disastrous. In this study, we propose SC-CCA, a new deep learning framework that specifically tackles the limitations of conventional methods for detecting smart contract vulnerabilities. SC-CCA embeds CNN combined with Bi-LSTM and Self-Attention Mechanism for further improving the extraction of features from a contract code. In this framework, the use of pre-trained CodeBERT language models for word embedding improves the ability of the feature extraction module to obtain more comprehensive semantic information and context-related information. Feature extraction and pipelined feature concatenation at different levels improve detection and robustness. Experimental results show that, especially in the context of vulnerability detection, SC-CCA achieves higher accuracy, recall and F1-score when compared to existing approaches on the Smart Willed datasets. Our research offers valuable insights for analyzing complex code and detecting a wider range of vul-nerabilities in smart contracts.
Blockchain smart contracts have emerged as a transformative technology, enabling the automation and execution of contractual agreements. These self-executing software programs leverage blockchain’s distributed and immutable nature to eliminate the need for third-party intermediaries. However, this new paradigm of automation and authority introduces a complex environment with technical intricacies that users are expected to understand and trust. The irreversible nature of blockchain decisions exacerbates these issues, as any mistake or misuse cannot be rectified. Current smart contract designs often neglect human-centric approaches and the exploration of trustworthiness characteristics, such as explainability. Explainability, a renowned requirement in Explainable Artificial Intelligence (XAI) aimed at enhancing human understandability, transparency and trust, has yet to be thoroughly examined in the context of smart contracts. A noticeable gap exists in the literature concerning the early development of explainability requirements, including established methods and frameworks for addressing requirements analysis phases, design principles, evaluation of their necessity and trade-offs. Therefore, this thesis aims to advance the field of blockchain smart contract systems by introducing explainability as a design concern, fundamentally prompting requirements engineers and designers to cater to this concern during the early development phases. Specifically, we provide guidelines for explainability requirements analysis, addressing what, why, when and to whom to explain. We propose design principles for integrating explainability into the early stages of development. To tailor explainability further, we propose a human-centred framework for determining information requirements in smart contract explanations, utilising situational awareness theories to address the ‘what to explain’ aspect. Additionally, we present ‘explainability purposes’ as an integral resource in evaluating and designing explainability. Our approach includes a novel evaluation framework inspired by the metacognitive explanation-based theory of surprise, addressing the ‘why to explain’ aspect. The proposed approaches have been evaluated through qualitative validations and expert feedback. We have illustrated the added value and constraints of explainability requirements in smart contracts by presenting case studies drawn from literature, industry scenarios and real-world projects. This study informs requirements engineers and designers regarding how to elicit, design and evaluate the need for explainability requirements, contributing to the advancement of the early development of smart contracts.
Fatemeh Erfan, Mohammad Yahyatabar, Martine Bellaïche, Talal Halabi
With the rapid expansion of using smart contracts, protecting the security of these contracts has become crucial. Existing analysis tools for detecting vulnerabilities in smart contracts are unreliable as they often fall short in accuracy, primarily due to their low recall rates-a significant challenge in this field. In this work, we utilize the open-source SolidiFi benchmark dataset to detect vulnerabilities related to Integer overflow/underflow (IoU), reentrancy (RE), and timestamp dependency (TD). These contracts, verified and available on Etherscan, proved unsuitable for direct application of LLMs due to comments, functions, and variables that might reveal the nature of the vulnerabilities. To address this, we performed several preprocessing steps to prepare the dataset for further research. We utilize a large language model to identify vulnerable code, provide reasoning for the vulnerabilities, explain how an attacker might exploit them, and propose fixed code. We design our prompts using chain-of-thought and expert patterns. Finally, we evaluate the results using various metrics and expert reviewers to assess the correctness of the reasoning, potential security risks, and code fixes. Our experiments demonstrate that our approach outperforms existing tools and methods. Notably, our recall rates are significantly high-93.5%, 95.4%, and 93.8%-addressing the challenge of low recall in detecting IoU, RE, and TD vulnerabilities, respectively.
In the fast-evolving domain of blockchain technology, smart contracts have become instrumental, facilitating billions of dollars in transactions daily. However, the increasing prevalence of smart contract vulnerabilities poses significant risks, potentially undermining trust in this innovative technology. To address these security challenges, our research introduces a novel approach for detecting and mitigating vulnerabilities through a comprehensive analysis of four principal modalities: Solidity source code, bytecode, opcode, and intermediate representations. This multimodal analysis employs a Transformer architecture, VulnFusion, which uniquely integrates these modalities to provide a deeper understanding of both the semantic and syntactical nuances of smart contracts. We propose an interleaving-based data fusion technique that outperforms traditional fusion methods such as concatenation and cross-attention. Experimental evaluations demonstrate that our interleavingbased fusion technique achieves an impressive average F1 score of 89% across source code, opcode, and intermediate representations, demonstrating the effectiveness of our approach.
To address the challenges of low accuracy and limited generalization in existing vulnerability detection methods, this paper presents a novel deep learning approach utilizing graph-based algorithms for detecting vulnerabilities in smart contracts. We begin by analyzing the characteristics of vulnerable smart contracts and introducing the concept of “critical opcodes.” A keyword extraction method is developed to effectively identify and select these critical opcodes from smart contracts. Following this, we integrate a critical opcode weighting mechanism into graph-based algorithms, enabling the capture of both hidden relational features and critical opcode characteristics inherent in vulnerable smart contracts. Experimental results indicate that our approach achieves a significant improvement in recognition accuracy, with F1-scores enhancing by 2.39% and 19.54% in binary and multi-class detection scenarios, respectively, when compared to traditional methods such as the LightGBM model.
Lei Yu, Shiqi Chen, Hang Yuan, Peng Wang · 10 authors
With the rapid development of blockchain technology, smart contract security has become a critical challenge. Existing smart contract vulnerability detection methods face three main issues: (1) Insufficient quality of datasets, lacking detailed explanations and precise vulnerability locations. (2) Limited adaptability of large language models (LLMs) to the smart contract domain, as most LLMs are pre-trained on general text data but minimal smart contract-specific data. (3) Lack of high-quality explanations for detected vulnerabilities, as existing methods focus solely on detection without clear explanations. These limitations hinder detection performance and make it harder for developers to understand and fix vulnerabilities quickly, potentially leading to severe financial losses. To address these problems, we propose Smart-LLaMA, an advanced detection method based on the LLaMA language model. First, we construct a comprehensive dataset covering four vulnerability types with labels, detailed explanations, and precise vulnerability locations. Second, we introduce Smart Contract-Specific Continual Pre-Training, using raw smart contract data to enable the LLM to learn smart contract syntax and semantics, enhancing their domain adaptability. Furthermore, we propose Explanation-Guided Fine-Tuning, which fine-tunes the LLM using paired vulnerable code and explanations, enabling both vulnerability detection and reasoned explanations. We evaluate explanation quality through LLM and human evaluation, focusing on Correctness, Completeness, and Conciseness. Experimental results show that Smart-LLaMA outperforms state-of-the-art baselines, with average improvements of 6.49% in F1 score and 3.78% in accuracy, while providing reliable explanations.
Smart contracts are programs deployed on the blockchain. The security issues of smart contracts have become the focus in recent years. Comments have been widely used to improve the readability of programs. Nevertheless, comments and code are not always consistent in smart contracts because of the modification of developers based on token standards and code reuse. These inconsistencies can mislead developers and even pose security risks. We call comment-code inconsistencies as CCIs. In particular, permission-related CCIs can easily expose vulnerabilities in smart contracts, causing funds to be hacked. In this work, we employ pre-training techniques to detect CCIs on permission in smart contracts. Specifically, we collect 3511 comments from Ethereum and Defi projects. Firstly, we utilize BERT to classify permission comments. Then, we extract related function implementations of each permission comment using the compilation technique and adopt CodeT5 to embed comment-code pairs. Finally, we make use of BiLSTM to predict inconsistencies. The evaluation results show that our proposed approach performs better than the existing tools in both precision and recall. Moreover, considering the two stages, it achieves an accuracy of 95.2% and 91.5% in permission comment recognition and permission CCI detection, respectively.