模式驱动的系统安全性设计的验证*

郑小宇，刘冬梅，杜益宁，周子健，邱玫媚，朱 鸿

(1.南京理工大学计算机科学与工程学院，江苏 南京 210094；2.Oxford Brookes大学工程、计算和数学学院，英国 牛津 OX33 1HX)

1 引言

随着系统安全性研究的日益深入和安全性技术的不断成熟，研究人员提出了一组可以广泛使用的安全设计模式[1]，以模式组合为基本特征的系统安全性工程已经逐渐成熟[2-4]。其基本思想是，根据实际应用场景中的身份验证、访问控制、数据完整性等安全需求，开发人员识别适用的安全模式，并将这些模式进行组合，形成整个系统的安全解决方案。通常，整个系统的安全解决方案包括多种安全机制，每个机制又可能由多个适合不同应用场景和条件的模式组成。因此，系统的安全性解决方案往往是许多模式的组合。由于系统安全性需求的复杂性和安全机制之间关系的复杂性，是否正确地选择了安全机制、是否正确地使用了实现安全机制的模式、是否正确地将模式组合在一起以达到安全机制的功能等已成为安全性工程亟待解决的问题。针对这些问题，本文提出一个以代数规约为基础的安全解决方案的设计和验证方法。

目前，对安全解决方案进行验证的主要思路是先将UML模型转换成通信演算系统CCS(Calculus of Communicating Systems)[5]、Petri网和代数规约[6]、Alloy[7]等形式化规约，再使用模型检测工具进行验证。这类方法能够较好地验证单个安全模式是否满足给定的安全需求，但缺少对模式组合细节的描述，难以验证组合的正确性。虽然也可将系统的安全解决方案看做一个整体，应用这些方法来验证系统的安全性，但是系统的规模和复杂度限制了这些方法的实用性，而且当发现错误时难以迅速定位缺陷。此外，模型检测工具只能用于验证模型属性，无法进一步对系统实现进行安全性测试。

代数规约是一种支持自动化软件测试的形式化方法，已被广泛应用于面向对象的软件、软件构件、Web服务描述和测试中[8 - 10]。大量案例研究表明[11 - 13]，相对于其他形式化方法，代数规约具有简短精确、易学易理解、高度模块化等特点，更适合描述复杂的系统。文献[14]提出了代数规约的组合方法，使用由抽象规约和实现规约组成的双元结构描述服务组合，其中抽象规约描述服务组合结果的需求，实现规约描述如何将已知服务组合在一起。文献[14]还阐明了如何用已知服务的代数规约和组合描述的双元结构形式化地证明服务组合的正确性。本文中的案例表明，该双元结构也适用于描述安全模式的组合，其中抽象规约描述系统的安全需求，实现规约描述安全解决方案中如何将安全模式进行组合以满足需求。此外，本文在已有工作的基础上，进一步研究对代数规约组合的自动验证，应用模型检测工具自动分析并验证安全解决方案规约的正确性。

本文提出的方法可以概括为4个步骤:(1)首先使用模块化设计思想对安全解决方案的结构进行分解，确定方案中包含的基本模块和模块间的依赖关系，以及各个模块所使用的模式。(2)使用代数规约语言以代数为基础的面向服务的形式化语言SOFIA(Service-Oriented Formalism In Algebras)描述每个基本模块中包含的数据结构和操作，确定模块是如何将模式实例化的，并验证基本模块的形式化规约是否满足安全需求。(3)使用SOFIA抽象规约和实现规约分别描述组合模块的对外功能和内部实现，并验证模块是否正确组合了其使用的模式且满足安全需求。(4)通过基于代数规约的自动测试检查系统实现的正确性。由于篇幅所限，本文仅讨论安全性的形式化验证，对于自动测试的研究将另文报告。

2 系统安全性设计与验证流程

如图1所示，模式驱动的系统安全性建模和验证流程包括设计流程、形式化建模流程和验证流程。

Figure 1 Pattern-driven system security design and verification flow图1 模式驱动的系统安全性设计和验证流程

