文档介绍：信息安全测评技术
分析验证与形式化分析验证
分析验证基于一定的分析手段或经验，验证信息产品或信息系统中不存在相应的安全隐患。控制流、信息流、边界值等是重点分析的对象，普通安全隐患可凭经验发现，复杂的需形式化的安全验证。
形式的测试用数据为测试序列。

通过输入、下载不同带宽、速率的数据或建立不同数量的通信连接，得到被测产品或系统的数据处理能力指标值及他们之间可能的相互影响情况。如得到最大带宽、吞吐量、最大处理速率等。

利用网络攻击或密码分析手段，检测网络安全设备或密码模块的安全性质，如网络扫描技术，用于测试防火墙、IDS与服务器安全特性。
测试技术
测试技术

通过测试了解信息安全产品或系统出现故障的可能性、故障环境及故障类型，故障测试结果课反映被测对象的运行稳健性，如错误数据输入。

对于信息安全产品、系统或其模块、子系统，检测他们在接口、协议等方面与其他配套产品、系统或模块、子系统的互操作情况，确定他们是否都符合相关的接口、协议设计与规范。
可信计算平台测评
可信平台模块(Trusted Platform Module，TPM)是可信计算平台的核心和基础，可信平台模块的功能测试和验证是保证可信平台模块的实现正确性以及规范一致性的重要手段，以TPM密码子系统为例给出了该子系统的形式化规格说明，并且基于该规格说明，给出了扩展有限状态机模型，最后，将该有限状态机模型应用于测试用例的自动生成，并通过实验验证了形式化测试的有效性。
TPM密码子系统
在TPM ，TPM提供了基本的密码操作，主要的密码操作有RSA的密钥生成，加密、解密操作，RSA的签名操作，同时TPM提供了封装存储的功能．其中主要有三类密钥：加密密钥、封装密钥和签名密钥。不同的密钥能执行不同的操作，如封装密钥能执行Seal和UnSeal的操作。
EFSM模型
扩展的有限状态机(Extended Finite State Machine，EFSM)。M定义为一个六元组<S，So，I，O，D，T，V>，其中S是一个非空的状态集合，So是初始状态，I是一个非空的输入消息集合，，O是一个非空的输出消息集合一，V是变量集合，对于任意的t∈T，t是一个六元组(s，x，P，op，Y，s’)，其中S，s’∈S分别为初始状态和终止状态。x∈I是状迁移t的输入；y∈O是状态迁移t的输出；P是状
态迁移t的前置条件，可能为空；op是状态迂移中的操作，其中由一系列的输出语句和变量赋值语句组成。
基于EFSM的形式化测试
本节的测试用例的生成分为两步：第1步通过算法自动生成抽象测试用例，抽象测试用例是不能执行的；第2步将抽象测试用例具体化为可执行的测试用例，在这一步中需要填入具体的测试数据．采用两阶段的方法更有利于测试方案的实施，更有利于模块化的部署．由于TPM命令的复杂性，第2步测试数据的生成目前还不能完全进行自动化的生成，需要人工的参与。在测试一些模块时，不需要用户显式地要求TPM产生授权会话，这是由用例工具自动生成的，也是一个基本的假设条件；通过EFSM模型生成的测试用例只能对TPM的抽象功能(主要是TPM规范的第一部分)进行符合性测试，并不能对具体的实现接口进行参数化的测试。
子系统测试先后顺序
不同的子系统的测试是有先后顺序的，如密码子系统依赖于授权协议管理子系统，只有先对授权协议管理子系统进行测试之后才能对密码子系统进行测试。
覆盖度
覆盖度是衡量测试用例完备性的一个重要手段．在一致性测试中，状态覆盖度和迁移覆盖度是最常见的覆盖标准． (完全状态覆盖，all state coverage)，测试集完全状态覆盖状态变量X指的是对于x的任意取值，至少有一个测试用例覆盖到该值．测试集完全状态覆盖EFSM模型，指的是对于任意的状态变量Y，测试集都完全状态覆盖变量Y．
EFSM的可达性分析树，是一颗表达在所有的可能性输入的情况下，从初始节点出发扩展有限状态机的行为．对于每一个输入序列，该树包含一条从根出发的路径．可达性树是一个有向图，因此可以通过图论中的DFS或BFS方法对图进行遍历．
生成可达性分析树算法
，从EFSM的指定初始节点出发对EFSM进行深度优先遍历，生成可达性分析树．
2．在深度优先遍历过稷中将遍历到的节点放入已遍历状态集合Stravel中．
3．当遍历深度>l时，停止可达性分析树的生成．
4．先在可达分析树中找到所有的可行路径，为每条可信路径指定具体的数据，主要指定的数据格式为(命令号，随机产生的命令数据，预期值)。每一条路径对应一个完整的测试用例。
密码予系统的可达性树
节点标示EFSM中状态，路