安全策略及设计规范的半形式化方法
邓辉 , 石竑松 , 张宝峰 , 杨永生 , 刘晖     
中国信息安全测评中心, 北京 100085
摘要:对安全功能要求的错误理解会在IT产品中引入内在的安全缺陷。半形式化方法可提高描述安全功能要求的准确性,增强设计的合理性,从而有助于降低引入安全缺陷的风险。因此,该文将重点研究产品安全策略及设计规范的半形式化描述及验证方法。首先,论述了通过分析安全功能接口,从安全功能要求中提取安全策略,以及从模块设计中提取设计规范的一般方法,给出了降低耦合性的子系统和模块划分规则;其次,通过选择和改进现有的半形式化工具,给出了描述安全策略以及设计规范的半形式化方法;最后,以IC卡芯片产品的测评为例,通过对部分安全策略以及设计规范进行半形式化处理,论证了产品所采取的安全策略可使安全功能要求得以充分满足,且相应的设计规范也是合理的。结果表明:该文所建立的半形式化方法在一定程度上适于所有信息技术产品的安全测评。
关键词安全策略    设计规范    半形式化    
Semi-formal method for security policies and design specifications
DENG Hui, SHI Hongsong, ZHANG Baofeng, YANG Yongsheng, LIU Hui     
China Information Technology Security Evaluation Center, Beijing 100085, China
Abstract: Inadequacies in IT products can result from misunderstandings of the security requirements. Semi-formal methods can accurately describe the security requirements and implement reasonable requirements that avoid causing security flaws. Thus, semi-formal descriptions and verification methods are used in this study for security policies and design specifications represented by collections of the security requirements and module designs of security functionality interfaces. The system uses a loosely coupled partitioning method for the subsystem and module. Semi-formal methods are given to describe the security policy and design specification derived from existing semi-formal tools. The approach is applied to an IC card chip product to show that its security policies are adequate and the security design provides reasonable security. This approach can be used to evaluate all kinds of IT products.
Key words: security policy     design specification     semi-formal    

信息技术安全产品在进入应用市场前,有必要对其进行安全测评[1],以在不同程度上提前规避安全风险。信息安全测评机构常依据相关标准开展测评活动。目前,国际广泛采用信息安全通用评估准则ISO/IEC15408 CC标准(Common Criteria for Information Technology Security Evaluation)[2]以及与之等同的中国标准GB/T 18336[3],都将安全测评(隐含地)划分为“评估”和“测试”2部分。其中,“评估”贯穿测评的始终,其目的是验证为满足安全功能需求所采取的安全策略的充分性,以及这些策略在设计和开发这些细化阶段的一致性;“测试”是“评估”的支撑,“测试”的目的是验证产品在实现安全功能要求方面的正确性,以及抵抗攻击的能力。通过“测试”和“评估”共同发现产品安全缺陷,帮助产品开发者改进并提升产品的安全性[1]

对安全策略与设计规范的验证是“评估”活动的一项重要内容。通过分析对两者的描述,可以确认开发者对安全功能要求进行了正确理解及正确设计,所采用的安全策略是充分的并且设计规范是合理的。进而得知,产品的安全需求得到了满足。但是,安全策略与设计规范的描述方法对评估活动的效率和质量会产生很大影响。例如,在GB/T 18336中,不同的评估保障级(EAL1~EAL7) 对测评文档的详细程度和形式化程度要求不同,使得不同级别中的安全策略与设计规范的描述及验证方法存在着不同。在EAL1~EAL4低级别测评中,产品的测评文档均为非形式化形式,一致性验证基于评估人员人工比对文档完成,耗时耗力。同时,非形式化的二义性问题可能影响评估人员对安全策略和设计规范的正确理解,进而影响描述及验证结果。在EAL5及以上级别测评中,GB/T 18336标准对文档的形式化要求提高,如要求产品设计规范文档为(半)形式化形式。但是,该标准对安全功能要求(security function requirement, SFR)的描述仍停留在非形式化。这两方面的不同形式化程度将影响二者一致性验证结果。