设计流程根据安全性需求将安全解决方案分解为相对独立的模块，并确定各个模块使用的安全解决方案设计模式，然后结合模块间的相互关系构造方案的设计结构图，采用拓扑排序确定模块的建模和验证顺序。

形式化建模流程根据设计方案中使用的安全模式构造各个基本模块的代数规约，然后使用抽象规约和实现规约组成的双元结构描述组合模块。

验证流程将SOFIA语言书写的代数规约转换成Alloy语言的规约后，依次验证基本模块和组合模块规约的正确性。对于基本模块，需要验证其是否满足公理中定义的功能和安全需求；对于组合模块，首先验证其是否正确组合了使用的安全模式，然后验证模块是否满足抽象规约公理中定义的安全需求。

3 安全模式及其代数归约

通过代数规约对安全模式进行建模，有助于进一步分析模式中包含的数据、操作及安全需求，从而为模式驱动的系统安全性建模奠定基础。分析现有的安全模式文档[15]发现，安全模式主要包含模式中使用的数据结构和操作语义，同时包括模式的安全需求、类型和适用平台等相关信息，因此可以使用四元组表示安全模式，其定义如下：

定义1(安全模式(Security Pattern)) 安全模式描述了特定应用场景下的安全需求以及相应的解决方案，使用四元组〈S,O,R,I〉表示，其中：

S表示安全模式中使用的数据类型，描述模式的静态结构。

O表示安全模式中的操作及其语义，描述模式的动态行为。

R表示安全模式要实现的安全需求，通常使用一组操作序列构成的应用场景对其进行描述。

I表示安全模式的相关信息。I=〈C,P,D〉，其中C表示安全模式的类型，如身份认证、访问控制等；P表示安全模式的适用平台，大多数模式独立于平台，少部分模式依赖特定平台；D表示该模式依赖的其他模式。

根据上述定义，使用SOFIA语言描述安全模式的主要结构，构建安全模式的代数规约。代数规约语言SOFIA将模式和S中的每个数据类型定义为一个类子(Sort)，类子包括基调(Signature)和公理(Axiom)2个部分，其中基调描述类型中的数据成员和O中的操作集合，包括各操作的操作名和输入输出参数。公理描述O中的操作行为和模式安全需求R。模式信息I用于辅助开发人员选择合适的模式，与形式化验证无关，使用自然语言描述。

安全模式的代数规约使用三元组〈S,Σ,Ax〉表示[16]，其中，S=〈S,▷,>〉表示规约包含的类子集合及其上的扩展和依赖关系，Σ表示基调集合，Ax表示公理集。本节在文献[16]定义的基础上将规约中的公理集Ax细分为描述数据类型约束的公理集Axattr，描述单个操作语义的公理集Axop以及描述操作组合序列(即应用场景中的安全需求)的公理集Axseq，即Ax=Axattr∪Axop∪Axseq。

下面以基于会话的身份认证模式Session中的创建和验证会话操作为例，说明如何使用代数规约描述安全模式。相关数据类型S包含会话数据和数据库，安全需求R为“通过Session能够获取登录用户信息”，可使用“用户创建Session后查询该Session，结果中的用户ID与创建时的用户ID一致”的应用场景进行描述。

SpecSession;

usesInteger,String;

Attrid:String;uid:Integer;created:Integer;

End

SpecSessDB;

usesListOfSession;

Attrdatas:ListOfSession;

End

SpecSessReturn;

usesSession,SessDB;

Attrsess:Session;sdb:SessDB;

End

SpecSessM;

usesString,Integer,Bool,Expire,SessReturn,…;

Retr

verify_sess(SessDB,String,Integer):Bool;

get_sess(SessDB,String,Integer):Session;

Tran

create_sess(SessDB,Integer,Integer):SessReturn;

Axiom

Foralls:SessM,util:UtilOp,e:Expire,sid:String,

t:Integer,sdb:SessDBthat

letsess=util.getDataById(sid,sdb)in

s.verify_sess(sdb,sid,t) = true;

ifsess〈〉null,sess.last+e.expire>=t;//公理1

