近年来,内存泄漏、缓冲区溢出等内存漏洞频发,尤其是对于C和C++之类的内存不安全语言来说,更容易受到内存脆弱性的影响,从而导致难以预料的系统崩溃。这些脆弱性一旦被恶意攻击者利用,就会产生严重的后果。此外,由于程序员的疏忽导致的代码低效行为更是屡见不鲜,这些行为虽然不会带来致命的后果,但是会严重影响程序的执行效率。更有甚者会利用系统本身的特性进行恶意攻击,从而获取内存中的敏感信息,如近几年爆发的幽灵、熔断等漏洞,也对内存安全带来极大的威胁。因此,内存安全漏洞的检测就显得尤为重要。目前广泛使用的脆弱性检测方法包括动态检测和静态检测,这两种方式都各有优势并且受众多科研工作者的青睐,也因此产生了很多科研成果,但也不可避免的存在一定的局限性,或是检测范围仅局限于堆,或是检测效率低下,或是需要对源代码进行分析。而本文通过将动态检测和静态检测相结合,提出一种基于内存访问轨迹的程序脆弱性检测方法,其主要内容及创新点如下:(1)将有限状态机模型应用于内存访问中,根据违反有限状态机模型中状态转化的操作定义了几种相关的内存脆弱性,并将其形式化的描述为求解器可以理解的约束表达式。(2)通过二进制插桩动态跟踪记录可执行程序的内存访问轨迹,包括函数记录、内存分配及释放记录、内存读写记录以及全局变量等信息。从数据流和控制流两个角度对其进行了跟踪,由此分析可执行程序的内存操作执行顺序以及内存访问模式。(3)根据内存操作的状态转化顺序以及漏洞模型,计算可能触发漏洞的约束条件,调用Z3约束求解器判断轨迹是否触发漏洞,同时确定脆弱性的地址及类型,并将检测结果以可视化的形式展现出来,可以清晰直观的描述内存访问的轨迹以及漏洞所在位置。此外,我们通过一些实验对本文方法的有效性和性能进行了测试,结果表明本文的方法可以在保证效率的同时有效检测出相关的脆弱性。