| In Traditional Financial Systems,a trust intermediate organization is needed to process a valuable transaction on a secure network.This traditional system has some problems.It is the first problem that this mechanism will take a long transaction time,and another problem is that the mechanism will result in the high transaction fee.In order to resolve these two problems and other issues,Blockchain that is a decentralized platform was proposed in 2008.One of the most important features of Blockchain technology is the ability that communications can be performed between mutually distrustful parties without relying on a trusted third-party entity.This communication can be implemented by using smart contract.Smart contract is a Turing-complete program that run on the Blockchain.But the development of smart contract has two critical problems.Smart contract generally runs on a distributed and permissionless network,which are highly vulnerable.Vulnerability in smart contract is one form of security issue.These vulnerabilities allow an attacker to extract currency from contracts.The second issue is that smart contract can't be changed or upgraded after it is deployed on a decentralized Blockchain network.It is well known as an immutable feature of smart contract.Due to these two problems,smart contract must be correct and secure before deploying it into Blockchain network.As a result,Blockchain applications based on smart contract should be checked and verified to ensure smart contract implementation's correctness,security,and safety.This thesis firstly studies smart contracts' security vulnerabilities in Ethereum.Secondly,existing formal verification methods for smart contract are investigated.Finally,we verify and test the ERC20 smart contracts by using the Remix IDE tool and also show how the tool solves the reentrance problem by adjusting the gas limit and show how it detects vulnerabilities such as unchecked call and timestamp dependence. |
PDF Full Text Request