## 5 Academic Efforts to Blockchain-Based Supply Chain Management:
### Efforts against Computational Attacks
#### 5.2.2 Security to Smart Contracts and Their Execution Environment  
Most critical attacks on smart home are exploiting the vulnerabilities in a smart contract and executing them in a compromised way. Recently, several tools have been developed to identify vulnerabilities in smart contract. These vulnerabilities include (but not limited to) inconsistent balance, re-entrance, transaction disorder, tampering block timestamp, failed exception handling, call stack depth, over- and underflow of numeric values, asynchronous send operation, no restricted write operation, and non-validated arguments. To identify such vulnerabilities, existing tools perform static analysis on source code of the smart contract, static analysis on the byte code of the smart contract, dynamic analysis of the contract execution, symbolic analysis of the contract code and execution, and verification based analysis of the the contract.  
Since the execution of smart contracts enables mutually untrusted entities to interact without relying on trusted third parties. Therefore, it is required to write a contract that is free from any vulnerability. Security [57] is one of the tools with a rigorous security-analyzer to identify security vulnerabilities in Ethereum based smart contracts. To this end, Securify is scalable, fully automated, and is able to detect the safe/un-safe behaviors of smart contracts on a given model/property. Securify's performs security analysis in two steps. First, it generates dependency graph from the contract, and symbolically analyzes the dependency graph to extract precise semantic information from the contract code. Then, based on the extract semantics, it checks compliance and violation patterns that capture sufficient conditions for proving if a property holds or not. Furthermore, to enable extensibility, all patterns are modelled in a domain-specific language. Securify has been publicly released and has analyzed more than 18K contracts submitted by its users, and is also regularly used to conduct security audits by experts. although, Securify helps to detect security vulnerabilities in smart contracts, but it fails to detect those vulnerabilities which are raised by business operations of the involved stakeholders and consumers.  
Also, ZEUS framework is developed by [PERSON] et al., [55] to verify the correctness and validate the fairness of smart contracts. The framework perceives correctness as adherence to safe programming practices, while fairness is validated by finding whether a smart contract following the higher-level business logic. To this end, ZEUS leverages both abstract interpretation and symbolic model checking, along with the power of constrained horn clauses to efficiently verify the security of contracts. The prototype implementation of the framework was evaluated on almost 22.4 K smart contracts of Ethereum and Fabric blockchain platforms, identifying 94.6% of contracts as vulnerable. Such vulnerabilities contain cryptocurrency transactions of more than $0.5 billion. Furthermore, the framework was proven correct with zero false-negative and very low false-positive rates, had better performance as compared to state-of-the-art. The major drawback of the framework is its limitation to detect only those vulnerabilities that involve integer expressions. It failed to identify any external vulnerabilities,like the ones due to the language or its execution environment.