摘要:加密货币比特币的出现带动了区块链技术的蓬勃发展，智能合约技术则是区块链技术中的一个技术 高地． 目前以太坊中的智能合约应用受到大量的关注，创造了海量的价值应用，同时也带来了密集的攻击活动． 随着智能合约的数量越来越多，尤其是智能合约中的代码漏洞也逐渐被许多研究人员和恶意攻击者发现，造成 了一系列重大的经济损失案件． 为了对智能合约技术的稳定性发展提供理论研究基础，文章针对以太坊上已知 的智能合约漏洞进行了介绍、分类和总结，并对智能合约安全漏洞进行详细的原理阐述与场景代码复现．

摘要:Blockchain based smart contracts are computer programs that encode an agreement between non-trusting participants. Smart contracts are executed on a blockchain system if specified conditions are met, without the need of a trusted third party. Blockchains and smart contracts have received increasing and booming attention in recent years, also in academic circles. We carry out a systematic mapping study of all peer-reviewed technology-oriented research in smart contracts. Our interest is twofold, namely to provide a survey of the scientific literature and to identify academic research trends and uptake. We only focus on peer-reviewed scientific publications, in order to identify how academic researchers have taken up smart contract technologies and established scientific outputs. We obtained all research papers from the main scientific databases, and using the systematic mapping method arrived at 188 relevant papers. We classified these papers into six categories, namely, security, privacy, software engineering, application, performance & scalability and other smart contract related topics. We found that the majority of the papers falls into the applications (about 64%) and software engineering (21%) categories. Compared to our 2017 survey [1], we observe that the number of relevant articles has increased about eightfold and shifted considerably towards applications of smart contracts.

摘要:This paper presents an introduction to the current state of art of the Blockchain and Smart Contract technologies. Blockchain is a fast-disruptive technology becoming a key instrument in share economy. The Blockchain-based Smart Contract aim to automatically and securely execute the needed responsibilities of a contract without the support of a centralized execution authority. The Smart Contract runs on top of the Blockchain to facilitate, execute and enforce an agreement between un-trusted parties without the interfere of third party to trust it as this Smart Contract is an executable code that runs with rules on the Blockchain. Smart Contracts have some features that serve the goals of social justice and fairness. The paper presents the basic important information about the structures of the Blockchain and Smart Contract technologies and conduct a comparison between the different methodologies used in the Smart Contracts. The issues faced within the Smart Contract technology are surveyed. The four key issues are identified as: codifying, security, privacy and performance issues. We survey case cases of usage of the Blockchain in various business sectors like real estate, voting system and supply chain. The paper aims to assist a developer to grasp the big picture of the Blockchain technology and to further assist in the decision process of suitability of the technology to a specific application area.

摘要:In the last decade blockchain technology become mainstream research topic because of its decentralized, peer to peer transaction, distributed consensus, and anonymity properties. The blockchain technology overshadows regulatory problem and technical challenges. A smart contract is a set of programs which are self-verifying ,self-executing and tamper resistant. Smart contract with the integration of blockchain technology capable of doing a task in real time with low cost and provide a greater degree of security. This paper firstly, explains the various components and working principle of smart contract. Secondly, identify and analyse the various use cases of smart contract along with the advantage of using smart contract in blockchain application. Lastly, the paper concludes with challenges lie in implementing smart contract the future real-life scenario.

摘要:Smart contract is a code contract and algorithm contract and will become the basisfuture agreements in digital society. Smart Contract utilizes protocols and user interfacesfacilitate all steps of the contracting process.This paper summarized the main technic:characteristics of smart contract and existing problems such as trustworthiness and security anproposed that formal method is applied to the smart contract modeling，model checking and modeverification to support the large-scale generation of smart contract. In this paper，a formverification framework and verification method for smart contract in the whole life circle of smatcontract has been proposed. The paper presented a smart shopping scene，in which Promellanguage is used for modeling a SSC( smart shopping contract) and SPIN is used to simulate anmodel checking to verify the effect of formal method on smart contract.

