摘要: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.

摘要:区块链与 5G 都是新型技术，二者结合的巨大潜力和价值已日益凸显。5G 作为通信基础设施，如同“信息高速公路”一样，为庞大 数据量和信息量的传递提供了可能性，同时，它也带来了更为高效和 可靠的传输速度。区块链作为去中心化、隐私保护的技术工具，协助 5G 解决可靠、安全、隐私、信任等问题，提升网络信息安全和服务效率，创新商业模式。5G 和区块链有效地融合，将促进整个社会生 产方式的改进和生产力的发展。

摘要: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.

摘要:Developing smart contract decentralised application based systems typically involves writing code for various platforms, from the smart contract code residing on the underlying distributed ledger technology implementation to back end oracles and front end websites or mobile apps. In addition to the different technologies used for the different parts, the programmer is also burdened with implementing communication channels between the various parts. In this paper we propose a unified programming model allowing for developers to build such systems through a single code artifact, using a macroprogramming approach.

摘要:This research addresses the issue that in-depth programming knowhow is needed to read and write smart contracts. The goal was making the creation of smart contracts accessible to non-computer experts by the use of a graphical programming language (Blockly). We used modularization to capture the complexity of legal contracts and developed a mapping process to transform the graphical representation to the smart contract programming language Solidity. We applied our approach to legal purchase agreements and proved the practicality of our solution and explored its limitations. A prototype was built to show the feasibility of our approach. Our industry partner challenged the prototype by applying it to the contract creation process. We consider our work as the first step towards an application of smart contracts in the nonIT world and outside the today’s expert shaped ecosystem of blockchain specialists. Several continuative research questions have been derived from our finding and are listed at the end of this paper.

摘要:Emerging blockchain technology has introduced a new challenge to the distributed system research: Can Byzantine fault-tolerance protocols scale up to, for example, hundreds of nodes? In this work, we introduce HiBFT, a hierarchical Byzantine fault-tolerance protocol to address the problem. The core idea is to divide replicas into groups and exchange consensus messages among groups, thus avoiding the necessity of message broadcasting. The motivation for such approach bases on the hierarchical property of network architecture in permissioned block chains, our target deployments. HiBFT works very much in the same way as the classical Practical Byzantine Fault-Tolerance protocol. However, it replaces the concept of physical replica with a logical one that represents a replica group. As such, protocol message complexity can be reduced from O(N2) to O(s2) where N and s are the total number of replicas and the number of groups. Additionally, using threshold signature scheme for representing a logical group results in two important improvements: The cost of signature verification is significantly reduced at each replica; blocks can be secured more effectively in terms of signature size. Our protocol guarantees safety and liveness under partially synchronous assumption with a correctness proof. Our experiment results show that the protocol can scale up to hundred of nodes.

摘要: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.

摘要:In this work, we acknowledge the need for software engineers to devise specialized tools and techniques for blockchain-oriented software development. Ensuring effective testing activities, enhancing collaboration in large teams, and facilitating the development of smart contracts all appear as key factors in the future of blockchain-oriented software development.

摘要:Smart contracts play an advent role in automated business participation by rendering collaboration processes more time efficient, cost-effective and establishing more transparency. Smart contracts facilitate trust-less systems, without the need for intervention from third-party intermediaries. Existing smartcontract languages mainly focus on technical utility and do not take into consideration social and legally relevant issues, e.g., lack of semantics, ontological completeness, and so on. In this research, we address the gap by developing with rigorous means a smart contract’s language that aims to be legally relevant, and that comprises socio-technical utility for crossorganizational business collaboration. The proposed language seeks to retain the strengths of the already existing languages of different generations while eluding their limitations. We aim to identify and implement abstract grammar patterns for a smart- contract language that has the expected application utility and verifiability. We evaluate the developed language based on automating industry-collaboration cases with our novel smartcontract language to test the suitability, utility and expressiveness.

摘要:The smart contract on the blockchain allows credible transactions without a third party. These transactions are traceable and irreversible. The deployment and implementation of smart contracts in Ethernet will consume some gas, which will directly affect the cost of smart contracts. In order to reduce the consumption of gas during the execution of smart contracts, this article proposes an optimization algorithm for generating business process smart contracts. First, business process modeling notation (BPMN) models are extended to Petri nets. Second, Petri nets are simplified to find nodes in BPMN models that can be considered fusion tasks. Using new mapping rules from the BPMN model to solidity language, BPMN model is generated into Ethereum Smart contract model. In the BPMN models with multilayer fusion task, experimental results show that the proposed algorithm can save 15% gas on average for business processes with multiple fusion tasks.

摘要:Abstract—As the number of Web APls is rapidly increasing, itis an urgent issue to discover qualified Web APis and providevalue-added services by orchestrating them. How ever, most ofthe interface descriptions of Web APls are informal, and theWeb API SLA contracts, w hich are a key to quality of servicesorchestration，requirc manual operations at the consumers.Meanwhile，applying the blockchain，the distributed ledgertechnology， to various domains beyond Fintech is attractingattention because of its fault-tolerant and anti-4ampering.However,it isn't applied to Web API SLA contracts,yet.inthis article，the authors propose a formal specificationdescription of Web APls together with its associated SLAspecifications based on RDF,and an SLA contract mcthodbased on the common SLA contract platfor m built on theblockchain. We implementedtheprototype of the SLAcontract platform,and applied itto theexamples fordemonstrating itsfeasibility.Thosc experiences prove thcfe asibility of the proposed Web API SLA contract method andits supporting platform.

摘要:为解决区块链在查询方面存在的访问方法支持有限、查询功能单一、查询效率低等不足，提出一种区块链数据的 关系查询解决方案FabricSQL,将Hyperledged Fabric与MySQL结合,把实时存储的区块链有效交易数据同步存储到SQL数据库中。为防止数据库中的数据被篡改，提出一种交易数据存储验证机制，在SQL数据存储时使用Salt加密方法,在数据顺序追加时引入区块链前哈希的思想防止作恶,在用户访问时，进行数据的一致性校验，返回需求数据和校验结果，保证数据的安全性。在设计的实验模型和基于Fabric的区块链系统上进行多项查询性能的对比实验,实验结果表明,FabricSQL同时拥有区块链和关系型数据库的良好特性。

摘要:Due to limited computing and storage resources, light clients and full nodes coexist in a typical blockchain system. Any query from light clients must be forwarded to full nodes for execution, and light clients verify the integrity of query results returned. Since existing authenticated query based on Authenticated Data Structure (ADS) suffers from significant network, storage and computing overheads by virtue of Verification Objects (VO), an alternative way turns to Trust Execution Environment (TEE), with which light clients have no need to receive or verify any VO. However, state-of-the-art TEE cannot deal with largescale application conveniently due to limited secure memory space (i.e, the size of enclave in Intel SGX is only 128MB). Hence, we organize data hierarchically in both trusted (enclave) and untrusted memory and only buffer hot data in enclave to reduce page swapping overhead between two kinds of memory. Security analysis and empirical study validate the effectiveness of our proposed solutions.