摘要：软件漏洞是引发信息安全问题的重要根源.内存泄露作为一种常见的软件漏洞,会加快系统内存的不良消耗,造成系统崩溃,一旦被利用,可形成拒绝服务攻击DoS,成为程序稳定性的致命威胁.遗憾的是在程序运行时,内存泄漏难以定位.如果程序包含多线程,内存泄漏分析需进行线程隔离,实现难度大.为提高C程序内存泄露漏洞分析的效率,本文首先划分程序的可行路径,并构建程序的状态变迁图,图中任意一个分支即对应一条可行路径.其次,针对存在内存分配的分支,均对应构建内存是否释放的判断条件,作为安全属性.再次,基于半代数系统将程序执行看作为变量间的代数交互,以此构建程序及安全属性的形式化建模规则,模型称为半代数系统.与此同时,构建半代数系统至多项式系统间转换规则,将程序进一步形式化建模为多项式系统.最终,基于约束求解的思想,将程序对应的多项式系统转化为单个多项式等式作为目标函数,将安全属性对应的半代数系统作为约束条件,两者相结合形成Max函数.通过填充函数法求解此函数,当目标函数不等于零时,则程序存在内存泄露.实验证明本文方法在C程序内存泄露漏洞分析过程中具备可行性和有效性。