s.verify_sess(sdb,sid,t) = false;

ifs= null;//公理2

s.verify_sess(sdb,sid,t) = false;

ifsess.last+e.expire

End

End

Foralls:SessM,util:UtilOp,e:Expire,sid:String,

sdb:SessDB,u,t:Integerthat

letsr=s.create_sess(sdb,u,t)in

sr.sess.uid=u;//公理4

sr.sess.created=t;//公理5

sr.sdb=util.union(sdb,sr.sess);//公理6

End

End

Foralls:SessM,sid:String,sdb1,sdb2:SessDB,

u,t:Integerthat

s.create_sess(sdb1,u,t);get_sess(sdb2,sid,t).uid=u;

ifsdb2=s.create_sess(sdb1,u,t).sdb;

sid=s.create_sess(sdb1,u,t).sess.id;//公理7

End

End

上述规约中的类子集合S包括模式类子SessM，数据库SessDB、会话Session和操作结果SessReturn，其中SessM类子的基调定义了验证操作verify_sess、创建操作create_sess和查询操作get_sess，公理集合中的公理1～公理3描述验证操作，表示仅当Session不为空且未过期时才能通过验证并返回true，否则返回false；公理4～公理6则描述创建操作，表示新创建的Session中保存当前用户的ID和创建时间t；Axseq中的公理7则描述了上述应用场景，表示用户依次调用创建和查询操作，如果调用查询操作时提供的Session ID等于创建Session时返回的Session ID，则返回Session中的用户ID与当前用户一致。

4 安全解决方案的设计和建模

4.1 安全解决方案的模块化设计

设计安全解决方案的主要思路是根据系统安全需求确定方案应实现的功能，将其分解为一系列模块，并确定模块使用的安全模式，为形式化建模打下基础。在模块化设计的过程中，基本模块粒度过大往往会导致模块内部仍存在复杂的结构，从而加大建模的难度；而粒度过小则需要将模块进行多次组合，使建模流程变得繁琐。针对这一问题，本文根据现有软件模块化设计研究[17,18]给出的策略设计安全解决方案，并分析各个模块对外提供的接口和需要调用的接口，确定模块间的依赖关系，从而构造安全解决方案的设计结构图，其定义如下：

定义2(安全解决方案的设计结构图(Structure Diagram of Security Solution)) 一个安全解决方案的设计结构图G=〈N,E,l〉使用L(L≥2)层有向无环图表示，其中:

N表示节点集，N=Ns∪Nm，其中Ns表示基本模块节点集合，Nm表示组合模块节点集合。

E表示边集，E=Ed∪Ec,Ed中的边表示模块间的依赖关系，使用带箭头的实线表示;Ec中的边表示模块间的组合关系，使用带菱形的实线表示，Ec⊆(Ns×Nm)∪(Nm×Nm)。对于边(n,n′)∈Ec，称n是n′的一个子模块。

l表示节点层次标识函数n→{i|0≤i≤L-1}，基本模块节点ns的层数l(ns)=0;组合模块节点nm的层数l(nm)=max(l(Nsub))+1，其中Nsub为nm的子模块集合。

图2以一个基于区块链的医疗数据管理方案DataM为例，给出了该安全解决方案的设计结构。该方案的安全需求为仅允许用户对其拥有的数据或具有访问权限的数据进行操作，当数据所有者为多个用户时，由这些用户共同决定是否授予其他用户访问权限。因此安全解决方案需实现数据操作、访问控制和共识机制等功能，划分为DataOp、DataAC和Vote 3个子模块，其中DataOp模块无需使用安全模式，Vote模块使用投票模式；然后进一步分析DataAC包含的2种访问控制机制，将其划分为基于数据所有者的Owner和基于策略的Policy 2个子模块；最后根据模块接口的相互调用确定依赖关系，完成设计结构图的构造。

Figure 2 Structure diagram of security solution design图2 安全解决方案的设计结构图

设计结构图同时反映出模块的建模和验证顺序，由定义1可知，图中节点的入度表示该模块依赖和组合的其他模块数量，因此采用拓扑排序思路优先遍历层数较低的节点生成模块序列，如DataOp→Owner→Policy→Vote→DataAC→DataM。