摘要:Smart contracts are programs that are stored and executed on the Blockchain and can receive, manage and transfer money (cryptocurrency units). Two important problems regarding smart contracts are formal analysis and compiler optimization. Formal analysis is extremely important, because smart contracts hold funds worth billions of dollars and their code is immutable after deployment. Hence, an undetected bug can cause significant financial losses. Compiler optimization is also crucial, because every action of a smart contract has to be executed by every node in the Blockchain network. Therefore, optimizations in compiling smart contracts can lead to significant savings in computation, time and energy. Two classical approaches in program analysis and compiler optimization are intraprocedural and interprocedural analysis. In intraprocedural analysis, each function is analyzed separately, while interprocedural analysis considers the entire program. In both cases, the analyses are usually reduced to graph problems over the control flow graph (CFG) of the program. These graph problems are often computationally expensive. Hence, there has been ample research on exploiting structural properties of CFGs for efficient algorithms. One such well-studied property is the treewidth, which is a measure of tree-likeness of graphs. It is known that intraprocedural CFGs of structured programs have treewidth at most 6, whereas the interprocedural treewidth cannot be bounded. This result has been used as a basis for many efficient intraprocedural analyses. In this paper, we explore the idea of exploiting the treewidth of smart contracts for formal analysis and compiler optimization. First, similar to classical programs, we show that the intraprocedural treewidth of structured Solidity and Vyper smart contracts is at most 9. Second, for global analysis, we prove that the interprocedural treewidth of structured smart contracts is bounded by 10 and, in sharp contrast with classical programs, treewidth-based algorithms can be easily applied for interprocedural analysis. Finally, we supplement our theoretical results with experiments using a tool we implemented for computing treewidth of smart contracts and show that the treewidth is much lower in practice. We use 36,764 real-world Ethereum smart contracts as benchmarks and find that they have an average treewidth of at most 3.35 for the intraprocedural case and 3.65 for the interprocedural case.

摘要:Ethereum is a major blockchain-based platform for smart contracts – Turing complete programs that are executed in a decentralized network and usually manipulate digital units of value. Solidity is the most mature high-level smart contract language. Ethereum is a hostile execution environment, where anonymous attackers exploit bugs for immediate financial gain. Developers have a very limited ability to patch deployed contracts. Hackers steal up to tens of millions of dollars from flawed contracts, a well-known example being “The DAO“, broken in June 2016. Advice on secure Ethereum programming practices is spread out across blogs, papers, and tutorials. Many sources are outdated due to a rapid pace of development in this field. Automated vulnerability detection tools, which help detect potentially problematic language constructs, are still underdeveloped in this area. We provide a comprehensive classification of code issues in Solidity and implement SmartCheck – an extensible static analysis tool that detects them1 . SmartCheck translates Solidity source code into an XML-based intermediate representation and checks it against XPath patterns. We evaluated our tool on a big dataset of real-world contracts and compared the results with manual audit on three contracts. Our tool reflects the current state of knowledge on Solidity vulnerabilities and shows significant improvements over alternatives. SmartCheck has its limitations, as detection of some bugs requires more sophisticated techniques such as taint analysis or even manual audit. We believe though that a static analyzer should be an essential part of contract developers’ toolbox, letting them fix simple bugs fast and allocate more effort to complex issues.