目前国际上均已开展信息技术产品的高级别测评[4],特别是芯片类产品主要以高级别测评为主[5],因此针对产品安全策略及设计规范的分析和验证也以半形式化和形式化方法为主[6],而国内目前还缺少高级别测评的技术储备和应用案例。为此,本文将着重研究安全策略及设计规范半形式化描述及验证方法。基于统一的半形式化描述框架,以消除EAL5级非形式化安全功能要求与半形式化设计规范间的不一致性,实现对安全功能要求的正确理解,并提高安全策略和设计规范间的一致性验证能力。

1 安全策略的提取及设计规范的描述框架

具有安全功能的信息技术产品开发常采用安全需求分析、安全策略提取、安全功能设计到安全功能实现的技术路线。其中,安全策略描述了安全功能的规则集,可从安全功能要求的集合中提取。设计规范描述安全功能设计的具体信息,随着测评级别的提高带来保障要求的增加,设计规范提供设计信息的详细程度也随之增加。同时,随着安全功能规模和复杂性的增加,设计需要分层。EAL5级测评中,产品设计需要基于子系统和模块2个层次从高到低进行分解,以逐步细化对安全功能设计的描述。

GB/T 18336给出安全功能接口的定义为所有处于产品外部(或处于产品内部,但在安全功能外部),可给安全功能提供数据、从其获得数据以及调用其服务的方法或途径,如图 1箭头所示。

图 1 安全功能接口

图 1可看出,安全功能接口是外界和产品安全功能交互的入口,因此也是攻击入口。产品的安全策略可通过安全功能接口的安全策略来表达,产品的设计规范可通过安全功能接口的设计规范,以及通过接口连接起来的安全功能模块和子系统的设计规范来表达。因此,可围绕安全功能接口完成安全策略及设计规范的特征提取,并建立两者之间的联系。

对于信息技术产品来说,安全功能接口类型可分为逻辑接口(例如函数、指令等)和物理接口(例如芯片表面、芯片引脚等)2类。

1.1 安全策略的提取

安全策略描述了安全功能的规则集,因此策略提取的正确性取决于对安全功能要求的正确理解。GB/T 18336预定义安全审计、通信、密码支持等11类安全功能要求,以供实际文档描述过程选用,并可针对产品特殊安全需求对安全功能要求进行扩展定义。以芯片产品为例,国标GB/T 22186[7]对具有中央处理器的IC卡芯片在达到EAL4+/5+/6+级时所需满足的安全功能要求进行详细定义,可划分为密钥支持、用户数据保护、标识和鉴别、安全管理等7类,具体描述如表 1所示。

表 1 具有中央处理器的IC卡芯片安全功能要求
安全功能类 安全功能要求组件
密码支持 密钥生成
密码运算
用户数
据保护
子集访问控制
基于安全属性的访问控制
子集信息流控制
基本内部传送保护
存储数据完整性监视
存储数据完整性监视和行动
标识与鉴别 鉴别的时机
鉴别失败处理
安全管理 受限能力
受限可用性
安全属性的管理
静态属性初始化
TSF(TOE security functionality)数据的管理
管理功能规范
安全角色
安全功能保护 失效即保持安全状态
内部TSF数据传送的基本保护
物理攻击抵抗
子集TSF测试
资源利用 受限容错

以安全管理类中的安全功能要求(受限能力和受限可用性)为例来说明提取安全策略的步骤。

步骤1 明确安全功能要求的具体含义。

1) 受限能力:IC卡芯片安全功能应采取某种能力受限的设计和实现方法。

2) 受限可用性:IC卡芯片安全功能应采取某种可用性受限的设计和实现方法。

步骤2 明确安全功能要求具体由产品安全功能的哪一部分满足。对于IC卡芯片来说,此两项安全功能要求由实现模式控制的功能来满足。

步骤3 明确安全功能要求分别对应产品安全功能某部分中哪几项安全策略,每项安全策略将对应哪几个安全功能接口。通过分析,受限能力和受限可用性分别对应以下安全策略。