4.2 安全解决方案的建模

安全解决方案的建模流程包括2个主要步骤：首先根据设计结构图给出的建模顺序依次将各个基本模块使用的安全模式实例化，然后使用抽象规约和实现规约分别描述组合模块的对外功能和内部实现。

安全模式中往往使用抽象数据类型，与实际应用中的数据类型存在一定差异，其代数规约无法直接用于安全解决方案的建模。因此，需要对基本模块使用的安全模式进行实例化，将模式规约中描述抽象数据的类子替换为描述应用场景中具体数据的类子，并更新使用这些类子的操作和公理。实例化操作得到的基本模块代数规约与安全模式的代数规约相同，使用三元组〈S,Σ,x〉表示。

以基于数据所有者的访问控制模式Owner为例，若使用该模式构建病历管理模块，其包含的抽象数据类型SOData需要实例化为病历数据MedicalCase，将owner属性更名为patient_id，同时新增了就诊时间visit_time和就诊医院hospital等属性，实例化前后的类子规约如下所示：

SpecSOData; //实例化前的类子SOData

usesInteger;

Attr

owner:Integer;

End

SpecMedicalCase;//实例化后的类子MedicalCase

usesInteger,Date,String;

Attr

patient_id:Integer;

visit_time:Date;

hospital:String;

End

实例化后的MedicalCase数据类型使用patient_id属性存储病历所有者，因此验证数据所有者操作中的公理也更新为使用patient_id属性与当前用户ID进行比较,相关公理如下所示：

//实例化前的公理

o.owner_verifier(db,uid,i) = true,ifd.owner=uid;

//实例化后的公理

o.owner_verifier(db,uid,i) = true,ifd.patient_id=ac.id,…;

以4.1节中的DataM模块为例，该模块为包含DataAC、DataOp和Vote 3个子模块的组合模块，其代数规约包括抽象规约DataM和实现规约DataMImp 2部分。模块中的数据更新操作update的相关公理如下所示：

dac.update(ac,s,did,db,pdb).content=s,

ifdac.access_verifier(ac,did,2,pdb) = true;∥axA

dac.update(ac,s,did,db,pdb) =dac.dop.update(ac,s,did,db),

ifdac.access_verifier(ac,did,2,pdb) = true;∥axI

抽象规约中的公理axA表示若当前用户通过权限验证，则返回更新后的数据内容；实现规约中的公理axI则表示首先调用DataAC中的权限验证操作，若验证通过再调用DataOp中的数据更新操作实现更新功能。

5 代数规约的转换和验证

本节将SOFIA规约转换为Alloy规约后，使用模型检测工具[19]依次验证方案中的基本模块是否满足安全需求，以及组合模块是否正确组合了其子模块且满足安全需求。其中SOFIA规约中描述数据类型的类子对应为Alloy规约中的signature，类子的基调对应为Alloy规约中的enum或field。对于区块链应用中的基本模块，其SOFIA规约中描述单个操作的公理定义了各个操作的行为，对应为Alloy规约的谓词；而描述操作序列的公理定义了模块在具体应用场景中的安全需求，对应为Alloy规约的断言。对于组合模块，实现规约公理必须正确实现抽象规约公理中定义的模块行为，因此对应为Alloy规约的谓词；而抽象规约中的公理对应为断言，用于验证模块使用的安全模式是否被正确组合和模块是否满足安全需求。接下来将在此基础上分析2种规约间的映射关系并构造转换规则，从而将区块链应用的SOFIA规约转换为Alloy规约。

5.1 基本模块的规约转换

基本模块的Alloy规约使用七元组〈S,M,Enum,F,O,P,A〉表示，定义如下：

定义3(基本模块的Alloy规约(Alloy Specification of Basic Module)) 使用Alloy语言对基本模块进行形式化描述，所得规约是一个七元组〈S,M,Enum,F,O,P,A〉，其中：

