Oct 17, 2024¡Companion Proceedings of the 2024 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity
Blockchain technologies are applied in diverse domains such as financial systems, supply chains, and identity management, leading to the emergence of various smart contract languages design. These contracts often involve time dependent transactions recorded immutably on the blockchain, making their correctness crucial. This paper addresses the formal verification of temporal behaviors in smart contracts without human interaction. We study 9 recent smart contract languages used in 7 leading blockchains and model 27 common temporal patterns from 3148 benchmarks across 9 domain specific application categories. We introduce VESC, a temporal specification language that allows developers to specify temporal properties in structured natural language, which VESC compiles into formal linear temporal logic. Our experiments demonstrate that VESC effectively specifies common temporal behaviors, paving the way for automated temporal verification of smart contracts.
While many studies show that more advanced LLMs excel in tasks such as mathematics and coding, we observe that in cryptocurrency trading, stronger LLMs sometimes underperform compared to weaker ones. To investigate this counterintuitive phenomenon, we examine how LLMs reason when making trading decisions. Our findings reveal that (1) stronger LLMs show a preference for factual information over subjectivity; (2) separating the reasoning process into factual and subjective components leads to higher profits. Building on these insights, we propose a multi-agent framework, FS-ReasoningAgent, which enables LLMs to recognize and learn from both factual and subjective reasoning. Extensive experiments demonstrate that this fine-grained reasoning approach enhances LLM trading performance in cryptocurrency markets, yielding profit improvements of 7\% in BTC, 2\% in ETH, and 10\% in SOL. Additionally, an ablation study reveals that relying on subjective news generates higher returns in bull markets, while focusing on factual information yields better results in bear markets. Code is available at https://github.com/Persdre/FS-ReasoningAgent.
Krzysztof Gogol, Manvir Schneider, Tessone, Claudio, Livshits, Benjamin
Layer-2 (L2) blockchains inherit Ethereums security guarantees while reducing gas fees. As a result, they are gaining traction among traders at Automated Market Makers (AMMs), sparking debate over whether they contribute to liquidity fragmentation of Ethereum. Our research suggests that such fragmentation is not currently occurring. However, it could emerge in the future, particularly if Liquidity Providers (LPs) recognize the higher returns available on L2s. Using Lagrangian optimization, we develop a model for optimal liquidity allocation across AMMs on Ethereum and its L2s, using staking as a benchmark. We show that, in equilibrium, AMM liquidity provision returns converge to this reference rate. Additionally, we measure the elasticity of trading volume with respect to Total Value Locked (TVL) in AMMs and find that, on well-established blockchains, an increase in TVL does not necessarily lead to higher trading volume. Finally, our empirical findings reveal that Ethereums liquidity pools are oversubscribed compared to those on L2s and often yield lower returns than staking Ether. LPs could maximize their rewards by reallocating more than two-thirds of their liquidity to L2s and staking.
This chapter presents a research perspective that explores the transformative impact of blockchain technology on Behavioral and Experimental Economics. It addresses critical digital challenges such as subject identity verification and privacy, trust in researchers, and the design of experimental incentives. By advocating for a blockchain-integrated framework, the chapter aims to enhance data authenticity, privacy, and incentivization through decentralized mechanisms and smart contracts, thereby ensuring research that is transparent, tamper-proof, and practical. Additionally, the chapter proposes a paradigm shift toward a âplay to learnâ model, which bridges decentralized science with the realm of gaming finance to advance research and development. This integration signals a new era of interdisciplinary research, offering profound insights into human behavior within the digital economy and illuminating new research pathways that connect Web2 to Web3 environments.
Background: Health 3.0 allows decision making to be based on longitudinal data from multiple institutions, from across the patient's healthcare journey. In such a distributed setting, blockchain smart contracts can act as neutral intermediaries to implement trustworthy decision making. Objective: In a distributed setting, transmitted data will be structured using standards (such as HL7 FHIR) for semantic interoperability. In turn, the smart contract will require interoperability with this standard, implement a complex communication setup (e.g., using oracles), and be developed using blockchain languages (e.g., Solidity). We propose the encoding of smart contract logic using a high-level semantic Knowledge Graph, using concepts from the domain standard. We then deploy this semantic KG on blockchain. Methods: Off-chain, a code generation pipeline compiles the KG into a concrete smart contract, which is then deployed on-chain. Our pipeline targets an intermediary bridge representation, which can be transpiled into a specific blockchain language. Our choice avoids on-chain rule engines, with unpredictable and likely higher computational cost; it is thus in line with the economic rules of blockchain. Results: We applied our code generation approach to generate smart contracts for 3 health insurance cases from Medicare. We discuss the suitability of our approach - the need for a neutral intermediary - for a number of healthcare use cases. Our evaluation finds that the generated contracts perform well in terms of correctness and execution cost ("gas") on blockchain. Conclusions: We showed that it is feasible to automatically generate smart contract code based on a semantic KG, in a way that respects the economic rules of blockchain. Future work includes studying the use of Large Language Models (LLM) in our approach, and evaluations on other blockchains.
Daniele Friolo, Geoffrey Goodell, D. R. Toliver, Hazem Danny Nakib
This article builds upon the protocol for digital transfers described by Goodell, Toliver, and Nakib, which combines privacy by design for consumers with strong compliance enforcement for recipients of payments and self-validating assets that carry their own verifiable provenance information. We extend the protocol to allow for the verification that reissued assets were created in accordance with rules prohibiting the creation of new assets by anyone but the issuer, without exposing information about the circumstances in which the assets were created that could be used to identify the payer. The modified protocol combines an audit log with zero-knowledge proofs, so that a consumer spending an asset can demonstrate that there exists a valid entry on the audit log that is associated with the asset, without specifying which entry it is. This property is important as a means to allow money to be reissued within the system without the involvement of system operators within the zone of control of the original issuer. Additionally, we identify a key property of privacy-respecting electronic payments, wherein the payer is not required to retain secrets arising from one transaction until the following transaction, and argue that this property is essential to framing security requirements for storage of digital assets and the risk of blackmail or coercion as a way to exfiltrate information about payment history. We claim that the design of our protocol strongly protects the anonymity of payers with respect to their payment transactions, while preventing the creation of assets by any party other than the original issuer without destroying assets of equal value.
The need for secure user authentication in blockchain-based applications has been growing with the increased adoption of Decentralized Identity (DID) credentials in blockchain.Zokrates, a tool designed to protect user privacy within smart contracts, had a limitation in that it could not accept authenticated user information such as credentials, only allowing the use of manually inputted data.In this paper, we propose a smart contract system that securely validates DID credentials to overcome the limitations of traditional centralized authentication systems.This system ensures the safe identification of users within blockchain-based applications by authenticating their identities in a trusted manner within the blockchain.As the demand for user authentication in blockchain rises, this paper emphasizes the significance of a blockchain-based identity verification system that guarantees both privacy and security.Leveraging the Zero-Knowledge Proof method and utilizing the Zokrates tool, this innovative approach aims to provide solutions for the digital identity verification process, thereby expanding the scope of blockchain technology applications.Moreover, we also provide a CLI for each entity.We help anyone who wants to authenticate their identity using the tool to safely verify it on-chain.
Hamza Salem, Hadi Salloum, Manuel Mazzara, Nursultan Askarbekuly ¡ 6 authors
The rapid expansion of the non-fungible token (NFT) market has catalyzed new opportunities for artists, collectors, and investors, yet it has also unveiled critical challenges related to the storage and distribution of associated metadata. This paper examines the current landscape of NFT metadata storage, revealing a significant reliance on centralized platforms, which poses risks to the integrity, security, and decentralization of these digital assets. Through a detailed analysis of top-selling NFTs on the OpenSea marketplace, it was found that a substantial portion of metadata is hosted on centralized servers, making them susceptible to censorship, data breaches, and administrative alterations. Conversely, decentralized storage solutions, particularly the InterPlanetary File System (IPFS), were identified as a more secure and resilient alternative, offering enhanced transparency, resistance to tampering, and greater control for creators and collectors. This study advocates for the widespread adoption of decentralized storage architectures, incorporating digital signatures to verify ownership, as a means to preserve the value and trustworthiness of NFTs in an increasingly digital world. The findings underscore the necessity for NFT platforms to prioritize decentralized methodologies to ensure the long-term sustainability and integrity of the NFT
The widespread use of smart contracts results in high repeatability of their source code. The solution seems to lay in reusing the verification rules that check the feasibility of logically related transactions. The software allows for developing a smart contract that may process various transaction types. Besides, employing the package in implementing a smart contract eliminates the redundancy of verification rules. The package structure ensures the ability to handle actual smart contracts and transactions at the abstract level. Moreover, the article presents a proposal to standardize the way of designing the transaction verification function in a smart contract.
Abstract Environmental, social, and governance (ESG) disclosure has drawn much attention from listed companies, investors, and regulators. In response to the increasing demand of investors and regulators for nonâfinancial information, listed companies have paid attention to publishing ESG reports consisting of environmental, social, and governance information. Listed companies are increasingly required to provide highâquality information that is clear and comparable. However, the lack of incentive to listed companies makes it hard to improve the quality of ESG disclosure, and the cost of ESG disclosure leads to the uncontrollable quality of ESG reports and may even manipulation by opportunistic behaviors. In this paper, we illustrate the moral hazard problem in ESG disclosure from the perspective of investors and listed companies, in which the effort level for listed companies to provide highâquality ESG report cannot be observed by investors. Then we propose a blockchainâbased incentive mechanism for ESG disclosure from a principalâagent perspective to improve the information quality of ESG disclosure, where investors act as principal and listed companies act as agents. Token in blockchain technology is utilized as the rewards to improve the listed companies' reputation, thus increasing their chance of being promoted to investors for preferential investment opportunities in the blockchain platform. We then design the firstâbest (FB) and secondâbest (SB) optimal contracts based on classic principalâagent model to overcome the moral hazard problem. Extensive simulations are conducted to demonstrate the effectiveness and feasibility of the incentive mechanism.
Florian Spychiger, Parminder Kaur Makode, Lukas KĂźng, Claudio J. Tessone
In the evolving landscape of blockchain and distributed ledger technologies, the quest for decentralized governance has led to the advent of Decentralized Autonomous Organizations (DAOs). DAOs offer a groundbreaking framework where token holders directly influence the management and strategic direction of decentralized structures. This study delves into the concept of DAO through the lens of No1s1, an experimental project embodying a self-sustaining architecture governed autonomously. No1s1 stands out as a physical space that operates independently, rewarding participants with tokens for performing maintenance tasks crucial for its upkeep. In this contribution, we employ agent-based modelling to simulate interactions between participants and No1s1, exploring the dynamics of the token economy, participatory governance, and the sustainability of such an autonomous entity. By examining the reciprocal maintenance relationship and its impact on No1s1's longevity and wealth, this study sheds light on the potential and challenges of DAO- governed structures.
This research paper investigates how Ethereum blockchain technology can transform real estate investment through crowdfunding. Traditional real estate markets often encounter issues related to liquidity, accessibility, and transparency; this study addresses these challenges by proposing a blockchain-based solution. It examines the use of Ethereum smart contracts, Initial Coin Offerings (ICOs), and ERC20 tokens to facilitate fractional ownership of properties and automate investment processes. The technical stack for the proposed system includes Vue.js for the front-end, Solidity for developing smart contracts, and the Truffle framework for deployment. Ethereum is used as the blockchain platform, with Ganache-CLI providing a local testing environment. MetaMask is integrated for managing digital wallets, and Stripe is used for processing fiat currency, showcasing a robust approach to blending blockchain technology with current financial systems. This paper offers a detailed examination of the practical applications and challenges of using blockchain in real estate crowdfunding. The findings indicate that while this technology holds great potential for resolving persistent issues in real estate investment, important factors such as scalability, regulatory compliance, and user adoption still need to be carefully considered [4]. Keywords: Blockchain, Ethereum, Smart Contracts, Real Estate Crowdfunding, Tokenization, ERC-20 Tokens, ICO, Fractional Property Ownership, Liquidity, Transparency, Ganache, Remix IDE, MetaMask, Solidity, Truffle Framework.ramework.
Togzhan Barakbayeva, Zhuo Cai, Amir Kafshdar Goharshady, Karaneh Keypoor
Correlated equilibria are a standard solution concept in game theory and generalize Nash equilibria. In a 2-player non-cooperative game in which player i has action set A_i, a correlated equilibrium is a self-enforcing probability distribution Ď over A_1 * A_2. Specifically, when a strategy profile (s_1, s_2) in A_1 * A_2 is sampled according to Ď, each player i can observe their own component s_i, but not the other player's component. Knowing s_i and Ď, player i cannot increase their expected payoff by defecting and playing a strategy s'_i different from s_i. Correlated equilibria are ubiquitous and crucial in mechanism design, including in the design of blockchain-based protocols which aim to incentivize honest behavior. A correlated equilibrium depends on a centralized and impartial oracle, often called the ''external signal'' in game theory literature, to sample a strategy profile and disclose each player's component to them, while keeping the other player's component secret. However, there is currently no trustless method to achieve this on the blockchain without centralization or relying on trusted third-parties. In this work, we address this challenge and provide two novel protocols, one based on oblivious transfer and the other based on zkSNARKs to replace the public signal with a smart contract. We prove that our approaches are secure and provide the desired privacy properties of a correlated equilibrium, while also being efficient in terms of gas usage and thus affordable in practice.
Daniel Sousa-Dias, Daniel Amyot, Ashkan RahimiâKian, John Mylopoulos
The transactive energy market (TEM) is a recent development in energy management that enables prosumers to trade directly, promising many environmental and economic benefits. Prosumer trading necessitates sharing information to facilitate transactions. Additionally, many TEMs propose using blockchains to manage auctions and store transactions. These facts introduce privacy concerns: consumption data, trading history, and other identifying information pose risks to users if leaked. Anonymity by trading under a pseudonym is commonly presented as a solution; however, this creates risks for market participants: scammed users will not have recourse, and users with innocent malfunctions may be banned from trading. We propose the Individually Linkable Pseudonymous Trading Scheme (ILPTS), which enables users to trade under a pseudonym, protecting their identity, while a smart contract monitors reputations and can temporarily deanonymize a user, ensuring market integrity. ILPTS was developed in stages. Examination of existing TEM literature was performed to identify desirable features. Analysis of cryptography literature was performed to identify techniques that may confer certain features. It was found through formal analysis that ILPTS adheres to identified design goals, improves upon existing solutions, and resists common attacks against TEMs. Future work includes software simulation and on-device implementation to further verify security and feasibility.
Zhiyang Chen, Ye Liu, Sidi Mohamed Beillahi, Yi Li ¡ 5 authors
Smart contracts, self-executing programs on the blockchain, facilitate reliable value exchanges without centralized oversight. Despite the recent focus on dynamic analysis of their transaction histories in both industry and academia, no open-source tool currently offers comprehensive tracking of complete transaction information to extract user-desired data such as invariant-related data. This paper introduces OpenTracer, designed to address this gap. OpenTracer guarantees comprehensive tracking of every execution step, providing complete transaction information. OpenTracer has been employed to analyze 350,800 Ethereum transactions, successfully inferring 23 different types of invariant from predefined templates. The tool is fully open-sourced, serving as a valuable resource for developers and researchers aiming to extract or validate new invariants from transaction traces. A demonstration video of OpenTracer is available at https://youtu.be/vTdmjWdYd30. The source code of OpenTracer is available at https://github.com/jeffchen006/OpenTracer.
Smart contracts are programs with mutable state. Transactions submitted to these contracts trigger functions that often modify state. Nodes of the Ethereum blockchain schedule such transactions in a nondeterministic order, potentially leading to races between transactions and concurrency issues. When the outcome of a smart contract varies depending on the order in which transactions are processed, we have a Transaction Ordering Dependency (TOD). TOD enables malicious actors to profit from a smart contract, similar to the well-known frontrunning vulnerability. Existing approaches for detecting TOD in Ethereum smart contracts yield a high rate of false positives and false negatives. To help contract developers and testers detect TOD vulnerabilities with enhanced precision, we propose and evaluate an analysis based on information flow in our tool TODChecker1. We evaluate our approach using a benchmark comprising 513 vulnerable transactions involving 235 real-world Ethereum smart contracts susceptible to frontrunning attacks. Our evaluation finds that our approach outperforms existing approaches, including Oyente, Securify, SAILFISH, TODler, and Nyx, in precision, runtime, and in identifying novel TOD vulnerabilities.
Abstract Ethereum, as a leading blockchain platform, has attracted a significant number of practitioners. These practitioners require a platform for communication and collaborative problemâsolving, which led to Ethereum Stack Exchange (ESE), a Q&A site dedicated to Ethereumârelated issues. While the Q&A site facilitates communication among practitioners, it also introduces new challenges. Practitioners adopt code snippets from Q&A sites to address problems encountered. However, the quality of code snippets on ESE remains largely unexplored. Vulnerabilities and gasâinefficient patterns in ESE may spread to the code in Ethereum and threaten its regular operation. In this article, we conduct an empirical study investigating the distribution of vulnerabilities and gasâinefficient patterns in ESE. Further, we analyze the potential impact of vulnerabilities and gasâinefficient patterns from ESE on Ethereum. However, we encounter a problem during the vulnerability and gasâinefficient pattern detection. Established smart contract analysis tools in the mainstream realm necessitate complete source code files for thorough analysis, while codes on ESE are often incomplete code snippets. To address this, we introduce the ASTâbased code clone detection technique to construct detectable files corresponding to code snippets. This enables us to detect vulnerabilities and gasâinefficient patterns in code snippets. In the end, our findings demonstrate that 11.18% of the contractâlevel code snippets and 4.06% of functionâlevel code snippets in ESE have vulnerabilities. And 27.21% of contractâlevel code snippets and 17.89% of functionâlevel code snippets contain gasâinefficient patterns. The additional consumption caused by the gasâinefficient pattern in ESE is approximately $1,695,002. Based on these findings, we provide recommendations for both ESE and its users, aiming to foster collaborative efforts and create a more reliable Q&A site for practitioners.
El-hacen Diallo, Mohameden Dieye, Omar Dib, Pierre Valiorgue
As blockchain technology continues to evolve, it has fostered an extensive ecosystem of applications and platforms. This dynamic landscape is characterized by a myriad of innovative solutions, ranging from decentralized finance and supply chain management to digital identity and voting systems, each contributing to the ongoing advancement and adoption of blockchain technology across various sectors. Achieving interoperability among these applications and platforms poses a significant challenge due to their use of distinct protocols, and remains a bottleneck hindering the widespread adoption of blockchain technologies. Addressing this challenge requires designing a universal interoperability protocol while ensuring compliance with the security and privacy constraints specific to each blockchain, thus adding complexity. We propose an agnostic interoperability protocol designed for seamless asset movement across independent private blockchain networks, regardless of their individual protocols. This protocol leverages incentive-driven smart contract and Zero-Knowledge Proofs to establish a decentralized, secure, and privacy-focused framework for interoperability. We conduct a security analysis using game theory and provide both theoretical and empirical evaluations of the protocol end-to-end delay. Through a comprehensive use case, we demonstrate the secure deployment of the proposed protocol for asset movement between two private blockchains. We also discuss the trade-offs between cost and delay in cross-blockchain transactions. Furthermore, a comparative analysis with existing interoperability schemes showcases the proposed interoperability scheme superiority in terms of robustness, privacy preservation, and verifiability.
Ensuring the reliability of smart contracts is of vital importance due to the wide adoption of smart contract programs in decentralized financial applications. However, statically checking many rich properties of smart contract programs can be challenging. On the other hand, dynamic validation approaches have shown promise for widespread adoption in practice. Nevertheless, as part of the programming environment for smart contracts, existing dynamic validation approaches have not provided programmers with a notion to clearly articulate the interface between components, especially for addresses representing opaque contract instances. We argue that the âdesign-by-contractâ approach should complement the development of smart contract programs. Unfortunately, there is limited linguistic support for it in existing smart contract languages. In this paper, we design a Solidity language extension, ConSol, that supports behavioral contracts. ConSol provides programmers with a modular specification and monitoring system for both functional and latent address behaviors. The key capability of ConSol is to attach specifications to first-class addresses and monitor violations when invoking these addresses. We evaluate ConSol using 20 real-world cases, demonstrating its effectiveness in expressing critical conditions and preventing attacks. Additionally, we assess ConSolâs efficiency and compare gas consumption with programs fixed with manually inserted assertions, showing that our approach introduces only marginal gas overhead. By separating specifications and implementations using behavioral contracts, ConSol assists programmers in writing more robust and readable smart contracts.
This thesis investigates the impact of design solutions on the execution costs of Ethereum smart contracts, focusing on gas consumption at function level. The work analyzes real-world smart contracts and combines transaction data from Etherscan, function similarity analysis through SmartEmbed and ANTLR, and statistical testing to identify design patterns associated with higher execution costs. Starting from a dataset of Solidity smart contract functions, the study identifies highly similar function pairs with divergent gas costs and manually examines the surrounding contract context to detect recurring design differences. These patterns are then grouped into broader categories and evaluated through statistical analysis to assess their relationship with gas consumption. The results provide practical insights for developers and researchers interested in designing more efficient, sustainable, and cost-aware smart contracts on Ethereum.
Dabao Wang, Bang Ye Wu, Xingliang Yuan, Lei Wu ¡ 6 authors
The prosperity of Decentralized Finance (DeFi) unveils underlying risks, with reported losses surpassing 3.2 billion USD between 2018 and 2022 due to vulnerabilities in Decentralized Applications (DApps). One significant threat is the Price Manipulation Attack (PMA) that alters asset prices during transaction execution. As a result, PMA accounts for over 50 million USD in losses. To address the urgent need for efficient PMA detection, this article introduces a novel detection service,DeFiGuard, using Graph Neural Networks (GNNs). In this article, we propose cash flow graphs with four distinct features, which capture the trading behaviors from transactions. Moreover,DeFiGuardintegrates transaction parsing, graph construction, model training, and PMA detection. Evaluations on the collected transactions demonstrate thatDeFiGuardwith GNN models outperforms the baseline MLP model and classical classification models in Accuracy, TPR, FPR, and AUC-ROC. The results of ablation studies suggest that the combination of the four proposed node features enhancesDeFiGuardâs efficacy. Moreover,DeFiGuardclassifies transactions within 0.892 to 5.317 seconds, which provides sufficient time for the victims (DApps and users) to take action to rescue their vulnerable funds. In conclusion, this research offers a significant step towards safeguarding the DeFi landscape from PMAs using GNNs.
With the widespread adoption of blockchain technology, a novel organizational structure known as Decentralized Autonomous Organizations (DAOs) has attracted considerable attention. DAOs facilitate decision-making through member voting, realizing the governance in a decentralized manner. However, DAOs face unique challenges compared to traditional organization. This paper focuses on two key challenges of governance within DAOs: the whale problem and collusion issue. The whale problem is characterized by the concentration of power among specific members, while for the collusion problem, voting results are distorted by fraudulent collaboration. In terms of voting, we consider Quadratic Voting, a voting system expected to deter the concentration of voting power among a subset of participants, analyzing its resistance to the collusion problem. We show with numerical examples that in comparison to Linear Voting, Quadratic Voting lacks resistance to collusion. Then, we propose a voting mechanism that integrates Quadratic Voting with the Vote escrow tokens, demonstrating the mitigation of the whale problem while acquiring resilience to collusion in the decision-making process. The numerical examples confirm the high efficacy of our proposed model.