In recent publications, we presented a novel formal symbolic process virtual machine (FSPVM) framework that combined higher-order theorem proving and symbolic execution for verifying the reliability and security of smart contracts developed in the Ethereum blockchain system without suffering the standard issues surrounding reusability, consistency, and automation. A specific FSPVM, denoted as FSPVM-E, was developed in Coq based on a general, extensible, and reusable formal memory (GERM) framework, an extensible and universal formal intermediate programming language, denoted as Lolisa, which is a large subset of the Solidity programming language that uses generalized algebraic datatypes, and a corresponding formally verified interpreter for Lolisa, denoted as FEther, which serves as a crucial component of FSPVM-E. However, our past work has demonstrated that the execution efficiency of the standard development of FEther is extremely low. As a result, FSPVM-E fails to achieve its expected verification effect. The present work addresses this issue by first identifying three root causes of the low execution efficiency of formal interpreters. We then build abstract models of these causes, and present respective optimization schemes for rectifying the identified conditions. Finally, we apply these optimization schemes to FEther, and demonstrate that its execution efficiency has been improved significantly.
This paper reports on the development and verification of a novel formal symbolic process virtual machine (FSPVM) for verifying the reliability and security of Ethereum smart contracts, denoted as FSPVM-E, completely in Coq proof assistant. It adopts execution-verification isomorphism (EVI), an extension of Curry-Howard isomorphism (CHI), as its fundamental theoretical framework. The current version of FSPVM-E is constructed on a general, extensible, and reusable formal memory (GERM) framework, an extensible and universal formal intermediate programming language Lolisa, which is a large subset of the Solidity programming language using generalized algebraic datatypes, and the corresponding formally verified interpreter of Lolisa, denoted as FEther. It supports the ERC20 standard and can automatically simultaneously symbolically execute the smart contract programs of Ethereum and verify their reliability and security properties using Hoare logic in Coq. In addition, this work, contributes to solving the problems of automation, inconsistency and reusability in higher-order logic theorem proving.
Bruno Tavares, Filipe Figueiredo Correia, André Restivo, João Pascoal Faria · 5 authors
The applications of the blockchain technology are still being discov-ered. When a new potential disruptive technology emerges, there is a tendency to try to solve every problem with that technology. However, it is still necessary to determine what approach is the best for each type of application. To find how distributed ledgers solve existing problems, this study looks for blockchain frameworks in the academic world. Identifying the existing frameworks can demonstrate where the interest in the technology exists and where it can be miss-ing. This study encountered several blockchain frameworks in development. However, there are few references to operational needs, testing, and deploy of the technology. With the widespread use of the technology, either integrating with pre-existing solutions, replacing legacy systems, or new implementations, the need for testing, deploying, exploration, and maintenance is expected to in-tensify.
Governments across the world are testing different uses of the blockchain for the delivery of their public services. Blockchain hashing–or the insertion of data in the blockchain–is one of the potential applications of the blockchain in this space. With this method, users can apply special scripts to add their data to blockchain transactions, ensuring both immutability and publicity. Blockchain hashing also secures the integrity of the original data stored on central governmental databases. The paper starts by analysing possible scenarios of hashing on the blockchain and assesses in which cases it may work and in which it is less likely to add value to a public administration. Second, the paper also compares this method with traditional digital signatures using PKI (Public Key Infrastructure) and discusses standardisation in each domain. Third, it also addresses issues related with concepts such as “distributed ledger technology” and “permissioned blockchains.” Finally, it raises the question of whether blockchain hashing is an effective solution for electronic governance, and concludes that its value is controversial, even if it is improved by PKI and other security measures. In this regard, we claim that governments need first to identify pain points in governance, and then consider the trade-offs of the blockchain as a potential solution versus other alternatives.
Distributed ledger technology has gained wide popularity and adoption since the emergence of bitcoin in 2008 which is based on proof of work (PoW). It is a distributed, transparent and immutable database of records of all the transactions or events that have been shared and executed among the participants. All the transactions are verified and maintained by multiple nodes across a network without a central authority through a distributed cryptographic mechanism, a consensus protocol. It forms the core of this technology that not only validates the information appended to the ledger but also ensures the order in which it is appended across all the nodes. It is the foundation of its security, accountability and trust. While many researchers are working on improving the current protocol to be quantum resistant, fault-tolerant, and energy-efficient. Others are focused on developing different variants of the protocol, best suited for specific use cases. In this paper, we shall review different consensus protocols of distributed ledger technologies and their implementations. We shall also review their properties, concept and similar-work followed by a brief analysis.
Qi Zhang, Petr Novotny, Salman Baset, Donna N. Dillenberger · 6 authors
The rise of crypto-currencies has spawned great interest in their underlying technology, namely, Blockchain. The central component in a Blockchain is a shared distributed ledger. A ledger comprises series of blocks, which in turns contains a series of transactions. An identical copy of the ledger is stored on all nodes in a blockchain network. Maintaining ledger integrity and security is one of the crucial design aspects of any blockchain platform. Thus, there are typically built-in validation mechanisms leveraging cryptography to ensure the validity of incoming blocks before committing them into the ledger. However, a blockchain node may run over an extended period of time, during which the blocks on the disk can may become corrupted due to software or hardware failures, or due to malicious activity. This paper proposes LedgerGuard, a tool to maintain ledger integrity by detecting corrupted blocks and recovering these blocks by synchronizing with rest of the network. The experimental implementation of LedgerGuard is based on Hyperledger Fabric, which is a popular open source permissioned blockchain platform.
The authors discuss several uses of blockchain and, more generally, distributed ledger technologies outside of cryptocurrencies. They take a pragmatic view, focusing on three main areas: the role of coin economies for “data malls” (specialized data marketplaces), data provenance (a historical record of data and its origins), and “keyless payments,” which are payments that can be made without having to know other users’ cryptographic keys. They also discuss voting and other areas and give a sizable list of academic and nonacademic references. <b>TOPICS:</b>Currency, quantitative methods
At the beginning of 2018, there is a growing belief that blockchain technologies constitute a revolutionary innovation in how we transfer value electronically. In that vein, blockchain may be a suitable complement to ontologies to achieve a big part of the vision of the semantic Web by Tim Berners-Lee. We believe that if this complementarity is to be achieved blockchain and ontologies must co-evolve. In this paper, we focus on what and how to engineer models, methods, designs, and implementations for this co-evolution. As a first step in this co-evolution, we propose a conceptual design of a governance ontology represented as meta-data tags to be embedded and instantiated in a smart contract at the blockchain protocol level. We develop this design by examining and analyzing smart contracts from the infamous The DAO experiment on the Ethereum blockchain. We believe there are two contributions of this paper: it serves to inform and implore the blockchain and ontology communities to recognize and collaborate with each other; and it outlines a roadmap for engineering artifacts to bridge the gap between blockchain community focus on protocol-level blockchain interoperability and the ontology community focus on semantic-level interoperability.
The invention of crypto-currencies as an online means of transactions has lured many IT companies, freelancers and coders to this new form of currency. Nakamoto’s consensus protocol and the invention of the idea behind the blockchain network have given a new platform for this exchange to take place. The growth of blockchain can be accounted by the fact that in 2017, the total global market capital of blockchain based tokens was reported to have reached over $150B. This growth in online transactions and crypto-currencies has invited researchers and developers to work on increasing the efficiency and security of this system. This paper revolves around the 2 hop blockchain model to increase the efficiency and reduce the physical resource requirements of the system. This paper describes the shift from proof of stake (PoS) to proof of authority (PoA) in the 2 hop model proposed by Tuyet Duong. Proof of authority guarantees safety and faster working of the system by using identity as a proof to validate blocks in the blockchain network. This paper also discusses the shortcomings of proof of work (PoW) and proof of stake models. A sequential execution of PoW and PoA is suggested as an alternative in this paper.
Recent attention to Bitcoin and other cryptocurrencies has opened investors and the public to the realm of digital currency. Greater exposure around the world has led to a frenzy of entry into the market and a test into the long-term feasibility of Bitcoin being able to remain a functioning peer-to-peer (P2P), decentralized currency. Its main structure is supported by the Proof-of-Work (PoW) protocol in which users can elect to participate in determining transaction approval and ensuring an honest blockchain. This system relies on elected users to expend computational power and energy to solve puzzles to prove the accuracy of the network’s transactions and create new blocks.\nEach cryptocurrency uses their own method to ensure blockchain accuracy, and this paper will focus on how a Proof-of-Stake (PoS) protocol is a superior algorithm to PoW by assigning mining ability equal to one’s stake within a coin, rather than her energy consumption, among other factors. We will discuss Bitcoin’s PoW as a baseline for our eventual analysis of PoS in terms of advantages and performance metrics. The main factors that can be compared between the two protocols is how each system can prevent itself against a variety of attacks from adversarial users within the network, as well as long-term sustainability.\nFinally, we will use the Cardano (ADA) cryptocurrency by IOHK as a case study for understanding how their Ouroboros Praos PoS protocol works. Our goal is to show how long-term adoption of PoS framework is more realistic from an energy perspective than PoW.
The interrelatedness between computer systems, networks, code, and traditional law and legal frameworks continues to pose a number of important and vexed questions. This report will consider one area of the relationship: legal recognition of distributed ledger technology (DLT) or blockchain applications. Specifically, registers appended to blockchains (thereby creating “blockchain registries”), and “smart contracts” executed on blockchains
Jawad Ali, Toqeer Ali Syed, Shahrulniza Musa, Ali Zahrani
The Internet of Things (IoT) is undergoing rapid growth in the IT industry, but, it continues to be associated with several security and privacy concerns as a result of its massive scale, decentralised topology, and resource-constrained devices. Blockchain (BC), a distributed ledger technology used in cryptocurrency has attracted significant attention in the realm of IoT security and privacy. However, adopting BC to IoT is not straightforward in most cases, due to overheads and delays caused by BC operations. In this paper, we apply a BC technology known as Hyperledgder Fabric, to an IoT network. This technol-ogy introduces an execute-order technique for transactions that separates the transaction execution from consensus, resulting in increased efficiency. We demonstrate that our proposed IoT-BC architecture is sufficiently secure with regard to fundamental se-curity goals i.e., confidentiality, integrity, and availability. Finally, the simulation results are highlighted that shows the performance overheads associated with our approach are as minimal as those associated with the Hyperledger Fabric framework and negligible in terms of security and privacy.
Shaen Corbet, Brian M. Lucey, Andrew Urquhart, Larisa Yarovaya
This paper provides a systematic review of the empirical literature based on the major topics that have been associated with the market for cryptocurrencies since their development \nas a financial asset in 2009. Despite astonishing price appreciation in recent years, cryptocurrencies have been subjected to accusations of pricing bubbles central to the trilemma \nthat exists between regulatory oversight, the potential for illicit use through its anonymity \nwithin a young under-developed exchange system, and infrastructural breaches influenced \nby the growth of cybercriminality. Each influence the perception of the role of cryptocurrencies as a credible investment asset class and legitimate of value.
Savva Shanaev, Arina Shuraeva, Mikhail Vasenin, Maksim Kuznetsov
In this article, an event studies approach is utilized to assess the influence of 51% attacks on proof-of-work (PoW) cryptocurrency prices. The study uses an exhaustive sample of 14 individual attacks on 13 cryptocurrencies. Across multiple event studies techniques, majority attacks on blockchains are consistently shown to immediately decrease corresponding coin prices by 12% to 15%. Significantly negative price response is robust in various event windows. Coin prices do not recover to pre-attack levels one week after the event. There is evidence of pump-and-dump schemes prior to the 51% attack, however the market demonstrates high efficiency after the attacks. 51% attacks are suggested to be a fundamental risk factor for cryptocurrency investments, primarily characteristic of small PoW coins with low hash rates. <b>TOPICS:</b>Currency, risk management, financial crises and financial market history <b>Key Findings</b> • 51% attacks on Proof-of-Work cryptocurrencies decrease their market prices by 12.60% on average. • The effect is robust to different measurement techniques and in various event windows. • There is evidence of insider trading and “pump-and-dump” schemes prior to the attacks.
We study investor sentiment on a non-classical asset such as cryptocurrency using machine learning methods. We account for context-specific information and word similarity by using efficient language modelling tools such as construction of featurized word representations (embeddings) and recursive neural networks (RNNs). We apply these tools for sentence-level sentiment classification and sentiment index construction. This analysis is performed on a novel dataset of 1220K messages related to 425 cryptocurrencies posted on a microblogging platform StockTwits during the period between March 2013 and May 2018. Both in- and out-of-sample predictive regressions are run to test significance of the constructed sentiment index variables. We find that the constructed sentiment indices are informative regarding returns' and volatility predictability of the cryptocurrency market index.
Effective cryptocurrency key management has become an urgent requirement for modern cryptocurrency. Although a large body of cryptocurrency wallet-management schemes has been proposed, they are mostly constructed for specific application scenarios and often suffer from weak security. In this paper, we propose a more effective, usable, and secure cryptocurrency wallet-management system based on semi-trusted social networks, therein allowing users to collaborate with involved parties to achieve some powerful functions and recovery under certain circumstances. Furthermore, we employ an identity-based hierarchical key-insulated encryption scheme to achieve time-sharing authorization and present a semi-trusted portable social-network-based wallet-management scheme that provides the features of security-enhanced storage, portable login on different devices, no-password authentication, flexible key delegation, and so on. The performance analysis shows that our proposed schemes require minimal additional overhead and have low time delays, making them sufficiently efficient for real-world deployment.
We study key leakage in the context of cryptocurrencies. First, we consider the problem of explicit key leakage occurring on open-source intelligence platforms. To do this, we monitor the Pastebin feed from Sep 2017–Mar 2018 to find exposed secret Bitcoin keys, revealing that attackers could have stolen 22.40 BTC worth roughly $178,000 given current exchange rates. Then, we focus on implicit key leakage by exploiting the wrong usage of cryptographic primitives and scan Bitcoin’s blockchain for ECDSA nonce reuse. We systematically outline how an attacker can use duplicate r values to leak nonces and secret keys, which goes beyond the simple case where the same nonce and the same key have been used in conjunction more than once. Our results show that ECDSA nonce reuse has been a recurring problem in the Bitcoin ecosystem and has already been exploited by attackers. In fact, an attacker could have exploited nonce reuse to steal 412.80 BTC worth roughly $3.3 million.