S表示基本模块中的类和类之间的继承关系。S=〈S,▷〉，其中S表示规约中signature的集合，▷表示S上的扩展(继承)关系。

M(Members)表示类中的数据成员，M={Ms|s∈S}，Ms表示s中的数据成员集合。

Enum(Enumeration)表示模式中的枚举类型集合。

F(Fact)表示模块中数据类型应满足的约束，F={Fs|s∈S}，其中Fs表示对s中数据成员的约束。对于每个f∈F，f=〈fV,fp〉,其中fV为变量集合，fp为一个约束条件。

O(Operation)表示模块中的操作集合。对于每个o∈O，o=〈φ,In,Out〉分别表示操作名和操作的输入输出参数集合。

P(Predicate)表示模块中操作的行为。P={Po|o∈O}，其中Po表示对操作o的谓词约束集合。

A(Assert)表示模块的安全需求。对于每个a∈A,a=〈aV,ap〉，其中aV表示断言中使用的变量集合，ap=〈seq,ae〉表示断言中的谓词约束，seq表示谓词中包含的操作序列，ae表示执行操作序列后应成立的等式。

根据上述定义，分析2种规约之间的映射关系，进而给出以下的转换规则：

规则1将SOFIA规约中的S转换为Alloy规约中的S。其中，SOFIA规约的类子集合S和扩展关系▷转换为Alloy规约的signature集合S和扩展关系▷，而使用关系在Alloy规约中没有显式定义，无需转换。

规则2对于SOFIA规约中每个类子的基调单元Σs∈Σ，将其中的常操作子(Const)加入Alloy规约的枚举类型集合Enum，属性操作子(Attr)转换为Alloy规约中对应signature的数据成员Ms∈M，其它操作子(Retr&Tran)则转换为Alloy规约中的一个操作o∈O。

规则3对于SOFIA规约中每个描述数据类型约束的公理axattr=〈V,e〉，转换为Alloy规约中的f∈F，其中变量集V转换为fV，条件等式e转换为fp。

规则4对于SOFIA规约中每个描述单个操作的公理axop=〈V,e〉，将公理中的条件等式e转换为Alloy规约中对应操作o的一条谓词约束po∈Po，其中变量为操作o的输入输出参数。

规则5对于SOFIA规约中每个描述操作序列的公理axseq=〈V,e〉，转换为Alloy规约中的一个断言a∈A，其中变量集V转换为aV，条件等式e转换为seq⟹ae。

根据上述规则构造基本模块的规约转换算法，表1给出了算法中使用的符号及描述。

Table 1 Symbols and descriptions in algorithm 1

算法1基本模块的规约转换算法

输入:基本模块SOFIA规约〈S,Σ,Ax〉。

输出:基本模块Alloy规约〈S,M,Enum,F,O,P,A〉。

1.foreachs∈Sdo/* 遍历SOFIA规约的类子，根据规则1和2进行转换 */

2.S←S+s;▷←▷+▷S;/* 转换类子s及其扩展关系 */

5.endfor

6.S=〈S,▷〉;

7.foreachax∈Axdo//遍历公理集合

8.ifax∈Axattrthen/*根据规则3将描述数据约束的公理转换为fact*/

9.fV=ax.v;fp=ax.e;F←F+〈fV,fp〉;/*将转换得到的fact加入集合F*/

10.endif

11.ifax∈Axopthen/* 根据规则4将描述单个操作的公理转换为一条谓词约束 */

12.o=∏op(ax);Po←Po+ax.e;/* 将公理等式加入对应操作o的谓词集合 */

13.endif

14.ifax∈Axseqthen/* 根据规则5将描述操作序列的公理转换为断言 */

15.seq=∏oplist_seq(ax);aV=ax.v;ae=ax.e;/* 获取公理的操作、变量和等式*/

16.foreacho∈seqdo/* 遍历操作集合，将操作的输出变量加入变量集 */

17.aV←aV+∏out(o);

18.endfor

19.A←A+〈aV,〈seq,ae〉〉;/*将转换得到的断言加入集合A*/

20.endif

21.endfor

