开源代码指源代码数据是公开的,所有人都可以获得的代码,方便人们在此基础上进行二次开发。开源代码出现问题就有可能导致使用它的软件都存在安全隐患。随着计算机软件技术的快速发展,软件系统尤其是代码的安全性、可靠性问题逐渐成为关注焦点。代码都是依据设计方案进行编写的,它最重要的性质就是与设计方案保持一致。因此,代码的安全性除了与自身的编写有关外,还与设计方案的安全性以及它是否保证与方案之间的一致性息息相关。当前针对软件的安全性检验,常见的方法主要包括安全测试和模型检测。代码与方案之间的一致性便是依靠测试来进行验证的。然而,传统的测试方法难以实现全面的分析,无法覆盖到全部的情况。模型检测作为形式化方法的一种,能帮助发现其它方法不容易发现的系统描述的不一致、不明确或不完整,在协议和软硬件系统的分析中有着广泛的应用。目前模型检测在设计层面和代码本身的验证上都多有运用。在设计层面分析上有众多可供使用且各有针对性的工具,而对代码本身也已有较为成熟的静态代码分析工具。因此本文针对如何进行工具的选择并方便有效地使用工具验证设计方案的安全性,以及如何进一步将形式化方法应用到代码安全分析上,分析代码和设计方案之间的一致性展开研究。论文主要工作如下:（1）面向开源代码,尤其是通信方面的开源软件,设计并实现了一整套对代码进行安全性分析的方案,通过对设计层面进行检验保证其安全性并验证代码与方案之间一致性,分析代码是否安全。（2）针对当前形式化方法众多难以选择的问题,对常用形式化方法及工具的特点进行总结,分析其优缺点及适用方面,为根据不同情况更有针对性地选择合适的工具打下基础。并且总结了用热门工具Tamarin进行建模的通用化方法,对常见安全目标属性进行了总结和分析,方便更加高效地利用Tamarin工具对方案的安全性进行分析。（3）在一致性测试的基础上,基于模型检测进行路径搜索的思想,对一致性进行了更加完备的定义。通过抽象出代码中各个功能模块的调用以及代码中各个函数之间的调用关系,建立合适的形式化模型,实现了能够更全面地覆盖到可能出现的路径,检测代码与方案之间一致性的方案。（4）通过实验,验证了所提出方案的可行性。该方案可以完成对软件设计层面及代码一致性的分析,并且可以找出一致性测试可能无法涉及到的路径进行更完备的检验。