摘要:Nakamoto's famous blockchain protocol enables achieving consensus in a so-called permissionless setting---anyone can join (or leave) the protocol execution, and the protocol instructions do not depend on the identities of the players. His ingenious protocol prevents "sybil attacks" (where an adversary spawns any number of new players) by relying on computational puzzles (a.k.a. "moderately hard functions") introduced by Dwork and Naor (Crypto'92). Recent work by Garay et al (EuroCrypt'15) and Pass et al (manuscript, 2016) demonstrate that this protocol provably achieves consistency and liveness assuming a) honest players control a majority of the computational power in the network, b) the puzzle-hardness is appropriately set as a function of the maximum network delay and the total computational power of the network, and c) the computational puzzle is modeled as a random oracle. Assuming honest participation, however, is a strong assumption, especially in a setting where honest players are expected to perform a lot of work (to solve the computational puzzles). In Nakamoto's Bitcoin application of the blockchain protocol, players are incentivized to solve these puzzles by receiving rewards for every "block" (of transactions) they contribute to the blockchain. An elegant work by Eyal and Sirer (FinancialCrypt'14), strengthening and formalizing an earlier attack discussed on the Bitcoin forum, demonstrates that a coalition controlling even a minority fraction of the computational power in the network can gain (close to) 2 times its "fair share" of the rewards (and transaction fees) by deviating from the protocol instructions. In contrast, in a fair protocol, one would expect that players controlling a φ fraction of the computational resources to reap a φ fraction of the rewards. We present a new blockchain protocol---the FruitChain protocol---which satisfies the same consistency and liveness properties as Nakamoto's protocol (assuming an honest majority of the computing power), and additionally is δ-approximately fair: with overwhelming probability, any honest set of players controlling a φ fraction of computational power is guaranteed to get at least a fraction (1-δ)φ of the blocks (and thus rewards) in any Ω(κ/δ) length segment of the chain (where κ is the security parameter). Consequently, if this blockchain protocol is used as the ledger underlying a cryptocurrency system, where rewards and transaction fees are evenly distributed among the miners of blocks in a length κ segment of the chain, no coalition controlling less than a majority of the computing power can gain more than a factor (1+3δ) by deviating from the protocol (i.e., honest participation is an n/2-coalition-safe 3δ-Nash equilibrium). Finally, the FruitChain protocol enables decreasing the variance of mining rewards and as such significantly lessens (or even obliterates) the need for mining pools.

摘要:Cryptocurrencies record transactions in a decentralized data structure called a blockchain. Two of the most popular cryptocurrencies, Bitcoin and Ethereum, support the feature to encode rules or scripts for processing transactions. This feature has evolved to give practical shape to the ideas of smart contracts, or full-fledged programs that are run on blockchains. Recently, Ethereum’s smart contract system has seen steady adoption, supporting tens of thousands of contracts, holding millions dollars worth of virtual coins. In this paper, we investigate the security of running smart contracts based on Ethereum in an open distributed network like those of cryptocurrencies. We introduce several new security problems in which an adversary can manipulate smart contract execution to gain profit. These bugs suggest subtle gaps in the understanding of the distributed semantics of the underlying platform. As a refinement, we propose ways to enhance the operational semantics of Ethereum to make contracts less vulnerable. For developers writing contracts for the existing Ethereum system, we build a symbolic execution tool called Oyente to find potential security bugs. Among 19, 366 existing Ethereum contracts, Oyente flags 8, 833 of them as vulnerable, including the TheDAO bug which led to a 60 million US dollar loss in June 2016. We also discuss the severity of other attacks for several case studies which have source code available and confirm the attacks (which target only our accounts) in the main Ethereum network.

摘要:With the exponential rise in the number of devices, the Internet of Things (IoT) is geared toward edge-centric computing to offer high bandwidth, low latency, and improved connectivity. In contrast, legacy cloud-centric platforms offer deteriorated bandwidth and connectivity that affect the quality of service. Edge-centric Internet of Things-based technologies, such as fog and mist computing, offer distributed and decentralized solutions to resolve the drawbacks of cloud-centric models. However, to foster distributed edge-centric models, a decentralized consensus system is necessary to incentivize all participants to share their edge resources. This paper is motivated by the shortage of comprehensive reviews on decentralized consensus systems for edge-centric Internet of Things that elucidates myriad of consensus facets, such as data structure, scalable consensus ledgers, and transaction models. Decentralized consensus systems adopt either blockchain or blockchainless directed acyclic graph technologies, which serve as immutable public ledgers for transactions. This paper scrutinizes the pros and cons of state-of-the-art decentralized consensus systems. With an extensive literature review and categorization based on existing decentralized consensus systems, we propose a thematic taxonomy. The pivotal features and characteristics associated with existing decentralized consensus systems are analyzed via a comprehensive qualitative investigation. The commonalities and variances among these systems are analyzed using key criteria derived from the presented literature. Finally, several open research issues on decentralized consensus for edge-centric IoT are presented, which should be highlighted regarding centralization risk and deciencies in blockchain/blockchainless solutions.

摘要:The block chain technology is changing rapidly. The block chain guarantees the integrity of the book through a specific consensus of the participants. In the past, the block chain technology had a limited range of applications. However, the use of block chain technology is gradually expanding as smart contracts that can formulate general business logic are mentioned. Already studied the components of smart contracts in other studies and proposed the possibility of extending them on the basis of ontology. And research on securing traceability of smart contract based on ontology has been carried out. However, research on various transactions constituting smart contracts is lacking. In this paper, the constituent elements of smart contract are analyzed and expressed by ontology. And the process of negotiating the components is represented by each transaction. Finally, we construct the component represented by the ontology as XML by including the state information in the transaction. In this way, the smart contract is represented in a formal language that contains state information. It also laid the foundation for a smart contract that can be reused and verified.

摘要:Smart contracts can automatically perform the contract terms according to the received information, and it is one of the most important research fields in digital society. The core of smart contracts is algorithm contract, that is, the parties reach an agreement on the contents of the contract and perform the contracts according to the behaviors written in certain computer algorithms. It not only needs to make sure about the correctness of smart contracts code, but also should provide a credible contract code execution environment. Blockchain provides a trusted execution and storage environment for smart contracts by the distributed secure storage, consistency verification and encryption technology. Current challenge is how to assure that smart contract can be executed as the parties’ willingness. This paper introduces formal modeling and verification in formal methods to make smart contract model and verify the properties of smart contracts. Formal methods combined with smart contracts aim to reduce the potential errors and cost during contract development process. The description of a general and formal smart contract template is provided. The tool of model checking, SPIN, is used to verify the correctness and necessary properties for a smart contract template. The research shows model checking will be useful and necessary for smart contracts.

摘要:Blockchain as a distributed computing platform enables users to deploy pieces of software (known as smart contracts) for a wealth of next-generation decentralized applications without involving a trusted third-party. The advantages of smart contracts do, however, come at a price. As with most technologies, there are potential security threats, vulnerabilities and various other issues associated with smart contracts. Writing secure and safe smart contracts can be extremely difficult due to various business logics, as well as platform vulnerabilities and limitations. Formal methods have recently been advocated to mitigate these vulnerabilities. This paper aims to provide a first-time study on current formalization research on all smart contract-related platforms on blockchains, which is scarce in the literature. To this end, a timely and rigorous systematic review to examine the state-of-the-art research and achievements published between 2015 and July 2019 is provided. This study is based on a comprehensive review of a set of 35 research papers that have been extracted from eight major online digital databases. The results indicate that the most common formalization technique is theorem proving, which is most often used to verify security properties relating to smart contracts, while other techniques such as symbolic execution and model checking were also frequently used. These techniques were most commonly used to verify the functional correctness of smart contracts. From the language and automation point of views, there were 12 languages (domain specific/specification/general purpose) proposed or used for the formalization of smart contracts on blockchains, while 15 formal method-specific automated tools/frameworks were identified for mitigating various vulnerabilities of smart contracts. From the results of this work, we further highlight three open issues for future research in this emerging domain including: formal testing, automated verification of smart contracts, and domain specific languages (DSLs) for Ethereum. These issues suggest the need for additional, in-depth research. Our study also provides possible future research directions.

摘要:Blockchain as a distributed computing platform enables users to deploy pieces of software (known as smart contracts) for a wealth of next-generation decentralized applications without involving a trusted third-party. The advantages of smart contracts do, however, come at a price. As with most technologies, there are potential security threats, vulnerabilities and various other issues associated with smart contracts. Writing secure and safe smart contracts can be extremely difficult due to various business logics, as well as platform vulnerabilities and limitations. Formal methods have recently been advocated to mitigate these vulnerabilities. This paper aims to provide a first-time study on current formalization research on all smart contract-related platforms on blockchains, which is scarce in the literature. To this end, a timely and rigorous systematic review to examine the state-of-the-art research and achievements published between 2015 and July 2019 is provided. This study is based on a comprehensive review of a set of 35 research papers that have been extracted from eight major online digital databases. The results indicate that the most common formalization technique is theorem proving, which is most often used to verify security properties relating to smart contracts, while other techniques such as symbolic execution and model checking were also frequently used. These techniques were most commonly used to verify the functional correctness of smart contracts. From the language and automation point of views, there were 12 languages (domain specific/specification/general purpose) proposed or used for the formalization of smart contracts on blockchains, while 15 formal method-specific automated tools/frameworks were identified for mitigating various vulnerabilities of smart contracts. From the results of this work, we further highlight three open issues for future research in this emerging domain including: formal testing, automated verification of smart contracts, and domain specific languages (DSLs) for Ethereum. These issues suggest the need for additional, in-depth research. Our study also provides possible future research directions.

摘要:Smart contract applications based on Ethereum blockchain have been widely used in many fields. They are developed by professional developers using specialized programming languages like solidity. It requires high requirements on knowledge of the specialized field and the proficiency in contract programming. Thus, it is hard for normal users to design a usable smart contract based on their own demands. Most current studies about smart contracts focus on the security of coding while lack of friendly tools for users to design the specialized templates of contracts coding. This paper provides a visual and user-defined smart contract designing systems. It makes the development of domain-specific smart contracts simpler and visualization for contract users. The system implements the domain-specific features extraction about the crawled data sets of smart contract programs by TF-IDF and K-means++ clustering algorithm. Then, it achieves the automatic generation of unified basic function codes by Char-RNN (improved by LSTM) based on the domain-specific features. The system adopts Google Blockly and links the generated codes with UI controls. Finally, it provides a set of specialized templates of basic functions for users to design smart contracts by the friendly interface. It reduces the difficulty and costs of contract programming. The paper offers a case study to design contracts by users. The designed contracts were validated on the existing system to implement the food trading and traders’ credit evaluation. The experimental results show that the designed smart contracts achieve good integration with the existing system and they can be deployed and compiled successfully.