22.foreacho∈Odo/* 公理处理完成后，遍历操作集合 */

23.P←P+Po/* 将遍历到的操作的谓词加入集合P*/

24.endfor

25.return〈S,M,Enum,F,O,P,A〉

5.2 组合模块的规约转换

组合模块使用其子模块定义的数据类型，因此其Alloy规约不包含对数据类型的描述，使用三元组表示，定义如下：

定义4(组合模块的Alloy规约(Alloy Specification of Composition Module)) 使用Alloy语言对组合模块进行形式化描述，所得规约是一个三元组〈O,P,A〉，其中：

O(Operation)表示模块中的操作集合。

P(Predicate)表示模块中操作的内部实现。P={Po|o∈O}，其中Po表示描述操作o内部实现的谓词集合。

以下规则从组合模块的SOFIA规约中提取出定义操作的基调集合、描述操作内部实现和功能特性的公理集合，以及描述操作序列的公理集合，并将其转换为Alloy规约：

规则6将抽象规约的基调集合ΣA加入Alloy规约的操作集合O。

规则9将实现规约的基调集合ΣI加入Alloy规约的操作集合O。

规则10对于实现规约的每条公理axI=〈V,e〉，将公理中的条件等式e转换为Alloy规约中对应操作o的一条谓词约束po∈Po，其中变量为操作o的输入输出参数。

根据上述规则给出组合模块的规约转换算法，算法的主要思路是依次处理抽象规约的基调和公理集，分别转换为Alloy规约的操作集合和断言集合，然后将实现规约的公理转换为Alloy规约中对应操作的谓词。除表1中定义的符号外，该算法还需要使用∏op_imp(axI)和∏oplist_abs(axA)2个符号，其中∏op_imp(axI)表示实现规约公理axI的对应操作，∏oplist_abs(axA)表示抽象规约公理axA包含的操作集合。

算法2组合模块的规约转换算法

输入:组合模块SOFIA规约，包括实现规约SI和抽象规约SA。

输出:组合模块Alloy规约〈O,P,A〉。

1.O←O+ΣA/* 将抽象规约的基调单元加入操作集合O*/

2.foreachax∈AxA do//遍历抽象规约的公理集

3.seq=∏oplist_abs(ax);aV=ax.v;e=ax.e;/*获取公理的操作集、变量集和等式*/

4.foreacho∈seqdo/* 遍历操作集合，将操作的输出变量加入变量集 */

5.aV←aV+∏out(o);

6.endfor

9.elseAseq←Aseq+〈aV,〈seq,e〉〉;/* 否则加入描述安全需求的集合Aseq*/

10.endif

11.endfor

12.foreachax∈AxIdo//遍历实现规约的公理集

13.o=∏op_imp(ax);Po←Po+ax.e;/* 将公理等式加入对应操作o的谓词集合*/

14.endfor

15.foreacho∈Odo/* 实现公理处理完成后，遍历操作集合 */

17.endfor

18.A=Aop+Aseq;

19.return〈O,P,A〉

5.3 安全解决方案的验证

安全解决方案的规约中往往存在操作的前后置条件定义错误、模块间的操作调用错误等缺陷，导致方案无法满足安全需求。本节使用模型检测工具Alloy Analyzer分析规约中的谓词和断言，检查规约中是否存在上述缺陷，从而对规约的正确性进行验证。

规约的验证过程包括2个阶段，第1阶段验证基本模块是否满足安全需求，第2阶段验证组合模块是否正确组合了其子模块且满足安全需求。下面分别介绍2个验证阶段的主要步骤。

在第1阶段中，对于方案中的每个基本模块，首先执行由谓词定义的操作，以检查该操作的前后置条件是否与模块中的其他公理存在相互矛盾。然后将模块中的断言改写为谓词，其中断言包含的全局变量被转换为谓词的变量，断言等式被转换为谓词等式，改写示例如下所示：

assertassertion{//改写前的断言

allv1:type1,v2:type2 |op[v1,v2] ⟹v1=v2

}

predpredicate[v1:type1,v2:type2] {/*改写后的谓词*/

op[v1,v2] =>v1=v2

}

