Abstract: It is difficult to detect and verify comprehensively new token trading backdoor vulnerabilities and owner authority transfer vulnerabilities in smart contracts. Based on static semantic analysis and symbolic execution technology, this paper proposes a method to comprehensively and effectively detect and verify the token trading vulnerability and authority transfer vulnerability at the source code and bytecode levels. The method firstly converts contract source code into bytecode through contract collection and preprocessing. Secondly, global sensitive variables “balance” and “owner” are located through static semantic analysis. Then the state space is constructed and the transaction sequence is simulated by symbolic variables. The method performs symbolic execution on the contract, and establishes constraints through the features of vulnerability models. Finally, the method uses satisfiability modulo theories (SMT) solver to solve the constraint. The method is tested on ethereum, binance smart chain mainnet and a part of smart contract CVE vulnerability sets. The experimental results show that the method proposed in this paper can effectively detect the new token trading backdoor vulnerability as well as the owner authority transfer vulnerability.Key words smart contract; vulnerability detection; symbolic execution; program analysis; blockchain security

Key words: smart contract, vulnerability detection, symbolic execution, program analysis, blockchain security

摘要： 针对智能合约中出现的新型代币买卖后门漏洞以及owner权限转移漏洞难以全面检测和验证的问题，基于静态语义分析和符号执行技术，提出了一种在源代码和字节码层面可以全面有效挖掘代币买卖漏洞和权限转移漏洞的检测和验证方法.该方法首先通过合约收集和预处理，将合约源代码转换为字节码；其次通过静态语义分析，对全局敏感变量“balance”以及“owner”进行定位；然后通过符号化变量构建状态空间，模拟交易序列，对合约进行符号执行；最后通过漏洞模型特征建立约束条件，使用约束求解器对约束进行求解.在以太坊、币安智能链主网上以及部分智能合约CVE漏洞集上进行测试，实验结果表明，提出的方法可以有效检测出新的代币买卖后门漏洞以及owner权限转移漏洞.关键词智能合约；漏洞检测；符号执行；程序分析；区块链安全

关键词: 智能合约, 漏洞检测, 符号执行, 程序分析, 区块链安全