A Survey on Security Verification of Blockchain Smart Contracts <s> 1) SETTING STANDARDS <s> In this position paper, we consider some foundational topics regarding smart contracts (such as terminology, automation, enforceability, and semantics) and define a smart contract as an automatable and enforceable agreement. We explore a simple semantic framework for smart contracts, covering both operational and non-operational aspects, and describe templates and agreements for legally-enforceable smart contracts, based on legal documents. Building upon the Ricardian Contract, we identify operational parameters in the legal documents and use these to connect legal agreements to standardised code. We also explore the design landscape, including increasing sophistication of parameters, increasing use of common standardised code, and long-term research. <s> BIB001 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 1) SETTING STANDARDS <s> Blockchain technology has emerged as a solution to consistency problems in peer to peer networks. By now, it has matured as a solution to a range of use cases in which it can effectively provide the notion of third party trust without the need for a trusted (physical) third party, which makes it an attractive coordination mechanism for distributed systems. To promote the wide adoption of this technology, we yet lack mechanisms that make the specification and interpretation of smart contracts accessible to a broader audience. In this work, we propose a modeling approach that supports the semi-automated translation of human-readable contract representations into computational equivalents in order to enable the codification of laws into verifiable and enforceable computational structures that reside within a public blockchain. We identify smart contract components that correspond to real world institutions, and propose a mapping that we operationalize using a domain-specific language in order to support the contract modeling process. We explore this capability based on selected examples and plot out directions for future research on smart contracts. <s> BIB002 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 1) SETTING STANDARDS <s> Often, we wish to let parties alter or undo a contract that has been made. Toward this end, contract law has developed a set of traditional tools for altering and undoing contracts. Unfortunately, these tools often fail when applied to smart contracts. It is therefore necessary to define a new set of standards for the altering and undoing of smart contracts. These standards might ensure that the tools we use to alter and undo smart contracts achieve their original (contract law) goals when applied to this new technology. This paper develops such a set of standards and, then, to prove their worth as a framework, applies to them to an existing smart contract platform (Ethereum). <s> BIB003 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 1) SETTING STANDARDS <s> Smart contracts are computer programs that can be consistently executed by a network of mutually distrusting nodes, without the arbitration of a trusted authority. Because of their resilience to tampering, smart contracts are appealing in many scenarios, especially in those which require transfers of money to respect certain agreed rules (like in financial services and in games). Over the last few years many platforms for smart contracts have been proposed, and some of them have been actually implemented and used. We study how the notion of smart contract is interpreted in some of these platforms. Focussing on the two most widespread ones, Bitcoin and Ethereum, we quantify the usage of smart contracts in relation to their application domain. We also analyse the most common programming patterns in Ethereum, where the source code of smart contracts is available. <s> BIB004
Setting standards is of great significance in regulating the programming of contracts. In order to find out the rules of programming, some studies focused on the large quantity of experiments. Delmolino et al.  used a large number of contracts to find common mistakes that were easy to occur during the writing process, and presented programming guidance to avoid these errors. Bartoletti and Pompianu BIB004 extensively analyzed the smart contracts related to Bitcoin and Ethereum applications, and provided a programming model for writing the correct contract. While, the other work started from the theory, they combined the knowledge of computational law to design the semantic framework of smart contracts BIB001 , BIB002 . Through semantic transformation, the solidity contract was generated and finally tested. In addition, Marino and Juels BIB003 proposed a standard for changing and revoking contracts. Applying the framework to Ethereum can make it easier to modify or cancel the released smart contracts, which had great value in maintaining the correctness of contracts.