1) 为满足受限能力:通过安全功能接口控制安全功能在用户环境下可用,但使其能力受限。

2) 为满足受限可用性:在用户环境下禁止和删除安全功能接口,使功能不可用。

依照此思路可分别提取表 1中其他安全功能要求在具体产品中所采取的安全策略。

1.2 设计规范的描述框架

设计规范用于描述为满足安全功能要求,产品所采用的安全设计方法。基于对GB/T 18336的理解,设计规范可按照测评级别的高低或产品复杂度,分别依据安全功能子系统到安全功能接口、安全功能模块到安全功能接口、安全功能子系统到安全功能模块再到安全功能接口3种途径来完成特征提取。对于简单产品,省略子系统单独提供模块到接口的设计表示框架是合适的。但是,对于复杂产品,没有子系统级别的设计描述,即便是对模块设计进行了大量描述也会给评估者带来很大困难。

为使本文所创建的方法适合复杂产品的EAL5级测评要求,本节将采用安全功能子系统到安全功能模块再到安全功能接口的设计规范提取框架,提取所有安全功能相关设计内容,具体如下。

1) 提取产品安全功能子系统和安全功能模块。提取过程中,分析产品是否基于低耦合原则从安全角度逻辑划分安全功能子系统和安全功能模块,划分规则如图 2所示。

图 2 产品安全功能子系统及模块划分规则

图 2表示合理的安全设计应首先依据安全功能子系统和安全功能模块的两层结构对安全功能进行划分,其中对于同时存在于2个安全功能子系统的安全功能模块C,为降低设计耦合,应将此模块独立设计成为一个子系统C。

2) 从安全功能模块层完整提取安全功能接口。

3) 提取安全功能子系统、模块、接口之间的映射关系,具体映射关系如图 3所示。

图 3 子系统、模块和接口的映射关系

需注意的是,在安全设计过程中对于图 3中不存在安全功能接口的模块D以及该模块所对应的子系统C需确认设计它们的合理性。

4) 提取安全功能接口相关特征,包括接口的参数、参数描述、使用方式、行为及错误消息。其中,通过提取参数及参数描述,可明确安全功能接口的具体输入和输出,以及如何通过对参数的不同赋值获取安全功能接口不同的使用方式,进而控制安全功能接口的行为,实现外界与安全功能的交互;通过提取接口使用方式,可明确外界如何触发安全功能接口的动作以及如何获得安全功能接口的响应;通过提取接口行为,可明确外界由使用方式触发安全功能接口的动作和响应;通过提取错误消息,可明确由外界调用(和非调用)安全功能接口可能产生的所有错误信息,包括直接错误(由调用安全功能接口产生的错误)、间接错误(非调用安全功能接口产生的错误,但是是在接口调用过程中发生的系统错误)以及无关错误(非接口调用过程中发生的错误)。

5) 基于安全功能接口提取模块间与安全功能相关的交互关系,完成子系统间与安全功能相关的交互关系的提取。

6) 提取安全功能子系统之间的与安全功能相关的交互关系,可通过安全功能模块间交互关系得到刻画。

以上提取内容中所涉及的产品安全功能子系统、安全功能模块交互策略、以及产品安全功能接口控制策略,均是产品的安全设计策略。

2 半形式化工具的建立

安全策略及设计规范半形式化包括半形式化描述及半形式化验证两项内容,其目的是解决非形式化描述的二义性问题,以便正确地理解安全功能要求及安全设计,使得可在统一描述框架下实现对二者的一致性判断,并由此得出安全设计是否是安全功能要求的一个完整且正确的实例化。半形式化通过采用具有确定语义和语法的语言表达规范,可解决非形式化二义性问题。通过研究,对于芯片安全测评,可选择ASN.1[8]和UML[9]工具对安全策略及设计规范进行半形式化处理。

2.1 ASN.1

