UTXO-based smart contract platforms face an efficiency bottleneck, in that any transaction sent to a contract must specify the entire updated contract state. This requirement becomes particularly burdensome when the contract state contains dynamic data structures, as needed in many use cases to track interactions between users and the contract. The problem is twofold: on the one hand, a large state in transactions implies a large transaction fee; on the other hand, a large centralized state is detrimental to the parallelization of transactions — a feature that is often cited as a key advantage of UTXO-based blockchains over account-based ones. We propose a novel UTXO-based blockchain model, named hybrid UTXO (hUTXO) , along with a technique to efficiently execute smart contracts on it. The key idea underlying hUTXO is the distribution of the contract state across multiple UTXOs, enabling transactions to access only the specific portions of the state they need, thereby reducing their size (and fees). Our hUTXO model also borrows features from account-based models (in particular, the handling of the contract balance), making it “hybrid” in nature. To simplify the development of smart contracts in hUTXO, we introduce a high-level smart contract language (named hURF), along with a compiler into hUTXO transactions. We show how to exploit our framework to parallelize the validation of transactions on multi-core CPUs. We implement our technique and provide an empirical validation of its effectiveness.
Gislainy Crisostomo Velasco, Noelí Antonia Pimentel Vaz, Sérgio T. Carvalho
The development of smart contracts presents significant challenges compared to traditional software development, such as the immutability of the blockchain and the limitation of program size. These challenges can lead to human errors and the existence of vulnerabilities that may be exploited by malicious individuals, resulting in substantial financial losses. Contract developers face language and infrastructure constraints and insufficient information on interface patterns and implementation specifications. Existing proposals are often challenging to understand, with complex formal verifications requiring expertise in this approach. This article proposes using Model-Driven Engineering (MDE), employing a metamodel for contract development and code generation for the corresponding platform. The metamodel proposed in this study referred to as the High-Level Metamodel for Smart Contract (HLM-SC), is an abstraction applicable to contract development in various contexts. HLM-SC consists of a set of metaclasses allowing the declaration of essential elements for constructing a contract on the Ethereum Virtual Machine (EVM). A graphical tool has been developed to facilitate contract modeling following HLM-SC specifications. Additionally, the model generated from the tool is transformed into Solidity code. This approach aims to overcome developers’ limitations, offering a more understandable and efficient approach to building smart contracts on the blockchain.
Johnnatan Messias Peixoto Afonso, Krzysztof Gogol, Maria Inês Silva, Benjamin Livshits
This paper examines inscription-related transactions on Ethereum and major EVM-compatible rollups, assessing their impact on scalability during transaction surges. Our results show that, on certain days, inscriptions accounted for nearly 90% of transactions on Arbitrum and ZKsync Era, while 53% on Ethereum, with 99% of these inscriptions involving meme coin minting. Furthermore, we show that ZKsync and Arbitrum saw lower median gas fees during these surges. ZKsync Era, a ZK-rollup, showed a greater fee reduction than the optimistic rollups studied -- Arbitrum, Base, and Optimism.
Smart contracts are software programs that enable diverse business activities on the blockchain. Recent research has identified new classes of "machine un-auditable" bugs that arise from both transactional contexts and source code. Existing detection methods require human understanding of underlying transaction logic and manual reasoning across different sources of context (i.e. modalities), such as code, dynamic transaction executions, and natural language specifying the expected transaction behavior. To automate the detection of ``machine un-auditable'' bugs, we present SmartInv, an accurate and fast smart contract invariant inference framework. Our key insight is that the expected behavior of smart contracts, as specified by invariants, relies on understanding and reasoning across multimodal information, such as source code and natural language. We propose a new prompting strategy to foundation models, Tier of Thought (ToT), to reason across multiple modalities of smart contracts and ultimately to generate invariants. By checking the violation of these generated invariants, SmartInv can identify potential vulnerabilities. We evaluate SmartInv on real-world contracts and re-discover bugs that resulted in multi-million dollar losses over the past 2.5 years (from January 1, 2021 to May 31, 2023). Our extensive evaluation shows that SmartInv generates (3.5X) more bug-critical invariants and detects (4$\times$) more critical bugs compared to the state-of-the-art tools in significantly (150X) less time. \sys uncovers 119 zero-day vulnerabilities from the 89,621 real-world contracts. Among them, five are critical zero-day bugs confirmed by developers as ``high severity.''
Given the complexity of issuing, verifying, and trading green power certificates in China, along with the challenges posed by policy changes, ensuring that China's green certificate market trading system receives proper mechanisms and technical support is crucial. This study presents a green power certificate trading (GC-TS) architecture based on an equilibrium strategy, which enhances the quoting efficiency and multi-party collaboration capability of green certificate trading by introducing Q-learning, smart contracts, and effectively integrating a multi-agent trading Nash strategy. Firstly, we integrate green certificate trading with electricity and carbon asset trading, constructing pricing strategies for the green certificate, carbon, and electricity trading markets; secondly, we design a certificate-electricity-carbon efficiency model based on ensuring the consistency of green certificates, green electricity, and carbon markets; then, to achieve diversified green certificate trading, we establish a multi-agent reinforcement learning game equilibrium model. Additionally, we propose an integrated Nash Q-learning offer with a smart contract dynamic trading joint clearing mechanism. Experiments show that trading prices have increased by 20%, and the transaction success rate by 30 times, with an analysis of trading performance from groups of 3, 5, 7, and 9 trading agents exhibiting high consistency and redundancy. Compared with models integrating smart contracts, it possesses a higher convergence efficiency of trading quotes.
Decentralized Exchanges (DEXs), leveraging blockchain technology and smart contracts, have emerged in decentralized finance. However, the DEX project with multi-contract interaction is accompanied by complex state logic, which makes it challenging to solve state defects. In this paper, we conduct the first systematic study on state derailment defects of DEXs. These defects could lead to incorrect, incomplete, or unauthorized changes to the system state during contract execution, potentially causing security threats. We propose StateGuard, a deep learning-based framework to detect state derailment defects in DEX smart contracts. StateGuard constructs an Abstract Syntax Tree (AST) of the smart contract, extracting key features to generate a graph representation. Then, it leverages a Graph Convolutional Network (GCN) to discover defects. Evaluating StateGuard on 46 DEX projects with 5,671 smart contracts reveals its effectiveness, with a precision of 92.24%. To further verify its practicality, we used StateGuard to audit real-world smart contracts and successfully authenticated multiple novel CVEs.
With the increasing demand for decentralized systems and the widespread usage of blockchain, low throughput and high latency have become the biggest stumbling blocks in the development of blockchain systems. This problem seriously hinders the expansion of blockchain and its application in production. Most existing smart contract scheduling solutions use static feature analysis to prevent contract conflicts during parallel execution. However, the conflicts between transactions are complex; static feature analysis is not accurate enough. In this paper, we first build the dependency between smart contracts by analyzing the features. After numerous experiments, we propose a conflict model to adjust the relationship between threads and conflict to achieve high throughput and low latency. Based on these works, we propose adaptive parallel scheduling for smart contracts on the blockchain. Our adaptive parallel scheduling can distinguish conflicts between smart contracts and dynamically adjust the execution strategy of smart contracts based on the conflict factors we define. We implement our scheme on ChainMaker, one of the most popular open-source permissioned blockchains, and build experiments to verify our solution. Regarding latency, our solution demonstrates remarkable efficiency compared with the fully parallel scheme, particularly in high-conflict transaction scenarios, where our solution achieves latency levels just one-twentieth of the fully parallel scheme. Regarding throughput, our solution significantly outperforms the fully parallel scheme, achieving 30 times higher throughput in high-conflict transaction scenarios. These results highlight the superior performance and effectiveness of our solution in addressing latency and throughput challenges, particularly in environments with high transaction conflicts.
Massimo Bartoletti, Angelo Ferrando, E. Lipparini, Vadim Malvone
Smart contracts are an attractive target for attackers, as evidenced by a long history of security incidents. A current limitation of smart contract verification tools is that they are not really effective in expressing and verifying liquidity properties regarding the exchange of crypto-assets: for example, is it true that in every reachable state a user can fire a sequence of transactions to withdraw a given amount of crypto-assets? We propose Solvent, a tool aimed at verifying these kinds of properties, which are beyond the reach of existing verification tools for Solidity. We evaluate the effectiveness and performance of Solvent through a common benchmark of smart contracts.
Haoxian Chen, Lan Lu, Brendan Massey, Yuepeng Wang · 5 authors
Smart contracts manage a large number of digital assets nowadays. Bugs in these contracts have led to significant financial loss. Verifying the correctness of smart contracts is, therefore, an important task. This paper presents an automated safety verification tool, DCV, that targets declarative smart contracts written in De-Con, a logic-based domain-specific language for smart contract implementation and specification. DCV proves safety properties by mathematical induction and can automatically infer inductive invariants using heuristic patterns, without annotations from the developer. Our evaluation on 23 benchmark contracts shows that DCV is effective in verifying smart contracts adapted from public repositories, and can verify contracts not supported by other tools. Furthermore, DCV significantly outperforms baseline tools in verification time.
Bugs in smart contracts may have devastating effects as they tend to cause financial loss. According to a recent study, accounting bugs are the most common kind of bugs in smart contracts that are beyond automated tools during pre-deployment auditing. The reason lies in that these bugs are usually in the core business logic and hence contract-specific. They are analogous to functional bugs in traditional software, which are largely beyond automated bug finding tools whose effectiveness hinges on uniform and machine checkable characteristics of bugs. It was also reported that accounting bugs are the second-most difficult to find through manual auditing, due to the need of understanding underlying business models. We observe that a large part of business logic in smart contracts can be modeled by a few primitive operations like those in a bank, such as deposit, withdraw, loan, and pay-off, or by their combinations. The properties of these operations can be clearly defined and checked by an abstract type system that models high-order information such as token units, scaling factors, and financial types. We hence develop a novel type propagation and checking system with the aim of identifying accounting bugs. Our evaluation on a large set of 57 existing accounting bugs in 29 real-world projects shows that 58% of the accounting bugs are type errors. Our system catches 87.9% of these type errors. In addition, applying our technique to auditing a large project in a very recent auditing contest has yielded the identification of 6 zero-day accounting bugs with 4 leading to direct fund loss.
Groundhog is a novel design for a smart contract execution engine based around concurrent execution of blocks of transactions. Unlike prior work, transactions within a block in Groundhog are not ordered relative to one another. Instead, our key design insights are first, to design a set of commutative semantics that lets the Groundhog runtime deterministically resolve concurrent accesses to shared data. Second, some storage accesses (such as withdrawing money from an account) conflict irresolvably; Groundhog therefore enforces validity constraints on persistent storage accesses via a reserve-commit process. These two ideas give Groundhog a set of semantics that, while not as powerful as traditional sequential semantics, are flexible enough to implement a wide variety of important applications, and are strictly more powerful than the semantics used in some production blockchains today. Unlike prior smart contract systems, transactions throughput never suffers from contention between transactions. Using 96 CPU cores, Groundhog can process more than half a million payment transactions per second, whether between 10M accounts or just 2.
Development of blockchain smart contracts is more difficult than mainstream software development because the underlying blockchain infrastructure poses additional complexity. To ease the developer's task of writing smart contract, as other research efforts, we also use Business Process Model and Notation BPMN modeling to describe application requirements for trade of goods and services and then transform automatically the BPMN model into the methods of a smart contract. In our previous research we described our approach and a tool to Transform Automatically BPMN models into Smart contracts TABS. In this paper, we describe how the TABS approach is augmented with the support for a BPMN collaborative transaction by several actors. Our approach analyzes the BPMN model to determine which patterns in the BPMN model are suitable for use as collaborative transactions. The found BPMN patterns that are suitable as transactions are shown to the developer who decides which ones should be deployed as collaborative transactions. We describe how our approach automatically transform the BPMN model into smart contract the provides a transaction mechanism to enforce the transactional properties of the nested transactions. Our approach greatly reduces the developers task as synchronization of collaborative activities is provided by our approach, so that the developer needs to code only independent tasks with well-defined inputs and outputs. We also overview the TABS+ tool we built as a proof of concept to show that our approach is feasible. Finally, we provide estimates on the cost of supporting the nested BPMN collaborative transactions.
Cryptocurrency forensics have become standard tools for law enforcement. Their basic idea is to deanonymise cryptocurrency transactions to identify the people behind them. Cryptocurrency deanonymisation techniques are often based on premises that largely remain implicit, especially in legal practice. On the one hand, this implicitness complicates investigations. On the other hand, it can have far-reaching consequences for the rights of those affected. Argumentation schemes could remedy this untenable situation by rendering the underlying premises more transparent. Additionally, they can aid in critically evaluating the probative value of any results obtained by cryptocurrency deanonymisation techniques. In the argumentation theory and AI community, argumentation schemes are influential as they state the implicit premises for different types of arguments. Through their critical questions, they aid the argumentation participants in critically evaluating arguments. We specialise the notion of argumentation schemes to legal reasoning about cryptocurrency deanonymisation. Furthermore, we demonstrate the applicability of the resulting schemes through an exemplary real-world case. Ultimately, we envision that using our schemes in legal practice can solidify the evidential value of blockchain investigations, as well as uncover and help to address uncertainty in the underlying premises—thus contributing to protecting the rights of those affected by cryptocurrency forensics.
In the wake of blockchain and Web3 technological advancements, Non-Fungible Tokens (NFTs) have emerged as prominent digital assets within the realms of art, gaming, and virtual commodities. Unlike their traditional counterparts, NFT auctions harness the virtues of decentralization, transparency, and immutability, ushering in a new era for trading artworks and other digital assets. This paper embarks on an exploration, first laying down the foundational principles of blockchain technology and NFTs. A comparative analysis follows, juxtaposing the dynamics of NFT auctions with the modus operandi of traditional auctions. Within the theoretical scaffold, the nuances of decentralization and trust in NFT auctions are elucidated, spotlighting the pivotal role of smart contracts throughout the auction trajectory. The emphasis also gravitates towards transparency and security, two cornerstones ensuring the integrity of the auction process. Diving into the methodology, this section delineates the research blueprint and the techniques employed for program testing. Delving into the practicalities, the discourse meticulously unpacks the architecture and operability of the smart contract, gauging its efficacy through rigorous assessments. Beyond the present scope, the paper ventures to uncover potential applications and horizons awaiting NFT auctions across diverse sectors.
Smart contracts are computer programs running on blockchains to implement Decentralized Applications. The absence of contract specifications hinders routine tasks, such as contract understanding and testing. In this work, we propose a specification mining approach to infer contract specifications from past transaction histories. Our approach derives high-level behavioral automata of function invocations, accompanied by program invariants statistically inferred from the transaction histories. We implemented our approach as tool SMCON and evaluated it on eleven well-studied Azure benchmark smart contracts and six popular real-world DApp smart contracts. The experiments show that SMCON mines reasonably accurate specifications that can be used to enhance symbolic analysis of smart contracts achieving higher code coverage and up to 56 % speedup, and facilitate DApp developers in maintaining high-quality documentation and test suites.
Ahmed Gouda Mohamed, Fahad Alqahtani, Mohamed Sherif, Sama Moustafa El-Shamie
The construction industry embodies a paramount role in the economic growth of various nations, including the Middle East and North Africa (MENA) region. Despite its significance, the industry faces construction disputes and payment issues, inducing financial losses and project postponements. Consequently, the construction industry has mutated smart contracts to enhance operational efficiency, which automates contract management tasks and offers perks, including transparency and efficiency. However, the adoption of smart contracts in the MENA construction sector remains limited, and the region lacks thorough research on this topic. This study addresses this gap by examining the level of cognizance and apprehension of smart contracts among construction industry stakeholders in the MENA region. The research employs Structural Equation Modeling (SEM) to analyze the relative importance of implementing smart contracts within different project lifecycle phases and relevant practices and identify the hindrances impacting MENA’s smart contract deployment. A practical implementation of smart contract-based tendering employing the Trakti platform is paraded. The findings unveiled the infancy of smart contract adoption in the MENA construction sector. They revealed the substantial importance of implementing smart contracts in the Project Execution Phase, Project Closure, and Monitoring and Control Phase, attaining relative weights of 23.23%, 21.62%, and 20.50%, respectively.
Smart contracts codify real-world transactions and automatically execute the terms of the contract when predefined conditions are met. This paper proposes SmartML, a modeling language for smart contracts that is platform independent and easy to comprehend. We detail its formal semantics and type system with a focus on its role in addressing security vulnerabilities. We show along a case study, how SmartML contributes to the prevention of reentrancy attacks, illustrating its efficacy in reinforcing the reliability and security of smart contracts within decentralized systems.
We consider Geometric Mean Market Makers (G3Ms) – a special type of Decentralized Exchange – with two types of traders: liquidity takers and arbitrageurs. Liquidity takers use G3Ms to swap tokens and to speculate, while arbitrageurs exploit arbitrage opportunities arising from misalignments between the G3M's price and the external market price. We show that in continuous time, a G3M charging proportional transaction fees offers exchange rates that are of finite variation, and that the opportunity cost of providing liquidity relative to rebalancing a self-financing constant-weights portfolio is, in fact, a non-negative gain. Moreover, we demonstrate that Impermanent Loss can be super-hedged in continuous time by a model-free rebalancing strategy. We conclude with a numerical analysis discussing the approximative nature of our continuous-time results for trading in discrete time.
The pivotal role of semiconductors in propelling the rapid advancement of technologies, such as artificial intelligence, electric vehicles, and robotics, has prompted global attention toward bolstering semiconductor competitiveness.A fabless firm's performance is a determinant factor in this landscape.However, the dominance of established global fabless firms in the semiconductor market presents formidable barriers to the ingress and expansion of new entrants.Consequently, this study advocates for a novel semiconductor business model utilizing smart contracts based on emerging blockchain technology.To substantiate the efficacy of this model, a survey encompassed 106 semiconductor experts across 11 nations.Results indicated that 75% of respondents perceived an enhancement in fabless growth of the semiconductor business model.They affirmed the potential for acquiring new clientele, thereby highlighting the significance of this business model in furnishing a novel growth trajectory for fabless semiconductor companies seeking entry into the global market.
Given the growing importance of smart contracts in various applications, ensuring their security and reliability is critical. Fuzzing, an effective vulnerability detection technique, has recently been widely applied to smart contracts. Despite numerous studies, a systematic investigation of smart contract fuzzing techniques remains lacking. In this paper, we fill this gap by: 1) providing a comprehensive review of current research in contract fuzzing, and 2) conducting an in-depth empirical study to evaluate state-of-the-art contract fuzzers' usability. To guarantee a fair evaluation, we employ a carefully-labeled benchmark and introduce a set of pragmatic performance metrics, evaluating fuzzers from five complementary perspectives. Based on our findings, we provide direction for the future research and development of contract fuzzers.
Hongyu Guo, Haozhe Liang, Ju Huang, Wei Ou · 7 authors
The proliferation of blockchain technology has resulted in diverse token standards, posing challenges for compatibility, security, and performance in existing cross-chain bridges. This paper introduces a novel framework capable of concurrently facilitating fungible token exchange, as well as the processing of both individual and batch non-fungible tokens (NFTs). We deploy token bridges that meet different token standards to support cross-chain staking and unlocking of ERC20, ERC721, and ERC1155. To minimize both waiting times and handling fees, we relocate processes necessitating frequent transactions and verifications to the sidechain. Additionally, we adopt a batch-processing approach for tokens necessitating cross-chain transfers, leveraging payment channels to facilitate efficiency. The system’s reliability is upheld through the validator group. Validators acquire an initial reputation value by making deposits and enhance both their rewards and reputation by successfully completing NFT auction tasks on the sidechain. We use OpenZeppelin’s security library functions to standardize token operations, and carefully design the validator’s reward, punishment, and reputation mechanisms. Our comprehensive contract security audit and system analysis validate our solution’s effectiveness in mitigating common vulnerabilities and internal threats. Implementation and testing with Ethereum and its test network demonstrate substantial reductions in transmission time for key cross-chain token steps by nearly half. Moreover, our framework showcases efficiency and cost-effectiveness with an average gas cost of 693,379.
James A. Cunningham, Nigel Davies, Sarah Devaney, Søren Holm · 7 authors
Abstract Decentralized autonomous organizations (DAOs) have emerged as a novel governance mechanism that operates through distributed ledgers and smart contracts, enabling members to direct an organization's actions. The widespread adoption of DAOs has occurred in response to their utility in managing emergent semi‐structured projects and has led to the development of various innovative governance mechanisms. The mechanisms employed by DAOs has the potential to be generalized beyond their core financial domain to a wide range of use cases. In the medical field the use of blockchain and DAOs can provide secure and transparent access to medical data, while ensuring patient privacy. Civic access to medical data is a growing area of interest, where individuals have control over their own medical data and can share it with healthcare providers, researchers, and other stakeholders. DAOs can facilitate this civic access, enabling individuals to share their data securely and selectively with authorized parties for research and other purposes. This paper explores the use of DAOs to medical data sharing, with a focus on ownership, governance, and transaction models. An application framework and API that enables the deployment of DAO‐like organizations is derived and this approach is applied to the patient‐centric management of medical data.
Burak Öz, Jonas Gebele, Parshant Singh, Filip Rezabek · 5 authors
Maximal Extractable Value (MEV) searching has gained prominence on the Ethereum blockchain since the surge in Decentralized Finance activities. In Ethereum, MEV extraction primarily hinges on fee payments to block proposers. However, in First-Come-First-Served (FCFS) blockchain networks, the focus shifts to latency optimizations, akin to High-Frequency Trading in Traditional Finance. This paper illustrates the dynamics of the MEV extraction game in an FCFS network, specifically Algorand. We introduce an arbitrage detection algorithm tailored to the unique time constraints of FCFS networks and assess its effectiveness. Additionally, our experiments investigate potential optimizations in Algorand's network layer to secure optimal execution positions. Our analysis reveals that while the states of relevant trading pools are updated approximately every six blocks on median, pursuing MEV at the block state level is not viable on Algorand, as arbitrage opportunities are typically executed within the blocks they appear. Our algorithm's performance under varying time constraints underscores the importance of timing in arbitrage discovery. Furthermore, our network-level experiments identify critical transaction prioritization strategies for Algorand's FCFS network. Key among these is reducing latency in connections with relays that are well-connected to high-staked proposers.