scholarly journals Rich specifications for Ethereum smart contract verification

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-30
Author(s):  
Christian Bräm ◽  
Marco Eilers ◽  
Peter Müller ◽  
Robin Sierra ◽  
Alexander J. Summers

Smart contracts are programs that execute in 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 rarely 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 specifications 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 for resources and resource transfers, expressing a contract's behaviour in intuitive and concise ways and excluding typical errors by default. We have implemented our approach in 2vyper, an SMT-based automated verification tool for Ethereum smart contracts written in Vyper, and demonstrated its effectiveness for verifying strong correctness guarantees for real-world contracts.

2021 ◽  
Vol 3 ◽  
Author(s):  
Ayman Alkhalifah ◽  
Alex Ng ◽  
Paul A. Watters ◽  
A. S. M. Kayes

In Ethereum blockchain, smart contracts are immutable, public, and distributed. However, they are subject to many vulnerabilities stemming from coding errors made by developers. Seven cybersecurity incidents occurred in Ethereum smart contracts between 2016 and 2018, which led to financial losses estimated to be over US$ 289 million. Reentrancy vulnerability was the cause of two of these incidents, and the impacts went far beyond financial loss. Several reentrancy countermeasures are available, which are based on predefined patterns that are used to prevent vulnerability exploitation before the deployment of a smart contract; however, several limitations have been identified in these countermeasures. Motivated by all these issues, the objective of this article is to help developers improve the cybersecurity of smart contracts by proposing a solution that calculates the difference between the contract balance and the total balance of all participants in a smart contract before and after any operation in a transaction that changes its state. Proof-of-concept implementations show that this solution can provide a detection and prevention mechanism against reentrancy attacks during the execution of any smart contract.


Author(s):  
Monika Di Angelo ◽  
Gernot Salzer

AbstractNext to cryptocurrencies, tokens are a widespread application area of blockchains. Tokens are digital assets implemented as small programs on a blockchain. Being programmable makes them versatile and an innovative means for various purposes. Tokens can be used as investment, as a local currency in a decentralized application, or as a tool for building an ecosystem or a community. A high-level categorization of tokens differentiates between payment, security, and utility tokens. In most jurisdictions, security tokens are regulated, and hence, the distinction is of relevance. In this work, we discuss the identification of tokens on Ethereum, the most widely used token platform. The programs on Ethereum are called smart contracts, which—for the sake of interoperability—may provide standardized interfaces. In our approach, we evaluate the publicly available transaction data by first reconstructing interfaces in the low-level code of the smart contracts. Then, we not only check the compliance of a smart contract with an established interface standard for tokens, but also aim at identifying tokens that are not fully compliant. Thus, we discuss various heuristics for token identification in combination with possible definitions of a token. More specifically, we propose indicators for tokens and evaluate them on a large set of token and non-token contracts. Finally, we present first steps toward an automated classification of tokens regarding their purpose.


2021 ◽  
Vol 54 (5) ◽  
pp. 1-34
Author(s):  
Vimal Dwivedi ◽  
Vishwajeet Pattanaik ◽  
Vipin Deval ◽  
Abhishek Dixit ◽  
Alex Norta ◽  
...  

Smart contracts are a key component of today’s blockchains. They are critical in controlling decentralized autonomous organizations (DAO). However, smart contracts are not yet legally binding nor enforceable; this makes it difficult for businesses to adopt the DAO paradigm. Therefore, this study reviews existing Smart Contract Languages (SCL) and identifies properties that are critical to any future SCL for drafting legally binding contracts. This is achieved by conducting a Systematic Literature Review (SLR) of white- and grey literature published between 2015 and 2019. Using the SLR methodology, 45 Selected and 28 Supporting Studies detailing 45 state-of-the-art SCLs are selected. Finally, 10 SCL properties that enable legally compliant DAOs are discovered, and specifications for developing SCLs are explored.


2021 ◽  
Vol 27 (8) ◽  
pp. 1871-1893
Author(s):  
Vasilii A. DADALKO ◽  
Vladimir V. NIKOLAEVSKII ◽  
Andrei D. NEKRASOV ◽  
Dar’ya S. SHERSTNEVA

