缓冲区溢出问题是软件系统的主要的安全隐患,通过向内存中写入超出缓冲区的数据,覆盖一些重要内存空间,从而达到篡改数据、控制系统、导致系统无法工作等目的。由于该问题涉及具体程序中复杂的控制流、数据流、指针分析、边界检测、权限控制等情况,尽管现有大量的静态和动态检测方法,但依然无法确保安全,每年仍有大量的漏洞随软件的发布而流入市场,其攻击数量逐年上升,并造成了巨大的经济损失。本文对较为常见的数组缓冲区溢出问题进行了研究,利用现有较新的程序分析理论和方法,进一步改进和设计更加高效和准确的数组缓冲区溢出检测方法。本文提出了基于符号运算的静态结构化分析框架,对数组索引以及指针边界进行分析和检测。并着重分析数组索引变量的数学依赖关系,通过符号运算的递归方程以及约束方程求解,生成变量边界;进而利用安全读写规则,为该函数或过程建立安全约束关系;利用该约束关系式以及实际输入的参数或者数据,可以判断溢出的可能性。该方案具有下面一些优点和创新点:(1)对该问题进行简化处理,缩小分析规模,提高分析的速度。(2)数组指针的状态分析与变量边界的数值分析相结合。(3)使用符号运算方式对变量进行计算,提高可分析问题的复杂度。(4)将循环结构作为基本分析单元进行递归分析,提出了新的静态分析框架模型。(5)可以对多循环、多分支、具有复杂依赖关系的变量进行分析和边界检测,扩展了可分析问题的范围。最后,通过实现的原型机对该方案进行验证,实验结果表明该方案具有较好的检测能力和分析效率。