A Survey on Security Verification of Blockchain Smart Contracts <s> B. SMART CONTRACTS <s> Smart contracts combine protocols with user interfaces to formalize and secure relationships over computer networks. Objectives and principles for the design of these systems are derived from legal principles, economic theory, and theories of reliable and secure protocols. Similarities and differences between smart contracts and traditional business procedures based on written contracts, controls, and static forms are discussed. By using cryptographic and other security mechanisms, we can secure many algorithmically specifiable relationships from breach by principals, and from eavesdropping or malicious interference by third parties, up to considerations of time, user interface, and completeness of the algorithmic specification. This article discusses protocols with application in important contracting areas, including credit, content rights management, payment systems, and contracts with bearer. <s> BIB001 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> B. SMART CONTRACTS <s> Computational law is an approach to automated legal reasoning focusing on semantically rich laws, regulations, contract terms, and business rules in the context of electronically-mediated actions. Current computational tools for electronic commerce fall short of the demands of business, organizations, and individuals conducting complex transactions over the web. However, the growth of semantic data in the world of electronic commerce and online transactions, coupled with grounded rulesets that explicitly reference that data, provides a setting where applying automated reasoning to law can yield fruitful results, reducing inefficiencies, enabling transactions and empowering individuals with knowledge of how laws affect their behavior. <s> BIB002 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> B. SMART CONTRACTS <s> Smart contracts---stateful executable objects hosted on blockchains like Ethereum---carry billions of dollars worth of coins and cannot be updated once deployed. We present a new systematic characterization of a class of trace vulnerabilities, which result from analyzing multiple invocations of a contract over its lifetime. We focus attention on three example properties of such trace vulnerabilities: finding contracts that either lock funds indefinitely, leak them carelessly to arbitrary users, or can be killed by anyone. We implemented Maian, the first tool for specifying and reasoning about trace properties, which employs interprocedural symbolic analysis and concrete validator for exhibiting real exploits. Our analysis of nearly one million contracts flags 34, 200 (2, 365 distinct) contracts vulnerable, in 10 seconds per contract. On a subset of 3, 759 contracts which we sampled for concrete validation and manual analysis, we reproduce real exploits at a true positive rate of 89%, yielding exploits for 3, 686 contracts. Our tool finds exploits for the infamous Parity bug that indirectly locked $200 million US worth in Ether, which previous analyses failed to capture. <s> BIB003
Smart contract is a series of symbolic protocols that can be executed by contract participants. In 1997, Szabo BIB001 rewrote the smart contract publication as the ''formalization and security of public network relationships'', which further improved the theoretical basis of smart contracts and the application of security protocols. However, smart contracts were not well developed due to the lack of relevant theoretical techniques and digital systems which support programmable smart contracts at that time. This is mainly reflected in three aspects. First, there are no digital assets that can be directly manipulated. Using an auto-executed contract to transfer the ''assets'' is the essence of a smart contract. But direct manipulation of real-world property, stocks, and other physical assets have become a major problem through computers. Second, the limitation of computational law BIB002 is a big problem. Computational law is an approach to automated legal reasoning focusing on semantically rich laws, regulations, contract terms, and business rules in the context of electronically-mediated actions. Traditional computational law focuses on analyzing and describing laws to help people understand and formulate real-life laws. However, the emergence of smart contracts requires that laws be converted into executable code and achieving legal interaction between the machines. Third, lacking of a credible environment is the key point. For the auto-executed contract, the participants can only see the results after the execution, but do not know the intermediate process at all. However, there are several properties of the contract execution which need to be guaranteed, including contract execution correctness, non-tampering, and semantic equivalence of the contract with the participant intentions. Therefore, in such an environment where theory and technology are seriously scarce, the development of smart contracts has been stagnant. In recent years, the decentralized blockchain technology has provided a trusted environment for smart contracts that does not require third-party intervention. Coupled with the rapid development of artificial intelligence, which has greatly promoted the progress and improvement of computational law, smart contracts have once again attracted people's attentions. Unfortunately, using vulnerabilities of smart contracts to attack contracts themselves has gradually increased. In 2018, Nikolic et al. BIB003 used the MAIAN analysis tool to perform a security analysis of nearly 1 million smart contracts, in 10 seconds per contract. Their analysis flags that 34,200 smart contracts are vulnerable. For further research, they randomly sampled 3,759 contracts in vulnerable contracts, and found that 3,686 smart contracts had a 89% probability of vulnerability. Therefore, the issue of security verification of smart contracts deserves imperative and comprehensive studies.