公开(公告)号：CN111124723A

公开(公告)日：2020-05-08

申请号：CN201911067304.9

申请日：2019-11-04

Applicant: 北京轩宇信息技术有限公司

Inventor： 高猛 ,  滕俊元 ,  郑小萌 ,  郭华 ,  孙民 ,  高栋栋 ,  侯清锋 ,  江云松 ,  冯涛 ,  周益

IPC: G06F11/07

Abstract: 本发明公开了一种基于干扰变量的中断驱动型程序整数溢出模型检测方法，该方法包括：对待处理程序进行解析，得到干扰变量集合；根据干扰变量集合中的干扰变量信息，对中断函数进行抽象处理，得到中断函数摘要；在主程序中插入中断函数摘要，得到顺序化后的程序；获得顺序化程序的静态单赋值形式SSA，并进行程序模型状态空间约简处理，得到约简后的程序；使用有界模型检测工具CBMC，对约简后的程序进行整数溢出检测。本发明在保证整数溢出问题检出率的前提下，不仅能够提高分析效率，还使得已有的模型检测技术能够适用于中断驱动型程序整数溢出检测。

公开(公告)号：CN111124723B

公开(公告)日：2023-04-14

申请号：CN201911067304.9

申请日：2019-11-04

Applicant: 北京轩宇信息技术有限公司

Inventor： 高猛 ,  滕俊元 ,  郑小萌 ,  郭华 ,  孙民 ,  高栋栋 ,  侯清锋 ,  江云松 ,  冯涛 ,  周益

IPC: G06F11/07

Abstract: 本发明公开了一种基于干扰变量的中断驱动型程序整数溢出模型检测方法，该方法包括：对待处理程序进行解析，得到干扰变量集合；根据干扰变量集合中的干扰变量信息，对中断函数进行抽象处理，得到中断函数摘要；在主程序中插入中断函数摘要，得到顺序化后的程序；获得顺序化程序的静态单赋值形式SSA，并进行程序模型状态空间约简处理，得到约简后的程序；使用有界模型检测工具CBMC，对约简后的程序进行整数溢出检测。本发明在保证整数溢出问题检出率的前提下，不仅能够提高分析效率，还使得已有的模型检测技术能够适用于中断驱动型程序整数溢出检测。