Subject. The article considers smart contracts as digital financial instruments, their financial and economic essence, which is defined as digital instruments for the settlement of financial relations. Objectives. The aim is to introduce into scientific use such a system concept as digital financial instruments and mechanisms based on the consideration of their economic, legal and financial essence. Methods. The study rests on systems approach that enables to present a smart contract from a technological, economic, legal and financial position as a set of elements with their specific functions defining its complex concept. Results. We reveal the nature of financial relations, arising at the time when bilateral or multilateral transactions are concluded and smart contracts are presented as ways to automatically settle them. Completion of a smart contract is a confirmation of the completion of the transaction and the moment of termination of financial relationship. The article shows the fundamental possibility of using smart contracts in the system of budget relations as a tool for the settlement of a multilateral transaction. Conclusions. Currently, smart contracts are an essential element of a new stage in the development of financial technologies. Specialists in the financial and banking sector recognize the emerging opportunities for their use in the system of financial relations. The paper shows an example of possible use of smart contracts in the settlement of budget relations and in improving the utilization efficiency of budget funds.


2021 ◽  
Vol ahead-of-print (ahead-of-print) ◽  
Author(s):  
Asli Pelin Gurgun ◽  
Kerim Koc

PurposeAs a remedy to usually voluminous, complicated and not easily readable construction contracts, smart contracts can be considered as an effective and alternative solution. However, the construction industry is merely known as a frontrunner for fast adoption of recent technological advancements. Numerous administrative risks challenge construction companies to implement smart contracts. To highlight this issue, this study aims to assess the administrative risks of smart contract adoption in construction projects.Design/methodology/approachA literature survey is conducted to specify administrative risks of smart contracts followed by a pilot study to ensure that the framework is suitable to the research question. The criteria weights are calculated through the fuzzy analytical hierarchy process method, followed by a sensitivity analysis based on degree of fuzziness, which supports the robustness of the developed hierarchy and stability of the results. Then, a focus group discussion (FGD) is performed to discuss the mitigation strategies for the top-level risks in each risk category.FindingsThe final framework consists of 27 sub-criteria, which are categorized under five main criteria, namely, contractual, cultural, managerial, planning and relational. The findings show that (1) regulation change, (2) lack of a driving force, (3) works not accounted in planning, (4) shortcomings of current legal arrangements and (5) lack of dispute resolution mechanism are the top five risks challenging the adoption of smart contracts in construction projects. Risk mitigation strategies based on FGD show that improvements for the semi-automated smart contract drafting are considered more practicable compared to full automation.Originality/valueThe literature is limited in terms of the adoption of smart contracts, while the topic is receiving more attention recently. To support easy prevalence of smart contracts, this study attempts the most challenging aspects of smart contract adoption.


Author(s):  
Abdullah Albizri ◽  
Deniz Appelbaum

Although research shows that blockchain provides fairly immutable virtual provenance workflows, proof that the Blockchain accurately represents physical events lacks truly independent verification. This dilemma, the Oracle Paradox, challenges blockchain architecture and is perhaps one reason why businesses have hesitated to adopt smart contracts. Blockchain proponents claim that people can serve as trusted Oracles in a smart contract. However, auditing research shows that people are the weak link in almost every internal control application, including those pertaining to blockchain. People are susceptible to collusion, bribery, error, and fraud and these tendencies are not entirely mitigated by blockchain technologies (Balagurusamy et al. 2019; Nakamoto 2008). This research proposes a framework to mitigate the paradox of the Oracle: A Business Process Management (BPM) model of a Blockchain Smart Contract-enabled Supply Chain with IoT as the sole "third-party" Oracle participant, utilizing Design Science research.


F1000Research ◽  
2017 ◽  
Vol 6 ◽  
pp. 66 ◽  
Author(s):  
Mehdi Benchoufi ◽  
Raphael Porcher ◽  
Philippe Ravaud

