Blockchain Papers

Apurba Pokharel, Krishna Dahal

No abstract is available for this record.

Fokke Heikamp, Lei Pan, Rolando Trujillo-Rasúa, Sushmita Ruj · 5 authors

No abstract is available for this record.

Franck Cassez, Joanne Fuller, Horacio Mijail Antón Quiles

We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language Dafny. In our methodology the ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise yet powerful solution to reasoning about contracts that have external calls. This includes arbitrary re-entrancy which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from Dafny to EVM bytecode, the results we obtain on the Dafny code can reasonably be assumed to hold on Solidity code: the translation of the Dafny code to Solidity is straightforward. As a result our approach can readily be used to develop and deploy safer contracts.

Pedro Antonino, Juliandson Ferreira, Augusto Sampaio, A. W. Roscoe

Smart contract evolution is crucial for the success of decentralized applications, and current methods and processes are not well suited to handle these drivers of change, as the knowledge about the software is predominantly stored in informal documents. In addition, they are the building blocks of the ”code is law” paradigm: the smart contract’s code indisputably describes how its assets are to be managed - once it is created, its code is typically immutable. Faulty smart contracts present the most significant evidence against the practicality of this paradigm; they are well-documented and resulted in assets worth vast sums of money being compromised. To address this issue, the Ethereum community proposed (i) tools and processes to audit/analyse smart contracts, and (ii) design patterns implementing a mechanism to make contract code mutable. Individually, (i) and (ii) only partially address the challenges raised by the ”code is law” paradigm. In this work, we combine elements from (i) and (ii) to create a systematic framework that moves away from ”code is law” and gives rise to a new ”specifica- tion is law” paradigm. It allows contracts to be created and upgraded but only if they meet a corresponding formal specification. We explain how formal verification techniques can be used to ensure safety properties of smart contracts during their evolution. Although formal verification methods have the potential of being used in several application fields, we focus on ensuring compliance with its specifications. The process consists of three phases: Formal requirements specification, verification, and deployment. All steps are planned and executed in an integrated way and together they form a framework capable of fostering safe evolution and make it more reliable and secure. The framework is centered around a trusted deployer: an off-chain service that formally verifies and enforces specification conformance. We have proto- typed this framework, and investigated its applicability to contracts implementing three widely used Ethereum standards: the ERC20 Token Standard, ERC3156 Flash Loans and ERC1155 Multi Token Standard, with promising results.

Franco Frattolillo

Copyright protection of digital content has become a problem not only for web content providers but also for ordinary web users who like to publish their digital contents on social or user generated content platforms. Among the possible solutions to such a problem, digital watermarking, in conjunction with watermarking protocols, appears to be a valid alternative to current DRM (digital rights management) systems. In fact, watermarking based solutions insert perceptually invisible copyright information into the copies of contents published or distributed on the web in order to track them. Such insertions are carried out according to the watermarking protocols, which have evolved over the years from the classic “buyer and seller” paradigm into a simpler and versatile “buyer friendly” and “mediated” approach. However, such an approach cannot exploit the new technologies that characterize the current Internet. This paper presents a new watermarking protocol able to adapt the “buyer friendly” and “mediated” approach to the use of innovative technologies such as cloud platforms and blockchain. In this way, (1) content providers and common web users can take advantage of the computing and storage resources made available by cloud platforms; (2) the involvement of trusted third parties in the protocols can be reduced by using blockchain without complicating the protection scheme. In fact, these two goals make the protocol particularly suited for the current Internet.

Kunjian Song, Nedas Matulevicius, Eddie B. de Lima Filho, Lucas C. Cordeiro

Smart contracts written in Solidity are programs used in blockchain networks, such as Etherium, for performing transactions. However, as with any piece of software, they are prone to errors and may present vulnerabilities, which malicious attackers could then use. This paper proposes a solidity frontend for the efficient SMT-based context-bounded model checker (ESBMC), named ESBMC-Solidity, which provides a way of verifying such contracts with its framework. A benchmark suite with vulnerable smart contracts was also developed for evaluation and comparison with other verification tools. The experiments performed here showed that ESBMC-Solidity detected all vulnerabilities, was the fastest tool, and provided a counterexample for each benchmark. A demonstration is available at https://youtu.be/3UH8_1QAVN0.

