<正>随着移动互联网终端的普及应用,移动互联网业务得到了前所未有的快速发展,相关的移动业务应用软件也被越来越多的个人或企业用于处理各种私密信息、敏感信息和高价值信息,例如个人隐私、商务谈判信息等,这使得移动业务应用软件成为企图获取这些信息攻击者的攻击目标。软件代码编写阶段引入的安全漏洞是最常见的安全漏洞,如何设计一种有效的代码安全测试方法,以检测存在于源代码中的潜在威胁是非常必要且迫切的。软件代码的漏洞主要通过静态方法和动态方法进行检测。虽然动态方法对代码的规模没有限制,可以对大型程序进行检测,但不足之处是检测的效果严重依赖输入方法,只有当特定的输入使代码执行到危险点时,漏洞才会被发现,所以这种方法漏报率较高。基于约束分析和模型检验的代码安全漏洞检测方法提出一种约束分析的模型检测方法对缓冲区溢出漏