A Survey on Security Verification of Blockchain Smart Contracts <s> 2) BEHAVIOR-BASED FORMAL VERIFICATION <s> Many software applications are based on collaborating, yet competing, agents or virtual organisations exchanging services. Contracts, expressing obligations, permissions and prohibitions of the different actors, can be used to protect the interests of the organisations engaged in such service exchange. However, the potentially dynamic composition of services with different contracts, and the combination of service contracts with local contracts can give rise to unexpected conflicts, exposing the need for automatic techniques for contract analysis. In this paper we look at automatic analysis techniques for contracts written in the contract language $\mathcal{CL}$. We present a trace semantics of $\mathcal{CL}$ suitable for conflict analysis, and a decision procedure for detecting conflicts (together with its proof of soundness, completeness and termination). We also discuss its implementation and look into the applications of the contract analysis approach we present. These techniques are applied to a small case study of an airline check-in desk. <s> BIB001 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 2) BEHAVIOR-BASED FORMAL VERIFICATION <s> This article presents the FormaLex toolset, an approach to legislative drafting that, based on the similarities between software specifications and some types of regulations, uses off-the-shelf LTL model checkers to perform automatic analysis on normative systems. <s> BIB002 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 2) BEHAVIOR-BASED FORMAL VERIFICATION <s> The notion of smart contracts in distributed ledger systems have been hailed as a safe way of enforcing contracts between participating parties. However, unlike legal contracts, which talk about ideal behaviour and consequences of not adhering to such behaviour, smart contracts are by their very nature executable code, giving explicit instructions on how to achieve compliance. Executable specification languages, particularly Turing complete ones, are notoriously known for the difficulty of ensuring correctness, and recent incidents which led to huge financial losses due to bugs in smart contracts, have highlighted this issue. In this paper we show how standard techniques from runtime verification can be used in the domain of smart contracts, including a novel stake-based instrumentation technique which ensures that the violating party provides insurance for correct behaviour. The techniques we describe have been partially implemented in a proof-of-concept tool ContractLarva, which we discuss in this paper. <s> BIB003 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 2) BEHAVIOR-BASED FORMAL VERIFICATION <s> 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. <s> BIB004 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 2) BEHAVIOR-BASED FORMAL VERIFICATION <s> Blockchain technology has attracted increasing attention in recent years. One reason of this new trend is the introduction of on-chain smart contracts enabling the implementation of decentralized applications in trust-less environments. Along with its adoption, attacks exploiting smart contract vulnerabilities are inevitably growing. To counter these attacks and avoid breaches, several approaches have been explored such as documenting vulnerabilities or model checking using formal verification. However, these approaches fail to capture the Blockchain and users behavior properties. In this paper, we propose a novel formal modeling approach to verify a smart contract behavior in its execution environment. We apply this formalism on a concrete smart contract example and analyze its breaches with a statical model checking approach. <s> BIB005
Model checking is well adopt in behavior-based verification. It can conveniently model the interaction between the user and the program to verify whether the smart contract can interact with the user in a reliable and secure way. Some good examples of behavior-based formal validation are demonstrated as follows. Ellul and Pace BIB003 proposed a runtime verification method. It was a novel state-based technique which ensured that the violating party provided insurance for correct behavior. They used the finite state machine to model the contracts, and this method had been partially implemented in a proofof-concept tool ContractLarva. Their method refered to the methods proposed by Fenech et al. BIB001 and Gorin et al. BIB002 , which validated the properties of the contract. Then, Bigi et al.  combined game theory with formal methods and proposed a probabilistic formal model to verify smart contracts. They first analyzed the logic of the smart contract through game theory, then constructed a probabilistic formal model for the contract, and finally used the PRISM tool to verify the model. It was published in the early research stage of blockchain smart contracts, ensuring the safety and reliability of smart contracts through rigorous mathematical proofs. Similarly, Bai et al. BIB004 also proposed a model checking method. They used the Promela language to model a shopping contract and used the SPIN tool to verify whether the logic of the shopping contract was correct. These two papers validates from the perspective of user-program interaction behavior to determine whether the attributes are satisfied or not. In addition to the above method, Abdellatif and Brousmiche BIB005 proposed a new verification method in 2018, which not only considered the interaction between users and programs, but also considered the interaction between programs and the environment, further advancing the development of using formal methods to verify smart contracts. They used the BIP (Behavior Interaction Priorities) framework to model components for smart contracts, blockchain, users, miners, trading pools, and attackers. Each component in the model was similar to an automatic state machine, which interacted through ports to enable dynamic interaction. Then they used the Statistical Model Checking (SMC) tool to verify whether the model satisfies a certain attribute. Specifically, the expected properties of the smart contract were described using the PB-LTL (Probabilistic Bounded Linear Time Logic) formula, which utilized probability to indicate the degree to which the model satisfied an attribute. This method simulated the whole process of smart contract execution (from being mined by miners to completing contracts) and modeled the attack's behavior. They found that attackers were the most likely to succeed in the process of interacting with the program, and that the likelihood of a successful attack would be significantly increased when the transaction was too long in the pending transaction pool.