Isaac Adjei-Mensah, Isaac Osei Agyemang, Collins Sey, Linda Delali Fiasam · 5 authors

From online education and trading, all aspects of our lives are affected by digital technology. Among them, the storage of music has also entered the digital era. Music productions created by artists have brought great joy to people. However, when artists upload their works, they are most downloaded and reprinted by others, and copyright information and the issue associated with the sharing of music arise. This will have a significant negative impact on the enthusiasm and motivation of artists. This paper provides an internet database platform for artists, which uses the distributed and tamper-proof technology of the Ethereum blockchain to store music works, and protect the copyright information of each album or music produced by artists in the music industry. Design and implementation of the system model and data storage are proposed and data storage processes based on the Ethereum smart contract are demonstrated in detail. The system stores music information on the blockchain network, using the smart contract to provide artists with a fast and efficient royalty payment. Node.js is applied to carry out the experiments of our system, and we test Remote Procedure Calls (RPC) with available account and private keys for contract development and use block explorer to track music information on the blockchain. Our system enables copyright revenue to be attributed to music creators that will help to eliminate the illegal uploading of music on other websites.

Muhammad Danil Muis, Muhammad Rifki Fauzan, Parman Sukarno, Aulia Arif Wardana

This reserach build access control and file distribution management system for electronic diploma and transcript using ethereum smart contract and InterPlanetary File System (IPFS). The falsification of diplomas/transcripts is one of the problems in education. In Indonesia, falsification of diplomas/transcripts is a form of criminal act of falsifying letters. In addition, diplomas/transcripts that have not been digitalized make them easily damaged, lost, and difficult to manage. Therefore, this research developed digital diploma/transcript as digital twin from the hardcopy of diploma/tramscript. This research used IPFS to store data in a distributed system and Smart Contracts Blockchain to store and protect the digital diploma/transcript. The system also comes with access control to create and give approval for diplomas or transcripts to be published and saved into the system. Access control settings will be saved using the blockchain. This research using Quality of Service test method for measurethroughput, packet loss, and delay. Beside that, tis research also analysis the usage of Central Processing Unit and Random Access Memory from the system. Based on the test that has been done, the fake diploma/transcript detection system can be run properly by using 1 node to 5 nodes. The best throughput value during the process of making and validating the diploma/transcript is to use 1 node. The value of packet loss in the process of making and validating the certificate/transcript has a very good category. The value of delay in the process of making and validating the diploma/transcript has a very good category.

Samvid Dharanikota, Suvam Mukherjee, Chandrika Bhardwaj, Aseem Rastogi · 5 authors

We present CELESTIAL, a framework for formally verifying smart contracts written in the Solidity language for the Ethereum blockchain. CELESTIAL allows programmers to write expressive functional specifications for their contracts. It translates the contracts and the specifications to F⋆ to formally verify, against an F⋆ model of the blockchain semantics, that the contracts meet their specifications. Once the verification succeeds, CELESTIAL performs an erasure of the specifications to generate Solidity code for execution on the Ethereum blockchain. We use CELESTIAL to verify several real-world smart contracts from different application domains. Our experience shows that CELESTIAL is a valuable tool for writing high-assurance smart contracts.

Afonso Falcão, Andreia Mordido, Vasco T. Vasconcelos

The popularity of smart contracts is on the rise, yet breaches in reliability and security linger. Among the many facets of smart contract reliability, we concentrate on faults rooted in out-of-order interactions with contract endpoints. We propose SmartScribble, a protocol language to describe valid patterns of interaction between users and endpoints. SmartScribble not only ensures correct interactive behaviour but also simplifies smart contract coding. From a protocol description, our compiler generates a smart contract that can then be completed by the programmer with the relevant business logic. The generated contracts rely on finite state machines to control endpoint invocations. As a proof of concept, we target Plutus, the contract programming language for the Cardano blockchain. Preliminary evaluation points to a 75% decrease in the size of the code that developers must write, coupled with an increase of reliability by enforcing the specified patterns of interaction.

Chaochen Shi, Yong Xiang, Jiangshan Yu, Keshav Sood · 5 authors