ASN.1是一种ISO/ITU-T标准,可描述各种类型的数据,可应用于描述产品设计规范中的部分提取内容:安全功能接口参数及参数描述。经提取ASN.1中可用于刻画安全功能接口参数及参数描述的简单类型和结构类型分别如表 23所示。

表 2 ASN.1常用简单类型
简单类型 含义
INTEGER 整数型
BOOLEAN 布尔型
ENUMERATED 枚举型
BIT STRING 比特流
OCTET STRING 字节流
EXTERNAL 自定义类型

表 3 ASN.1常用结构类型
结构类型 含义
SEQUENCE 多个类型的有序集合
SEQUENCE OF 某个类型的有序集合
SET 多个类型的无序集合
SET OF 某个类型的无序集合
ANY 任意类型

除定义数据类型外,需结合操作符号才可完成数据特征完整定义。ASN.1可用于刻画安全功能接口的常用操作符号如表 4所示。

表 4 ASN.1常用符号
符号 含义
:: = 对象赋值
{ } 对象相关项
[] 对象可选项
| 对象在可选项中任选其一
() 对象子类型
.. 对象子类型的取值范围
-- 对象注释

2.2 UML

UML是一种可视化建模语言,为面向对象软件设计提供统一标准的描述模型。在安全策略及设计规范半形式化过程中,本文主要对活动图、顺序图和构件图的图形符号进行混合和部分扩展,并依据半形式化对象特征对部分符号涵义进行重定义。

2.2.1 活动图

活动图用于描述一个过程或者操作的工作步骤。可用的符号表示分别为起点(实心圆)、终点(公牛眼形)、活动(圆角矩形)、活动转移(箭头)、判定(菱形)、并发路径(黑色粗实线)。但是,活动图仅能呈现单个对象的多个活动的执行流程,当安全策略及设计规范涉及多个对象的多个活动,且活动执行具有先后顺序时,则需要依赖顺序图的刻画框架实现策略及设计描述。

2.2.2 顺序图

顺序图旨在描述对对象的先后处理顺序。可用的符号表示分别为对象(矩形框)、生命线(虚线)、激活(窄矩形条)、活动转移(箭头)。为了描述安全功能接口的设计规范信息,在活动图和顺序图混合的基础上,引入新安全功能接口符号(空心圆)、并对和空心圆有关系的符号涵义进行了重定义,具体如表 5所示。

表 5 安全功能接口关系符号
符号 含义
安全功能接口
可使用此安全功能接口
可通过一种使用方式触发
一个安全功能动作
特定条件下可
使用此安全功能接口
此安全功能接口不可见
可通过一种使用方式触发
一个接口下的直接错误
可通过一种使用方式触发
一个接口下的间接错误
可通过一种使用方式触发
一个接口下的无关错误

2.3 构件图

构件图表示系统多个物理单元的组织方式。可用的符号表示为构件(矩形框)、接口(小圆圈)、关联(无端点直线)、依赖(虚线箭头)、实现(虚线空心三角箭头)、继承(实线空心三角箭头)、聚集(实线空心菱形箭头)。构件图可用于描述子系统、模块之间通过接口产生的交互关系。为区别安全功能接口和内部接口,将构件图中已有空心小圆圈代表安全功能接口,新增实心小圆圈代表内部接口。同时,将已有关联关系表示子系统和模块间简单的通信关系,当通信过程有和安全相关的信息传递时,将关联关系加上端点箭头。如果是单向传递,则为单向箭头(箭头指向代表消息传递方向);如果是双向传递,则为双向箭头,同时需将传递的具体消息标注在箭头上。

3 安全策略半形式化描述

在节2描述安全策略的提取,以及新建的半形式化工具的基础上,本节将以IC卡芯片产品模式控制的“有限的能力”和“有限的可用性”为例,论述如何以半形式化方法描述其中蕴含的安全策略。

1) 为满足受限能力:通过安全功能接口控制安全功能在用户环境下可用,但使其能力受限;依据已定义的半形式化语法,此策略可半形式为图 4所示。

图 4 有限的能力