Clinical trial consent for protocols and their revisions should be transparent for patients and traceable for stakeholders. Our goal is to implement a process allowing the collection of patients’ informed consent, which is bound to protocol revisions, storing and tracking the consent in a secure, unfalsifiable and publicly verifiable way, and enabling the sharing of this information in real time. For that, we will built a consent workflow using a rising technology called Blockchain. This is a distributed technology that brings a built-in layer of transparency and traceability. Additionally, it removes the need for third parties, and gives participative control to the peer-to-peer users. From a more general and prospective point of view, we believe Blockchain technology brings a paradigmatical shift to the entire clinical research field. We designed a Proof-of-Concept protocol consisting of time-stamping each step of the patient’s consent collection using Blockchain; thus archiving and historicising the consent through cryptographic validation in a securely unfalsifiable and transparent way. For each revision of the protocol, consent was sought again. We obtained a single document, in a standard open format, that accounted for the whole consent collection process: timestamped consent status with regards to each version of the protocol. This document cannot be corrupted, and can be checked on any dedicated public website. It should be considered as a robust proof of data. In the future, we think that the complex data flow of a clinical trial can be tracked using Blockchain. Moreover, a blockchain core functionality, named Smart Contract, can help prevent clinical trial events not to happen in the right chronological order: including patients before they consented or analysing case report forms data before freezing the database. This will help reaching reliability, security, and transparency, and could be a consistent step towards reproducibility.


2020 ◽  
Author(s):  
Gergana Varbanova ◽  

Are the technologies advanced enough to replace lawyers and the judiciary in the negotiation and enforcement process? Is it possible for a program code to be a contract that binds the parties named in it? What is a smart contract and what challenges does it pose to the law? The present study aims to clarify and show the advantages and disadvantages of using smart contracts in civil law.


Author(s):  
Pengcheng Xia ◽  
Haoyu Wang ◽  
Bingyu Gao ◽  
Weihang Su ◽  
Zhou Yu ◽  
...  

The prosperity of the cryptocurrency ecosystem drives the need for digital asset trading platforms. Beyond centralized exchanges (CEXs), decentralized exchanges (DEXs) are introduced to allow users to trade cryptocurrency without transferring the custody of their digital assets to the middlemen, thus eliminating the security and privacy issues of traditional CEX. Uniswap, as the most prominent cryptocurrency DEX, is continuing to attract scammers, with fraudulent cryptocurrencies flooding in the ecosystem. In this paper, we take the first step to detect and characterize scam tokens on Uniswap. We first collect all the transactions related to Uniswap V2 exchange and investigate the landscape of cryptocurrency trading on Uniswap from different perspectives. Then, we propose an accurate approach for flagging scam tokens on Uniswap based on a guilt-by-association heuristic and a machine-learning powered technique. We have identified over 10K scam tokens listed on Uniswap, which suggests that roughly 50% of the tokens listed on Uniswap are scam tokens. All the scam tokens and liquidity pools are created specialized for the "rug pull" scams, and some scam tokens have embedded tricks and backdoors in the smart contracts. We further observe that thousands of collusion addresses help carry out the scams in league with the scam token/pool creators. The scammers have gained a profit of at least $16 million from 39,762 potential victims. Our observations in this paper suggest the urgency to identify and stop scams in the decentralized finance ecosystem, and our approach can act as a whistleblower that identifies scam tokens at their early stages.


Author(s):  
Moutaz Abojeib ◽  
Farrukh Habib

Blockchain and smart contracts are forming new systems to record and manage businesses with less need for intermediaries. The new systems are expected to offer high level of governance with lower cost as compared to the traditional technologies. While there is a continuous effort to apply this innovative technology in several businesses, Islamic finance in general—and Islamic social finance in particular—are facing few challenges that could be solved by such innovations. Islamic social finance institutions such as waqf are facing some challenges in enhancing its governance structure to ensure Shariah compliance as well as economic efficiency. This chapter explains how blockchain and smart contract technologies can help these institutions for better governance, lower transaction cost, more transparency, and higher trust, hence enhancing the business flexibility and market accessibility. It also presents some related cases that are currently under development as an evidence for the practicality of these technologies in the Islamic social finance arena.


Sign in / Sign up

Export Citation Format

Share Document