改写后的谓词用于检查断言中定义的操作序列和需求是否存在矛盾，最后验证各个断言是否成立，以检查模块是否满足断言中定义的安全需求。

第2阶段中对组合模块的验证包括以下3个步骤，其中步骤1和步骤2用于验证模块组合的正确性，步骤3用于验证模块是否满足需求。

步骤1验证模块中各个谓词的可满足性。

组合模块中的谓词定义了模块中的操作如何通过调用其子模块中的的操作实现相应功能，如果谓词中的操作调用是正确的，则谓词应当是可满足的，即能够生成满足谓词的实例。因此，对于模块中每个操作o对应的谓词，使用模型检测工具生成满足谓词的实例。如果无法生成实例，则表明操作调用存在错误。

步骤2验证模块中各个操作的功能特性。

步骤3验证应用场景中的安全需求。

组合模块中描述操作序列的断言定义了模块在应用场景中应满足的安全需求。因此，对于模块中每个描述操作序列的断言，首先将断言改写为谓词并生成实例，若能够生成实例，则表明断言中不存在相互矛盾。然后在给定范围内生成违背断言的反例，若无法生成反例，则表明断言在给定范围内成立，即模块满足该断言中定义的安全需求。

根据文献[20]中案例研究的结论，较小范围的实例能够检测出绝大多数的缺陷，因此可以认为经过上述步骤验证的断言对所有实例都成立。

6 案例研究

6.1 案例描述

本文以4.1节的安全解决方案DataM为研究案例，该方案由基本模块DataOp、Vote和组合模块DataAC组成，因此其SOFIA规约包含Basic、UtilOp、DataOp、Owner、Policy、Vote、DataAC、DataACImp、DataM、DataMImp共10个规约包[14]，规约结构如图3所示。

Figure 3 Specifications structure of security solution DataM图3 安全解决方案DataM规约结构

规约中的Basic描述方案中使用的基本数据类型；UtilOp描述了一些公共操作，如集合操作、查询操作等；Owner、Policy、Vote、DataOp分别是数据所有者验证、访问策略管理、投票管理以及数据操作规约包；DataAC和DataACImp分别是访问权限验证的抽象规约包和实现规约包；DataM和DataMImp分别是数据管理方案的抽象规约包和实现规约包。对应的Alloy规约将组合模块的抽象规约和实现规约合并为一个模块，其余部分的结构与SOFIA规约基本相同。

由于Basic、UtilOp、DataOp中不包含数据安全相关的操作，因此本案例主要分析Owner、Policy等7个规约包及其转换后的Alloy规约模块。SOFIA规约中的类子、操作和公理数量及对应Alloy规约中的signature(表中简写成sig)、fact、谓词和断言数量见表2。

Table 2 Statistics of specifications

6.2 实验结果和分析

将Alloy规约中具有相同操作序列的断言合并后，首先使用Alloy Analyzer分析Owner、Policy和Vote基本模块中的谓词和断言，验证基本模块的正确性，然后执行DataAC和DataM规约中谓词描述的操作并验证描述单个操作和安全需求的断言，从而验证组合的正确性和模块的安全性。以DataM规约为例，其合并断言后的Alloy规约中包含4个谓词集合、4个描述单个操作的断言集合和10个描述安全需求的断言集合，验证结果显示描述操作的谓词及断言改写的谓词均能生成实例，且断言均无法生成反例，表明该方案能够满足定义的安全需求。

接下来向方案的SOFIA规约中注入单缺陷，再转换为Alloy规约进行验证。其中，注入缺陷的位置为基本模块规约和组合模块实现规约中描述单个操作的公理，此类公理被转换为Alloy规约中描述操作的谓词，因此能够通过验证模块中的断言检测注入的缺陷。注入缺陷后的规约不能存在语法错误，否则将无法进行规约转换和验证。

注入缺陷的类型包括替换公理中的常量、变量和操作，添加或删除公理，删除公理中的if条件等文献[21]给出的代数规约常见缺陷。这些缺陷往往改变了模式中部分操作的前后置条件，或改变了模式间的操作调用关系，导致模式无法实现预期的安全需求。以下面的公理为例：