图 4将安全功能接口命名为接口A,以区分“为满足受限可用性”中的安全功能接口。图 4将“为满足受限能力”解读为测试模式通过安全功能接口A与安全功能交互,而用户模式只能在特定条件下使用此接口与安全功能交互,使用能力受限。

2) 为满足受限可用性:在用户环境下禁止和删除安全功能接口,使功能不可用;依据节3中定义的半形式化语法,此策略可半形式化为图 5所示。

图 5 有限的可用性

图 5将“为满足受限可用性”解读为测试模式可使用的安全功能接口B在进入用户模式之前被禁止和删除,使得用户模式无法看见该接口,因此无法使用安全功能。通过对1) 和2) 的半形式化解读可得到IC卡芯片测试模式可利用安全功能接口与功能交互,当测试模式完成功能操作进入用户模式后,用户模式只能在特定条件下操作,或无法操作安全功能接口,因此无法和安全功能交互。

4 设计规范半形式化描述

设计规范指为满足安全功能要求中的安全策略,产品具体采用何种安全设计,即在节2.2中提到的需要提取的7项内容。下面仍然以“有限的能力”和“有限的可用性”为例对这7项内容分别提取并进行半形式化描述。“有限的能力”和“有限的可用性”对应模式控制。为突出描述本文方法,假设芯片安全功能仅包含这部分,经提取描述如下。

1) 子系统、模块、安全功能接口映射关系半形式化关系如图 6所示。

图 6 构件图

图 6对于子系统以及模块间映射关系描述基于构件图完成,基于子系统实现产品结构分解,基于模块实现产品安全功能结构分解。图 6指出模式控制功能依赖模式控制子系统、Flash子系统、寄存器子系统三者交互完成。其中,模式控制子系统包含接口管理模块、模式转换控制模块;Flash子系统仅包含Flash模块;寄存器子系统仅包含寄存器模块。

2) 安全功能接口半形式化。

在模式控制子系统、Flash子系统、寄存器子系统三者交互实现模式控制功能过程中,依赖的安全功能接口包括物理(硬件)接口PAD、逻辑(命令)接口O和P、逻辑(函数)接口M(X)和N(Y)。4个接口的作用及具体信息描述如下。

首先,基于ASN.1描述接口的参数及参数描述,分别以上述接口中的某一个为例描述如下。

a) 物理(硬件)接口PAD。

PAD BIT STRING [0|1], ——表明芯片外部引脚PAD1、PAD0取值状态的二进制字符串, 0表示给外部引脚置低电平, 1表示给外部引脚置高电平。

b) 逻辑(命令)接口O。

O :: = SEQUENCE OF

{

CLA OCTET STRING (SIZE(1B), VALUE(1)), ——1个1字节的十六进制数,取值为1

INS1 OCTET STRING (SIZE(1B), VALUE(1)), ——1个用于表明写下载标志位命令的1字节的十六进制数,取值为1

P1 OCTET STRING (SIZE(1B), VALUE(COS (0)), ——1个1字节的十六进制数,取值为0,表明COS用户ID

P2 OCTET STRING (SIZE(1B)), ——1个1字节的十六进制数

P3 OCTET STRING (SIZE(1B), VALUE(0))——1个1字节的十六进制数,取值为0

}

c) 逻辑(函数)接口N(Y)。

N(Y) :: = SEQUENCE OF

{

N(Y) :: = key ENUMERATED {key1, key2}, ——1个用于设置BOOT标志的函数,包含2个参数

key1 OCTET STRING (1), ——参数key1为一个十六进制数,数值为1

key2 OCTET STRING (2),——参数key2为一个十六进制数,数值为2

}

其次,基于混合和扩展后的活动图和顺序图描述接口的使用方式及动作。在产品具体实现中,逻辑(函数)接口M(X)和N(Y)配合使用,且具有先后顺序,因此以此2个接口为例描述如图 7所示。

图 7 混合使用活动图和顺序图的接口行为描述

最后,描述模块间与安全功能要求相关的交互关系。以BOOT API模块为例描述如图 8所示。