Context: Decentralized applications on blockchain platforms are realized through smart contracts. However, participants who lack programming knowledge often have difficulties reading the smart contract source codes, which leads to potential security risks and barriers to participation. Objective: Our objective is to translate the smart contract source codes into natural language descriptions to help people better understand, operate, and learn smart contracts. Method: This paper proposes an automated translation tool for Solidity smart contracts, termed SolcTrans, based on an abstract syntax tree and formal grammar. We have investigated 3,000 smart contracts and determined the part of speeches of corresponding blockchain terms. Among them, we further filtered out contract snippets without detailed comments and left 811 snippets to evaluate the translation quality of SolcTrans. Results: Experimental results show that even with a small corpus, SolcTrans can achieve similar performance to the state-of-the-art code comments generation models for other programming languages. In addition, SolcTrans has consistent performance when dealing with code snippets with different lengths and gas consumption. Conclusion: SolcTrans can correctly interpret Solidity codes and automatically convert them into comprehensible English text. We will release our tool and dataset for supporting reproduction and further studies in related fields.

Nam-Yong Lee, Jinhong Yang, Chul‐Soo Kim

Several platform companies have been successful in competing with digital piracy by producing consumer-friendly services. Nowadays, however, the digital content service market has become more monopolized than ever, which forms barriers to the entry of new platform companies. The platform monopoly would cause considerable problems both to content providers and consumers as it limits the choice of consumers. To remove the platform monopoly in digital content markets, we propose a public blockchain-based digital content service method. The proposed method encrypts the digital content to a self-decryptable form, which we call Smart Propertized Digital Content (SPDC), and utilizes the decentralization and traceability of the public blockchain to provide a non-monopolistic ecosystem for the management and distribution of the SPDC license. The proposed method can be more beneficial both to content creators and users than the current winner-takes-all platform model. For instance, users can download SPDC once and play many times without requesting the decryption key, and SPDC owners can make SPDC licenses to be time-limited, device-limited, resellable, or terminated without resorting to help from other intermediaries. We conducted the threat analysis on the proposed method by examining possible attacks in various scenarios. Based on threat analysis, we conclude that the proposed method can provide a new type of digital content service ecosystem that can be operated in a completely decentralized way and neutrally beneficial to all participants.

Aboua Ange Kevin N’DA, Santiago Matalonga, Keshav Dahal

No abstract is available for this record.

Asma Khatoon

The work presented in this thesis describes the design and development of smart contract system for blockchain based applications. The main objective is to investigate the current state of blockchain technology and its implementations and to reveal how main principles of this disruptive technology can reshape "business as normal" activities. This work examines the Blockchain technology as a whole and addresses its potential for the development of distributed applications. Blockchain based smart contract system for different applications that demonstrate a streamlined access management system using Ethereum blockchain has been designed and implemented. Ethereum reinforces the second gen of blockchain technology by providing an open and global computing/environment platform allowing for the exchange of cryptocurrency (Ether) and the creation of self-verified smart contract applications. Smart contracts provide a framework for the ownership of digital assets and a range of distributed applications in the blockchain region. Ethereum and smart contracts are open, decentralized and unalterable, as such, they are susceptible to vulnerabilities that arise from developers ' simple coding errors. We have designed and implemented smart contract system for blockchain based applications across healthcare management to Facilitate Medical Ecosystems and Energy systems to increase energy efficiency by designing smart contract system for energy-saving certificates. We also identified key themes, developments and emerging areas of healthcare and energy research. In this thesis, blockchain technology has been applied in areas such as healthcare and Energy sector. Healthcare applications are the main contribution of this thesis and the work on the Energy systems reflects as an additional contribution of this thesis. Hopefully the work presented in this thesis will give enough motivation towards developing distributed applications (ĐApps) using blockchain based smart contract system.

Hong Su, Bing Guo, Xinhua Suo, Chuanfeng Zhang

In the rapidly evolving landscape of the sixth generation (6G) network, smart contracts emerge as a pivotal technology for enforcing trustful rules. However, the conventional lifecycle model of smart contracts—encompassing stages from initiation to the termination of a contract instance—suffers from rigidity and lack of customization, leading to notable operational challenges. These challenges primarily manifest as heightened resource demands, including longer waiting periods and escalated transaction costs, which hinder the adaptability of smart contracts in the varied and dynamic contexts of 6G-connected environments. Driven by these issues, this article conducts a comprehensive analysis of the smart contract lifecycle. We introduce an innovative lifecycle model that offers customizable flexibility, allowing for the merging or separation of different stages in the smart contract process. Meanwhile, we propose a unique transaction data structure designed to integrate parameters of combined stages, each marked with distinct identifiers for differentiation. Further, we introduce an innovative address scheme for smart contract instances, which provides an identifier to simplify instance access while also maintaining a mechanism for traditional access methods. The verification results show that the model can save 52.72% of processing fee and 68.09% of completion time compared with the conventional method.

