This research presents a sophisticated technological framework for Cross-Chain Decentralized Finance (DeFi) and Smart Contract systems by seamlessly integrating Markov Models, Brownian Motion, and Stationary Processes. Focused on enhancing the adaptability and efficiency of financial interactions across interconnected blockchain networks, this framework establishes the foundational elements necessary for dynamic system modeling. The incorporation of Markov Models captures state transitions, Brownian Motion models random fluctuations, and Stationary Processes ensure statistical stability. The paper explores the technological implications of these stochastic processes, addressing challenges in system interoperability, latency, and security within decentralized financial ecosystems. Envisioning a future where decentralized systems are optimized and resilient, the research investigates advancements in blockchain protocol design, consensus mechanisms, and transaction validation strategies. The proposed framework, influenced by the dynamic and statistical nature of Brownian Motion and Stationary Processes, underscores the need for robust data structures, real-time data feeds, and decentralized oracle networks. This research invites collaboration from the blockchain, smart contract, and stochastic modeling communities to contribute to the ongoing exploration and refinement of this powerful technological framework, poised to reshape the landscape of cross-chain financial technologies.
This paper introduces a novel incentivization scheme tailored for a leaderless Directed Acyclic Graph-based Distributed Ledger Technology. The distinctive feature of the proposed scheme lies in enabling a no-fee environment with a fixed supply token, all while incorporating a robust anti-spam mechanism and a well-defined incentivization scheme.
Smart contracts play a critical role in blockchain applications, managing vast amounts of valuable assets. However, they are often vulnerable to attacks due to the inherent difficulties in modifying their code once deployed. Existing security analysis tools and verifiers primarily focus on single-contract verification, while many real-world blockchain applications involve multiple contracts and transactions. In this paper, we introduce an automated verifier, iCon, for inter-transaction properties of smart contracts on the Tezos blockchain platform. iCon is based on our program logic, which verifies inter-transaction properties in the presence of both known and unknown contracts. We present an abstraction technique for unknown contracts and propose a proof technique to ensure that an inter-transaction property holds for any existence of unknown contracts. The proof technique supports the correctness of our verification approach. We have implemented iCon on top of the Why3 verification framework, demonstrating its effectiveness through several case studies, including the decentralized exchange service Dexter2, of which a previous version had a flaw in its implementation.
Poorly specified smart contracts can be vulnerable to attacks on faulty design. Formal methods are currently unable to address these vulnerabilities because they are not vulnerabilities of incorrect code, but of incorrect specification. We are thus in need of a paradigm shift in how we specify and verify smart contracts which allows for a rigorous and accurate notion of a contract specification’s correctness. We submit that correctness includes appropriate cryptoeconomic behaviors, which are generally out of scope of a contract’s specification. We advocate for an approach to contract specification consisting of contract axiomatization and metaspecification, and illustrate with an example.
Kaiho Fukuchi, Ken Naganuma, Takayuki Suzuki, Takatoshi Ohara
Bug bounties are a helpful system for identifying vulnerabilities in smart contracts. Many web3 applications use bug bounties today. However, hackers might worry about not getting paid or receiving a reduced bounty if the bounty is not exchanged atomically with a bug report. This concern could lead hackers to exploit the identified bug instead of reporting it. Furthermore, other efforts related to bug bounties require modification of existing smart contracts. To solve this, we propose a practical bug bounty platform for smart contracts, ContractSafeguard, that utilizes Intel SGX to ensure the existence of bugs and atomic exchange of bounty and bug reports. Bug hunters send transactions to smart contracts hosted within the Enclave and glitch them. Test code within the Enclave generates a bug report that includes proof of the bug’s existence and a method that triggers the bug. In other words, within the Enclave, our mechanism detects and proves that the smart contract under test has entered an abnormal state. Our on-chain bug bounty contract then verifies the proof within the bug report and pays the bounty to the bug hunter atomically. Since the proof is produced within the Enclave, generating false proofs is impossible, and the on-chain contract can trust the report. Additionally, the developer can use existing smart contracts without modification since we have a runtime of smart contracts in the Enclave. We design ContractSafeguard for Ethereum smart contracts.
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.
Sharding is a prevailing solution to enhance the scalability of current blockchain systems. However, the cross-shard commit protocols adopted in these systems to commit cross-shard transactions commonly incur multi-round shard-to-shard communication, leading to low performance. Furthermore, most solutions only focus on simple transfer transactions without supporting complex smart contracts, preventing sharding from widespread applications. In this paper, we propose LightCross, a novel sharding blockchain system that enables efficient execution of complex cross-shard smart contracts. First, LightCross offloads the execution of cross-shard transactions into off-chain executors equipped with the TEE hardware, which can accommodate execution for arbitrarily complex contracts. Second, we design a lightweight cross-shard commit protocol to commit cross-shard transactions without multi-round shard-to-shard communication between shards. Last, LightCross lowers the cross-shard transaction ratio by dynamically changing the distribution of contracts according to historical transactions. We implemented the LightCross prototype based on the FISCO-BCOS project and evaluated it in real-world blockchain environments, showing that LightCross can achieve 2.6× more throughput than state-of-the-art sharding systems.
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.''
Federated learning (FL) is decentralized machine learning framework that finds various applications in health, finance, and the internet of things. This paper studies the under-explored business competition in FL, where organizations are both collaborators in training a shared model and competitors in providing model-based services to a continuum of customers. We focus on an oligopoly case with three organizations. To understand how competition affects FL collaboration, we start with a benchmark case where organizations are not competitors, and show that they have an incentive to collaborate. However, in the presence of competition, organizations may prefer to train local models instead of collaborating via FL (even if FL incurs zero training costs). The reason is that FL intensifies price competition by improving organizations’ model performance to a similar level. To address this issue, we devise a model differentiation mechanism in which organizations adaptively adjust their model performance, enabling differentiated model-based services to customers. We prove that the adaptive mechanism converges in polynomial time and is incentive compatible. Perhaps surprisingly, numerical experiments on CIFAR-10 show that the mechanism can simultaneously improve the model performance, organizations’ revenues, and social welfare. The improvement is up to 22.31%, 14.42%, and 19.50%, respectively.
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.
Dan Lin, Jiajing Wu, Yunmei Yu, Qishuang Fu · 6 authors
In recent years, money laundering crimes on blockchain, especially on Ethereum, have become increasingly rampant, resulting in substantial losses. The unique features of money laundering on Ethereum, such as decentralization and pseudonymity, pose new challenges for Ethereum anti-money laundering. Specifically, the existence of dense and extensive laundering gangs and intricate multilayered laundering pathways makes it exceptionally challenging for regulators to identify suspicious accounts and trace money flows. To address this issue, we propose an innovative DenseFlow framework that effectively identifies and traces money laundering activities by finding dense subgraphs and applying the maximum flow idea. We conduct multiple experiments on four datasets from Ethereum to validate the effectiveness of our approach. The precision of our DenseFlow is 16.34% higher than the start-of-the-art comparison methods on average, highlighting its distinctive contribution to tackling money laundering issues on blockchain.
M. Mahalakshmi, Vedant Bhatnagar, Kumar Adarsh Pandita
Developing a robust electronic voting system that upholds the principles of loveliness and sequestration essential in traditional voting styles, while employing the translucency and rigidity of electronic systems, has posed a patient challenge. This ongoing exploration trials to explore the operation of block chain technology as a means to produce allotted electronic voting systems. The study introduces an ingenious electronic voting model grounded on block chain, leveled at mollifying some of the failings observed in being systems. colorful block chain fabrics are assessed for their felicity in constructing such a system. Through a case study fastening on the electoral process, the paper illustrates the eventuality of allotted tally technologies in enhancing the screen and obscurity of choices. Throughout the design evolution, we remain aware of two intermediary questions Can block chain technology be effectively employed to expedite the deployment of meaningful, high- performing operations that extend distinct vantages over traditional styles? And can block chain grease the deployment of operations while maintaining respectable interpretation within being constraints? We cast to manipulate these inquiries through our exploration bid, which involves expansive testing, dissection, and iterative refinement of the proffered block chain grounded electronic voting system. By using creations in block chain technology and integrating them with established principles of advancing veracity, our end is to establish a complete result that not only meets the rigid demands of secure electronic voting but also sets a new metric for translucency, loveliness, and effectiveness in electoral processes.Through collaboration with stakeholders, policymakers, and experts in the field, we strive to ensure that our result isn't only technically sound but also ultra practical and scalable, paving the expressway for wide relinquishment and trust in electronic voting systems.
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.
Purpose Smart contracts are written in high-level programming languages, compiled into Ethereum Virtual Machine (EVM) bytecode, deployed onto blockchain systems and called with the corresponding address by transactions. The deployed smart contracts are immutable, even if there are bugs or vulnerabilities. Therefore, it is critical to verify smart contracts before deployment. This paper aims to help developers effectively and efficiently locate potential defects in smart contracts. Design/methodology/approach GethReplayer, a smart contract testing method based on transaction replay, is proposed. It constructs a parallel transaction execution environment with two virtual machines to compare the execution results. It uses the real existing transaction data on Ethereum and the source code of the tested smart contacts as inputs, conditionally substitutes the bytecode of the tested smart contract input into the testing EVM, and then monitors the environmental information to check the correctness of the contract. Findings Experiments verified that the proposed method is effective in smart contract testing. Virtual environmental information has a significant effect on the success of transaction replay, which is the basis for the performance of the method. The efficiency of error locating was approximately 14 times faster with the proposed method than without. In addition, the proposed method supports gas consumption analysis. Originality/value This paper addresses the difficulty that developers encounter in testing smart contracts before deployment and focuses on helping develop smart contracts with as few defects as possible. GethReplayer is expected to be an alternative solution for smart contract testing and provide inspiration for further research.
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.