近年来,针对政府、企业计算机信息系统的漏洞攻击、黑客恶意代码传播以及拒绝服务攻击活动频有发生,对国家安全和社会稳定造成了极大危害。为保证系统业务安全运行及其处理信息不会泄露或被篡改,我国提出了对计算机信息系统实现安全等级保护的要求,并将等级保护作为国家信息安全保障的一项基本制度、基本策略和基本方法。近十年,我国在信息安全等级保护方面出台了一系列相关的政策法规及其技术标准。本文以信息系统等级保护安全功能符合性检验为背景,研究了国内外已有的信息安全评估、安全测评方法及技术,结合我国信息安全等级保护要求,基于证据理论构建了一个多层安全功能符合性检验框架,并给出一种确定检验要素集合的方法。此外,本文将模型检测技术应用于信息系统的安全功能符合性检验中,给出安全策略的符合性、有效性和一致性验证方法。本文主要工作和研究成果有：(1)研究了与检验相关的安全评估、测试理论和协议一致性测试方法等,设计了安全功能符合性检验一般模型。由信息系统安全功能符合性检验的目标,参考软件测试的理论基础,提出了检验方法正确性的形式化表示方法。具体为：在给出衡量检验准则有效性和可靠性定义及其形式化描述的基础上,提出了理想检验集的概念；(2)研究了国内外信息安全相关标准,并深入分析了我国信息系统安全等级保护相关的几个主要标准,综合这些标准要求,得出不同等级的信息系统安全功能需求。针对这些安全功能要求,建立了基于证据理论的安全功能符合性检验三层证据框架,基于此框架提出一种信息系统安全功能检验集的确定方法；(3)将模型检测应用于信息系统安全策略的符合性检验,主要完成了安全策略与安全需求的符合性验证以及安全策略对其实施系统的有效性验证。在符合性验证中将系统的安全策略转化为策略规则约束下的系统操作,并采用有限状态机对其进行建模,安全需求则采用线性时态逻辑公式描述,基于模型检测完成了系统安全策略与安全需求的符合性检验。而在有效性验证中,安全策略则采用线性时态逻辑公式描述,对系统的结构及性能分别进行建模,最后应用模型检测方法验证安全策略的有效性；(4)防火墙是应用广泛的网络访问控制技术之一,目前对其安全分析的研究主要集中在安全规则分析及其冲突检测两个方面,而针对安全规则与访问策略的一致性验证研究得较少。本文提出了基于模型检测的防火墙安全分析验证方法,在安全规则形式化建模及访问策略时态逻辑描述基础上,使用模型检验工具SPIN完成了防火墙安全规则与系统安全访问策略的一致性验证；(5)设计了一个信息系统安全功能符合性检验原型系统。检验原型系统由检验管理平台和检验工具集组成,检验管理平台完成工具管理、任务管理、问卷管理、知识库管理等,管理平台提供统一的接口规范管理各检验工具。各检验工具的检验结果提供给检验管理平台后首先被解析成统一的数据格式,然后对这些数据进行综合分析而得出信息系统安全功能等级保护符合性结果。