董云卫， 张涵博, 李勇军

西北工业大学计算机学院, 西安 71012

0 引 言

软件定义的概念和技术的发展和应用，软件安全问题已经成为嵌入式系统乃至装备产品研制和运行维护的核心关注点.装备嵌入式系统的软件规模性和复杂性都在急剧增加，软件的安全性和可靠性问题日益突出.研究保障系统安全可信性的软件代码加固安全，提高系统运行管理的可信性显得尤为重要.

目前针对于保障软件代码的安全性，国内外众多研究者主要利用安全漏洞检测技术和安全漏洞修复手段来提高软件的安全性.安全漏洞检测技术可以分为静态检测技术和动态检测技术，其主要通过软件测试、代码分析、符号执行和模型检验等技术途径来实现[1].为此，涌现出了多个优秀工具，如SAGE[2]是基于二进制代码的重量级模糊测试工具，PEX[3]是微软将轻量级动态符号执行方法与单元测试领域结合起来设计出的工具，YOGI[4]是微软基于抽象解释和反例制导的求精方法的模型检验工具，KLEE[5]是基于轻量级动态符号执行的自动化白盒模糊测试方法工具.

WEILE等[6]实现的静态分析检测框架Marple，该工具通过对控制流图中的路径进行分析，把路径分为安全、漏洞、警告、不可达和未知这五类，通过自动检测分析将路径类型信息、漏洞根源信息与位置信息形成信息报告给用户.航空软件系统往往代码行数巨大，且对代码的质量要求极高，美国NASA的BRAT等[7]针对于航空航天软件系统利……