Vinícius Lima, Filipe Andrade Bernardi, Rui Rijo, Jó Ueyama · 5 authors

BACKGROUND: Intensified research and innovation and rapid uptake of new tools, interventions, and strategies are crucial to fight Tuberculosis, the world's deadliest infectious disease. The sharing of health data remains a significant challenge. Data consumers must be able to verify the consistency and integrity of data. Solutions based on distributed ledger technologies may be adequate, where each member in a network holds a unique credential and stores an identical copy of the ledger and contributes to the collective process of validating and certifying digital transactions. OBJECTIVES: This work proposes a mechanism and presents a use case in Digital Health to allow the verification of integrity and immutability of TB electronic health records. METHODS: IOTA was selected as a supporting tool due to its data immutability, traceability and tamper-proof characteristics. RESULTS: A mechanism to verify the integrity of data through hash functions and the IOTA network is proposed. Then, a set of TB related information systems was integrated with the network. CONCLUSION: IOTA technology offers performance and flexibility to enable a reliable environment for electronic health records.

Christian Bräm, Marco Eilers, Péter Müller, Robin Sierra · 5 authors

Smart contracts are programs that execute inside blockchains such as Ethereum to manipulate digital assets. Since bugs in smart contracts may lead to substantial financial losses, there is considerable interest in formally proving their correctness. However, the specification and verification of smart contracts faces challenges that do not arise in other application domains. Smart contracts frequently interact with unverified, potentially adversarial outside code, which substantially weakens the assumptions that formal analyses can (soundly) make. Moreover, the core functionality of smart contracts is to manipulate and transfer resources; describing this functionality concisely requires dedicated specification support. Current reasoning techniques do not fully address these challenges, being restricted in their scope or expressiveness (in particular, in the presence of re-entrant calls), and offering limited means of expressing the resource transfers a contract performs. In this paper, we present a novel specification methodology tailored to the domain of smart contracts. Our specification constructs and associated reasoning technique are the first to enable: (1) sound and precise reasoning in the presence of unverified code and arbitrary re-entrancy, (2) modular reasoning about collaborating smart contracts, and (3) domain-specific specifications based on resources and resource transfers, which allow expressing a contract's behavior in intuitive and concise ways and exclude typical errors by default. We have implemented our approach in 2vyper, an SMT-based automated verification tool for Ethereum smart contracts written in the Vyper language, and demonstrated its effectiveness in succinctly capturing and verifying strong correctness guarantees for real-world contracts.

Hong Su, Bing Guo, Junyu Lu, Xinhua Suo

Currently, the P2P method is that its software runs on a P2P hardware environment. However, the software is not a P2P one. It is difficult to match the scenarios in which the users’ requirements change often. Meanwhile, if the software is out of service, all participants are affected. Thus, in this paper, we propose the fully decentralized application model, in which a P2P software runs in a P2P hardware environment. It is based on the blockchain, as a blockchain provides a secured P2P hardware environment. We focus on its P2P software (the P2P smart contract). A P2P smart contract is formed by smart contracts from its participants instead of a third party. It allows each participant to specify its requirement in a turning-complete way and the failure of one smart contract does not affect other smart contracts. We first describe the requirement of the P2P smart contract and the dependence among them. Then, we propose different ways to pair associated smart contracts. At last, we verify the proposed P2P smart contract model, and it shows more flexibility and robustness than the centralized software method.

Xavier Foccroulle Ménard, Cécilia Barrette-Leduc

No abstract is available for this record.

Mukesh Kumar Gupta

No abstract is available for this record.

Gabin Heo, Dana Yang, Inshil Doh, Kijoon Chae

