一种基于模型检测的二进制程序脆弱性分析框架

针对二进制程序脆弱性分析的实际需求，提出了一种基于模型检测的二进制程序脆弱性分析框架。首先定义了二进制程序的抽象模型，描述了基于有限状态自动机的软件脆弱性形式化表示和基于事件系统的软件安全属性表示方法。在此基础上，提出了基于模型检测的脆弱性分析过程和算法。根据该分析框架，设计并实现了二进制程序脆弱性分析工具原型。通过脆弱性分析实验，详细说明了该框架的工作原理，验证了该分析方法的有效性。