《表4 整型溢出判断方案：基于符号执行的智能合约漏洞检测方案》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《基于符号执行的智能合约漏洞检测方案》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

整型溢出会导致算术运算后的结果（result）变成一个极小值甚至归0，对执行结果检测很容易判断是否溢出，图3给出了整型溢出检测的基本流程。例如判断uint a+uint b=result是否溢出，随机构建一个极大的值作为程序的输入，对执行结果添加约束UGT（a，result）OR UGT(b，result），即result比a或b小，则可能发生了整型溢出。利用a和b的符号值和路径信息进行符号运算，当遇到ADD指令时，对执行结果添加约束UGE(result，2^256），即result大于等于2256，通过约束求解器求解result，当result有解时发生溢出。表4给出整型溢出判断方案，当相应约束有解时，报告溢出漏洞。