| Summary: | To address the frequent security incidents of token smart contracts,this paper proposes a formal modeling and verification method based on integer overflow vulnerabilities of token smart contracts.The DAO and BEC vulnerability attacks are analyzed,and on this basis the security attributes of token smart contracts are defined.Then the method introduces global variables,numeric comparison and other constraints to extend the modeling language of token smart contracts,so as to enable it to support the formal representation of various statements of smart contracts.Finally,the idea of mathematical induction is used to optimize the model verification procedure of the SmartVerif tool in order to avoid infinite traversal of state space.Experimental results show that the proposed method can successfully find out the integer overflow vulnerabilities of token smart contracts,and has strong versatility.
|
|---|