pr.p.right=op;//公理1

pr.p.right=uid; //缺陷公理1(替换变量)

//公理2

dac.getdata(uid,did,db,pdb) =dac.dop.getdata(db,did);

//缺陷公理2(替换操作)

dac.getdata(uid,did,db,pdb) =dac.dop.deldata(did);

公理1为Policy规约中描述添加策略操作的公理，表示新策略的权限等级right等于输入参数op。注入缺陷后变量op被替换为uid，即用户id，导致添加策略操作出现错误。公理2为DataMImp规约中描述数据查询操作的公理，表示调用DataOp模块中的getdata操作查询数据。注入缺陷后getdata操作被替换为删除数据操作deldata，导致模式间的调用出错。

根据注入缺陷位置的不同，验证方法可分为2类。对于基本模块缺陷，首先执行存在缺陷的操作谓词，再验证该模块中的断言；对于组合模块缺陷，首先执行存在缺陷的操作谓词，再依次验证该模块中描述单个操作的断言和安全需求的断言。若验证过程中描述操作的谓词或由断言改写的谓词无法生成实例，以及断言成功生成反例，则表明该方法能够发现缺陷，否则无法发现缺陷。表3给出了注入150个单缺陷后的验证结果，即发现的缺陷数量与注入缺陷总数之比。

Table 3 Verification results of defect injection

分析表3中给出的验证结果，可得出以下结论：

(1)上述验证方法能够检测出规约中的大部分缺陷。表3的验证结果显示，在注入的150个缺陷中有12个缺陷未被检测出。进一步分析未被检测出的缺陷发现，其中5个缺陷没有改变操作的行为，如替换一个对操作结果没有影响的常量，或添加一条if条件永不成立的公理。以Vote模块中的部分公理为例，这些公理表示根据投票属性policyOp执行权限授予、更新或解除3种操作。policyOp为枚举类型，仅包含这3种操作，而缺陷公理的if条件表示policyOp不为这3种操作中的任何一种，因此这个条件不可能成立，缺陷公理对操作没有影响。

auth_grant_sys(pdb,v.user,v.data,v.right),ifv.op=grant;

auth_update_sys(pdb,v.policy,v.right),ifv.op=update;

auth_revoke_sys(v.policy,pdb),ifv.op=revoke;

//缺陷公理

…,ifv.op〈〉grant,v.op〈〉update,v.op〈〉revoke;

(2)模块中的公理必须正确、完整地描述安全需求。若公理缺少对部分应用场景的描述，则无法检测出这些应用场景中的缺陷，未检测出的7个缺陷属于此类。如Policy模块的授权操作中包含一个条件判断，当用户没有权限或权限较低时才执行操作，以防止重复授权。注入的缺陷删除了这一条件，但由于模块中的公理没有描述重复授权的场景，因此无法检测出该缺陷。

实验结果和上述分析表明，本文方法能够有效地检测出安全模式中的缺陷，但仍然存在一些问题。该方法只能验证方案和定义的安全需求是否一致，而不能发现安全需求定义本身存在的漏洞。此外，组合模块中描述安全需求的断言往往包含3个以上的操作，导致验证时生成的反例较为复杂，如DataM规约中的反例往往包含40个以上的变量，增加了在组合模块中定位缺陷的难度。

7 结束语

本文提出了一个模式驱动的系统安全性设计与验证方法，首先使用模块化思想设计安全解决方案并确定方案中各个模块使用的安全模式，然后使用SOFIA语言对模块中包含的数据结构和操作语义进行建模，最后将SOFIA规约转换为Alloy规约进行安全性验证。案例研究表明，该方法能够有效地验证安全解决方案设计的正确性。下一步的工作将使用SOFIA语言对常用的安全模式进行建模，构建安全模式库，并将该方法应用到一个完整的区块链医疗系统的开发过程中，结合模型检测和自动测试2种方式验证该系统，以提高区块链应用的安全性。