Blockchain is attracting attention as a new solution for problems such as illegal copying, profit distribution, and forgery and falsification in the digital content trading environment, which has become an essential asset in the information age. However, one problem is that it is difficult to propagate digital content to the blockchain network because of a limited capacity to upload to the blockchain. The integrity and transparency of blockchain are also considered as weak points in terms of privacy. In this paper, we propose a new blockchain system, the secret block-based blockchain (SBBC), to address the problems with the blockchain system in the digital content trading environment. SBBC is composed of off-chain and on-chain network components. Off-chain is the part that allows trading digital content through the authentication phase. The digital content that is traded has a digital fingerprint inserted, so if an illegal leak occurs, the destination can be tracked. In addition, the content is encrypted and traded, and only the rightful user can use the digital content, thus ensuring income for the legitimate content author. Next, the on-chain network is licensed to use digital content, and a verification process using a consensus algorithm is performed. The licensed consumer creates a secret block of their transaction and records it only on their ledger. In a private part, secret block creation ensures privacy and solves the network overload that can occur when uploading digital content to the blockchain. Finally, through the verification and agreement of all blockchain participants, a public block is created and recorded in the ledger to finalize the transaction. Consequently, we propose the SBBC system suitable for digital content trading environments and a safe and reliable system through a consensus algorithm in such environments.

Oyinomomo-emi Emmanuel Akpe, Denis Kisina, Samuel Owoade, Abel Chukwuemeke Uzoka · 6 authors

The increasing complexity of digital platforms, driven by cloud-native architectures, distributed applications, and user-centric services, necessitates robust, scalable, and secure identity management frameworks. This paper explores recent advances in federated authentication and identity management, emphasizing their role in enabling seamless and secure access across interconnected digital ecosystems. Beginning with a foundational overview of identity management’s evolution—from traditional siloed systems to federated and decentralized models—the study outlines key technologies such as SAML, OAuth, OpenID Connect, and emerging paradigms like decentralized identity and blockchain-based verification. It further investigates the integration of artificial intelligence and machine learning for adaptive authentication, anomaly detection, and risk-based decision-making, alongside privacy-enhancing technologies ensuring compliance with data protection regulations such as GDPR. Through the examination of scalability, interoperability, and security challenges, the paper identifies best practices and architectural strategies critical for real-world implementations. The discussion culminates in practical implications for industry adoption across sectors such as healthcare, finance, and e-commerce, and highlights future research directions including the development of standardized identity frameworks, AI integration, and decentralized identity systems in multi-cloud and edge computing environments. This study offers a comprehensive synthesis of current trends and technologies that are shaping the next generation of identity management in scalable digital platforms.

Jianlin Niu, Zhiyu Ren

The existing self-sovereign identity management schemes have some problems, such as weak availability and security risks. To solve these problems, we proposed a cross-domain self-sovereign identity management scheme using smart contracts. This scheme takes into account the entire lifecycle of identity, especially including the cross-domain use and recovery. To preserve the privacy data of users on the blockchain, we proposed a data storage method of anchoring on blockchain. Finally, we implemented this scheme using the Solidity programming language for smart contract. This scheme has been experimentally verified to be capable of maintaining the expenditure of resources under control and having good usability. Compared with other self-sovereign identity management schemes, this scheme has better performance in terms of controllability, security and portability.

Juan Cano-Benito, Andrea Cimmino, Raúl García‐Castro

Blockchain has become a pervasive technology in a wide number of sectors like industry, research, and academy. With the emergence of blockchain, new solutions with this technology to existing problems were devised, leading to the introduction of smart contracts. Smart contracts are similar to traditional contracts with the benefits provided by blockchain, such as immutability, privacy, and decentralisation. These contracts are usually defined based on a specific domain, and this domain knowledge can be represented through an ontology. Researches have explored the benefits of using domain ontologies with smart contracts, such as code generation, discovering other contracts in the network, or interaction with other contracts. Notwithstanding, the representation of smart contract languages themselves has not been studied. In this paper, we present an ontology for a well-known smart contract language, Solidity, defining all entities needed to cover the whole language and aligning it to other standardised ontologies such as EthOn, in a way to improve the knowledge of the ontology developed. Furthermore, the ontology has also been validated with already deployed contracts in the Ethereum blockchain. Thus, Solidity will be able to benefit from the advantages provided by ontologies, such as interoperability and the use of semantic web technologies.