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.
With the rise of living standards, more and more people pay attention to the grade of ceramic products. The beautiful appearance of two different ceramic products of the same type can bring a price difference of more than 1,000 times. Because the structure of ceramic products is simple, easy to imitate, and difficult to identify, many imitation products have infringed on the rights of customers and original product enterprises. Therefore, copyright protection becomes particularly important. However, traditional methods of copyright registration fail to satisfy the requirements due to their long cycle, non-transferable, and cumbersome in rights confirmation, etc. In this paper, we combine the appearance and structural features of ceramic products, investigate an approach for rights confirmation and infringement tracking with the digital features of ceramic products. As another contribution, we propose to establish a copyright transaction model based on smart contracts. To identify the infringement acts, we invoke smart contracts to extract the rights. Through the computer vision algorithms to compare the similarity between physical products and digital resources. Combined with this research, the registration, confirmation, traceability, and transaction of ceramic product copyright can be well realized.
A blockchain is a growing list of cryptographically secured blocks to maintain shared data on decentralized systems, in order to archive transactions between untrusted participants. Smart contracts are computer programs that automatically execute legal events according to the terms of contracts. Although the Ethereum blockchain has been successfully applied to a number of interesting applications, there have been several events that subtle flaws in smart contracts induce a huge amount of financial loss such as the DAO attack. Accordingly, to analyze smart contracts, we propose a novel formal verification technique to employ ATL (Alternating-time Temporal Logic) model checking. Our methodology represents the interaction between users and smart contracts with a two-player game and verify game properties by using MCMAS that is an efficient ATL model checker.
Emerging information technologies have accelerated the construction of the Industrial Internet of Things (IIoT). Unfortunately, the explosive growth of various services has caused serious challenges to access control in terms of scalability and trustworthiness. In this paper, we proposed the smart collaborative contract based endogenous access control mechanism. First, access control procedures running on centralized servers are migrated to distributed equipment located inside the data plane, which can reduce the transmission overhead and improve service capacity. Second, the smart collaborative contract is designed for credibility enhancement since part of attackers may attempt to compromise access control. It covers terminal behavior assessment and service request recording. Experiments conducted in a prototype show that the performance of the proposed scheme is better than the traditional solution and is resistant to common attacks.
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.
Priyanka Pandit, Alp Tezbasaran, Arjun Earthperson, Mihai Diaconeasa
Abstract The approval process from the U.S. Nuclear Regulatory Commission (NRC) for nuclear power plants is sequential. It involves several government bodies such as the Advisory Committee on Reactor Safeguards (ACRS), public meetings, and hearings. If the submissions made to the NRC do not contain enough information to meet the regulation requirements, the NRC issues a Request for Additional Information (RAI). Thus, the licensee has to go through a paperwork-intensive process that involves multiple regulatory agencies for the various licensing requirements. Moreover, sending applications to the NRC is limited to using an electronic submission generation tool called the Packing Slip Wizard (PSW). This paper presents a methodology to implement Distributed Ledger Technology (DLT) to address the need for a real-time, digitized documentation platform in the nuclear power industryâs licensing and regulation process. The evaluation of DLTâs implementation resulted in the formulation of a methodology to accept submissions from an applicant on a web application and storing the received data on a distributed ledger. The presented method offers a real-time submission of the available information of an application. It facilitates the NRC with a real-time feedback capability expediting the review process. RAIâs can be reduced in number by ensuring that the NRCâs information requirements are defined as smart contracts.
NFT is a unit of data stored on a blockchain digital ledger to represent items such as photos, videos, audio, and other intellectual property. NFT certifies a digital asset to be unique i.e. not interchangeable. Current blockchain store the transaction from each node but it is required more security to show the proof of ownership. This paper proposes NFT secure blockchain architecture confirming the ownership of transaction and implement secure payment method to avoid mistake of transfer the token by escrow account on transaction confirmation node called J Node.
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.
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.
Wafa Ben Slama Souei, Chiraz El Hog, Layth Sliman, Raoudha Ben Djemaa ¡ 5 authors
In recent years, Blockchain technology has proved its efficiency in many domains. A smart contract is a software component allowing exposing services via the Blockchain network. Smart contracts are small programs that automatically execute the terms of an agreement when predetermined terms and conditions are reached. With the increasing growth in the popularity of smart contracts, searching, retrieving and understanding smart contracts before executing them becomes a significant challenge. Nevertheless, the majority of these contracts are closed source contracts. Therefore, users cannot understand their functionality and their internal mechanism. In addition, their description lacks the expressiveness and it didn't cover the QOS parameters. In this paper, we propose a Uniform Description language for Smart Contract named UDL-SC. This proposal is an extension of USDL based on the MDA approach to promote trust and minimize the ambiguity between the user and the contract provider.
Safely keeping the accountâs private key is vital in blockchain technology, as there are no native blockchain mechanisms for recovering the account when the private key is lost. Therefore, this paper proposes a solution to this problem, running directly on the blockchain platform in the form of a smart contract, enabling deposit of digital assets into the contract for safekeeping, along with a list of security questions. The proposed solution can be used, for example, in online games. By providing proof of knowing answers to questions, a player can access his account without his private key. Furthermore, additional security measures are put in place to cope with malicious behaviour.
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.
The context of revenue generation streams in the music industry has been intermittently discussed since the transition from sales to streaming started when Spotify launched in 2008. Although revenues in the industry have reached new heights, musicians express dissatisfaction with lower royalty payouts. Moreover, it has become increasingly more difficult and convoluted to understand the royalty calculations in the music industry. With todayâs complicated licensing agreements, money flows through a complex chain of third parties before it reaches the hand of musicians. The industry struggles with transparency and efficiency, and the musicians are paying the price. Meanwhile, the rise of blockchain technology has developed since its first application with Bitcoin in 2008. Today, more and more advanced blockchains can run decentralized transparent applications that utilize the technologyâs efficient transaction system. With the industry issues and the promises of blockchain in mind, this paper demonstrates how blockchain technology can be applied to solve value chain problems within the music space. This paper identifies core issues in the music industry, proposes a decentralized application (dApp) that attempts to solve these issues and implements the proposed solution. This paper exhibits the business logic by developing smart contracts on the
Ethereum blockchain and uses IPFS (InterPlanetary File System) for decentralised file storage to make an associated web application choosing a JavaScript framework. The dApp works as a global copyrights database where musicians can register and license musical works. Author exploits Ethereumâs efficient transactional system to manage license purchases.
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.
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.
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.
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.
Contesto: Le tecnologie basate su blockchain sono oggetto di studio e implementazione fino dalla loro prima applicazione nel sistema Bitcoin. Uno degli sviluppi maggiormente interessanti e rappresentato dalla contrattazione smart, in cui alcune clausole vengono tradotte in software per lâesecuzione automatica al verificarsi di una determinata condizione. Il sistema risolve alla radice il problema di eventuali inadempimenti, spostando lâintervento della tutela giudiziale a un momento successivo in cui verranno verificate le condizioni di validita ed efficacia del contratto o lâeventuale presenza di errori di sistema. In particolare gli smart contract verranno applicati alla contrattazione cliente-fornitore nel campo dellâorganizzazione di eventi. Obiettivi: Lâorganizzazione di eventi di ogni tipo (concerti, fiere, matrimoni, meeting aziendali, compleanni, ecc) e un mercato in grande crescita, che coinvolge molti attori e stimola a sua volta diverse attivita economiche di supporto. Il progetto DME si propone di realizzare una piattaforma digitale di supporto alla organizzazione, gestione, comunicazione e partecipazione ad eventi. La piattaforma inoltre creera e gestira i contratti di fornitura dei diversi servizi attraverso degli smart contract, implementati in Hyperledger. Sara quindi necessario prima di tutto sviluppare lâarchitettura a microservizi per il lato backend e il lato front end della piattaforma che permettera la connessione tra clienti e fornitori, successivamente il front end verra integrato con Hyperledger per la definizione e gestione di smart contract. Metodo: Il modulo front-end, sviluppato in Angular, ha la responsabilita di erogare servizi di accesso e rendere operative sia le funzioni di ricerca dei fornitori adeguati al tipo di evento che si deve organizzare che quelle di gestione del contratto direttamente allâinterno della piattaforma. La progettazione prevede semplicita, accesso multi-device e in mobilita. Il modulo backend e basato su architettura a microservizi in cui ciascun microservizio e composto di funzionalita elementari riusabili. Lâimplementazione di ciascun microservizio prevede lâutilizzo di Java, Spring e Hibernate per la realizzazione di market place di definizione di beni e servizi, definizione di utenti e profili, servizi orizzontali di autorizzazione e autenticazione, back up e recovery. Infine, e stato realizzato, con lâutilizzo di Hyperledger Fabric, un distributed ledger per la definizione e gestione di smart contract come nucleo per la gestione della relazione cliente fornitore durante tutta la durata dellâevento. Conclusioni: Attraverso la comunicazione tra tutti e tre i moduli descritti si e riusciti a soddisfare i requisiti iniziali del progetto ovvero tutte le funzionalita di supporto allâ organizzazione, gestione, comunicazione e parteci-pazione ad eventi. Tuttavia, rimane incerta lâeffettiva validita legale degli smart contract in quanto per la legislazione presente non rispetterebbero i vincoli di forma dellâinsieme di vincoli necessari per la validita di un contratto(accordo delle parti, causa , oggetto, forma).
In order to ensure the confidentiality of digital contents, improve the fairness of digital copyright transactions, and reduce the time and management overhead of digital copyright owners, we proposed a blockchain-based digital rights management scheme. First, we designed a new multiauthority ciphertext-policy attribute-based encryption (MA-CPABE) scheme and showed that the new MA-CPABE has the indistinguishability of plaintext under adaptively chosen plaintext attack (IND-CPA) security and good performance. By combining the MA-CPABE and proxy re-encryption, the rights owner can flexibly sell the copyright to different users with once encryption by an agent who cannot access any information related to digital content when changing the ciphertext access policy as required. By using the smart contract of Ethereum, a fair trade of the decryption keys between the rights owner and rights requester is implemented. In order to further improve fairness, another blockchain is used as a ledge to store information related to digital rights, which greatly reduces the storage overhead in public blockchain. Security analysis shows that our scheme can provide IND-CPA security, resist collusion attacks, and protect the userâs privacy. Performance analysis shows that our scheme can provide a wealth of features to meet the various needs of users. The simulation results show that our scheme is very efficient compared to other schemes.