图 8 模块交互

5 安全策略与设计规范一致性验证

安全策略与设计规范一致性验证即验证产品具体设计方法与安全功能要求对应的安全策略两者是否一致。如果一致,则证明产品安全设计满足安全功能要求。

安全功能接口是外界与安全功能交互的入口,可围绕接口设计安全功能控制策略(如参数、使用方式、动作等的设计)和交互策略(接口对应的模块、子系统交互等)。通过节3对IC卡芯片安全功能接口的半形式化得到:

1) PAD用于实现测试模式到用户模式单向转换,用户模式只能在特定条件下使用此接口,与“有限的能力”策略对应;

2) O用于实现BOOT模式与COS用户模式单向转换,此接口对于COS模式来说不可见,与“有限的可用性”策略对应;

3) P用于实现BOOT模式封口,此接口对于COS模式来说不可见,与“有限的可用性”策略对应;

4) M(X)和N(Y)共同用于实现COS用户模式向BOOT模式跳转,此接口对于BOOT模式来说不可见,与“有限的可用性”策略对应。

由此得到,该IC卡芯片的安全设计完整覆盖安全功能要求对应的安全策略。因此,设计规范是安全功能要求的一个完整且正确的实例化。

6 结论

为实现对安全功能要求的正确理解,减少信息技术产品在设计上的内在安全缺陷,本文提出了一种半形式化的安全策略及设计规范描述方法。通过描述安全策略的特征提取和设计规范的半形式化描述框架,改进已有的半形式化表达工具,并以芯片EAL5+测评为例,对部分功能的安全策略和设计规范进行了半形式化分析。该文建立的半形式化方法可为后续开展产品高保障级测评提供借鉴。

参考文献
[1] Bañón M. Security evaluation, testing and specification [C]//In SC27 Security Techniques of 25 Years of Information Security Standardization (1990—2015). London, UK:Gipping Press, 2015: 124-130.
[2] ISO/IEC 15408. Information Technology-Security Techniques-Evaluation Criteria for IT Security [S]. Wellington, New Zealand: ISO/IEC, 2009.
[3] GB/T 18336. 信息技术安全技术信息技术安全评估准则[S]. 北京: 中国国家标准化管理委员会, 2016. GB/T 18336.Information Technology-Security Techniques-Evaluation Criteria for IT Security [S]. Beijing: Standardization Administration of the People's Republic of China, 2016. (in Chinese)
[4] Bundesam FVr Sicherheit der Informationstechnik. Guideline for the development and evaluation of formal security policy models in the scope of ITSEC and Common Criteria, version 2.0[Z/OL]. (December 2007). http://www.bsi.bund.de/cae/servlet/contentblob/478122/publicationFile/30243/Guideline_FMSP_v20_pdf.
[5] Narasamdya I, Périn M. Certification of smart-card applications in Common Criteria: Proving representation correspondences[Z/OL]. (November 2008). http://www-verimag.imag.fr.
[6] Schellhorn G, Reif W, Schairer A, et al. Verification of a formal security model for multiapplicative smart cards[J]. Lecture Notes in Computer Science, 2000, 1(1): 17–36.
[7] GB/T 22186. 信息安全技术具有中央处理器的IC卡芯片安全技术要求[S]. 北京: 中国国家标准化管理委员会, 2016. GB/T 22186. Information Security Techniques-Security Technical Requirements for IC Card Chip with CPU [S]. Beijing: Standardization Administration of the People's Republic of China, 2016. (in Chinese)
[8] ASN.1. Abstract Syntax Notation One [S]. Wellington, New Zealand: ISO/ITU-T, 2001.
[9] Schmuller J. UML基础、案例与应用[M]. 李虎, 王英美, 万里威, 译. 北京: 人民邮电出版社, 2002. Schmuller J. Sams Teach Yourself UML in 24 Hours [M]. LI Hu, WANG Yingmei, WAN Liwei, trans. Beijing: Posts & Telecom Press, 2002. (in Chinese)