可信执行环境访问控制建模与安全性分析.pdf

可信执行环境访问控制建模与安全性分析*苗新亮1,2,常瑞2,3,潘少平2,赵永望2,蒋烈辉11(数学工程与先进计算国家重点实验室(战略支援部队信息工程大学),河南郑州450002)2(浙江大学计算机科学与技术学院,浙江杭州310027)3(浙江省区块链与网络空间治理重点实验室,浙江杭州310027)通信作者:常瑞,E-mail:摘要:可信执行环境(TEE)的安全问题一直受到国内外学者的关注.利用内存标签技术可以在可信执行环境中实现更细粒度的内存隔离和访问控制机制,但已有方案往往依赖于测试或者经验分析表明其有效性,缺乏严格的正确性和安全性保证.针对内存标签实现的访问控制提出通用的形式化模型框架,并提出一种基于模型检测的访问控制安全性分析方法.首先,利用形式化方法构建基于内存标签的可信执行环境访问控制通用模型框架,给出访问控制实体的形式化定义,定义的规则包括访问控制规则和标签更新规则;然后利用形式化语言 B 以递增的方式设计并实现该框架的抽象机模型,通过不变式约束形式化描述模型的基本性质;再次以可信执行环境的一个具体实现 TIMBER-V 为应用实例,通过实例化抽象机模型构建 TIMBER-V 访问控制模型,添加安全性质规约并运用模型检测验证模型的功能正确性和安全性;最后模拟具体攻击场景并实现攻击检测,评估结果表明提出的安全性分析方法的有效性.关键词:内存标签;可信执行环境;访问控制;模型检测;安全性分析中图法分类号:TP311中文引用格式:苗新亮,常瑞,潘少平,赵永望,蒋烈辉.可信执行环境访问控制建模与安全性分析.软件学报,2023,34(8):36373658.http:/ and Security Analysis of Access Control in Trusted Execution EnvironmentMIAOXin-Liang1,2,CHANGRui2,3,PANShao-Ping2,ZHAOYong-Wang2,JIANGLie-Hui11(State Key Laboratory of Mathematical Engineering and Advanced Computing(Strategic Support Force Information EngineeringUniversity),Zhengzhou450002,China)2(CollegeofComputerScienceandTechnology,ZhejiangUniversity,Hangzhou310027,China)3(KeyLaboratoryofBlockchainandCyberspaceGovernanceofZhejiangProvince,Hangzhou310027,China)Abstract:The security of the trusted execution environment(TEE)has been concerned by Chinese and foreign researchers.Memory tagtechnologyutilizedinTEEhelpstoachievefiner-grainedmemoryisolationandaccesscontrolmechanisms.Nevertheless,priorworksoftenrely on testing or empirical analysis to show their effectiveness,which fails to strongly guarantee the functional correctness and securityproperties.Thisstudyproposesageneralformalmodelframeworkformemorytag-basedaccesscontrolandintroducesasecurityanalysismethod in access control based on model checking.First,a general model framework for the access control model of TEE based onmemory tag is constructed through a formal method,and those access control entities are formally defined.The defined rules include*基金项目:国家自然科学基金(61872016,62132014)本文由“形式化方法与应用”专题特约编辑陈立前副教授、孙猛教授推荐.收稿时间:2021-08-30;修改时间:2021-10-14;采用时间:2022-01-10;jos 在线出版时间:2022-01-28CNKI 网络首发时间:2023-01-19软件学报ISSN1000-9825,CODENRUXUEWE-mail:Journal of Software,2023,34(8):36373658doi:10.13328/ki.jos.006612http:/中国科学院软件研究所版权所有.Tel:[phone]accesscontrolrulesandtagupdaterules.Thenabstractmachinesundertheframeworkareincrementallydesignedandimplementedwithformal language B.In addition,the basic properties of the machines are formalized through invariant constraints.Next,a TEEimplementation called TIMBER-V is used as an application case.The TIMBER-V access control model is constructed by instantiatingthese abstract machines,and the security properties are formally specified.Furthermore,the functional correctness and security of themodelsareverifiedbasedonmodelchecking.Finally,thisstudysimulatesthespecificattackscenarios,andtheseattacksaresuccessfullydetected.Theevaluationresultshaveprovedtheeffectivenessofthesecurityanalysismethod.Key words:memorytag;trustedexecutionenvironment(TEE);accesscontrol;modelchecking;securityanalysis可信执行环境(trustedexecutionenvironment,TEE)是利用软硬件隔离机制提供的一块可信区域,通过对加载到该区域的数据和代码提供机密性和完整性保护,防御来自恶意系统的攻击.近几年,TEE 技术在工业界和学术界均受到持续关注,工业界的主流 TEE 实现方案包括 ARMTrustZone1、IntelSGX2、AMDSEV3等,学术界已有的典型方案包括 TIMBER-V4、Sanctum5、Sanctuary6、Keystone7等.这些 TEE 实现方案广泛应用于云端和设备端来托管数字产权管理8、移动支付911和生物特征识别12等安全功能.然而,随着 TEE 中曝出越来越多的漏洞1318,其安全性正面临着严重的挑战.为了提高 TEE 自身的安全性,研究者们提出了一些增强内存隔离性的方案.这些方案或通过在不可信区域构建隔离域以支持可信应用运行6,1921,或通过对可信区域进行进一步划分以增加隔离区域数量7,22,23.尽管这些方案有效减小了 TEE 系统的攻击面,但由于这些内存隔离仍然是区域(region)级的,即保护的内存在连续的地址空间中,因此无法支持更细粒度的安全保护策略.同时,隔离区域的增加也意味着更大的性能损耗.为此,内存标签(memorytag)技术逐渐应用于 TEE 的内存保护中.内存标签的核心是在每个内存字上划分若干位作为标签位,用于标识内存对象上的某种属性,可以提供细粒度、灵活的隔离边界.AMD 上的 TEE 实现方案如 SEV3,SEV-ES24,SEV-SNP25利用物理地址上的 4346 位标记不同的虚拟机,当通过页表访问虚拟机内存(可信区域)时,根据虚拟机物理地址携带的标签判断访问哪个虚拟机数据.此外,TIMBER-V4在内存字上使用 2 位标签位标记不同的隔离区域并根据标签判断访问是否允许,而 PENFLAI26利用所有权位图来标记每个物理页的状态,区分属于可信区域还是不可信区域.这些方案均实现了页表级的内存隔离以支持更细粒度的访问控制策略,有效地防御了某些攻击.然而,这些利用内存标签的方案都是以测试或经验分析的方式对访问控制机制的有效性进行评估,一直缺乏严格的功能正确性和安全性分析,因此数据泄露16、任意代码执行27、提权28,29等攻击仍时有发生.为解决上述问题,本文利用形式化方法对 TEE 访问控制进行研究,形式化方法是借助数学方法建立数学模型并进行模型验证的方法,可以对模型满足的性质提供严格的保证30.本文的研究工作主要包括两个方面.(1)对基于内存标签的 TEE 访问控制进行形式化建模.针对基于内存标签的 TEE 访问控制机制,本文提出通用的模型框架,该框架基于 TEE 提供的隔离区域建立标签域,然后利用标签在较高的抽象层次上定义了主体属性、客体属性和权限操作,并构建了安全规则,包括访问控制规则和标签更新规则.结合 TEE 系统运行过程,分析了访问控制中的状态迁移行为,并描述了基本操作和需要满足的基本安全性质.本文利用形式化语言 B 设计并实现了该框架的访问控制抽象机模型,包括标签、主体、客体和策略 4 个基本实体抽象机和访问控制执行抽象机.同时抽象机模型使用形式化的规范描述了作用于模型操作中的不变式约束以保证无二义性.基于创建的标签域,该框架和抽象机模型适用于 ARMTrustZone 系列、AMDSEV 系列以及基于 RISC-V 的 PENGLAI,Keystone,TIMBER-V 等 TEE 方案.(2)实现基于模型检测的 TEE 访问控制安全性分析.为实现基于内存标签的 TEE 访问控制安全性分析,本文提出一种基于模型检测的安全性分析方法.通过分析具体的访问控制规则、标签更新规则以及系统中的安全操作,以不变式约束的形式对访问控制安全性质进行规约,并利用模型检测工具 ProB 检测构建的模型是否符合安全性质,实现模型功能正确性和安全性的验证.同时,结合威胁模型的定义,构建威胁操作以模拟攻击场景,并通过模型检测验证威胁模型是否与安全性质冲突以实现攻击检测.本文以 TIMBER-V 中的访问控制为应用案例,结合TIMBER-V 的具体实现,通过实例化通用模型构建了 TIMBER-V 基于内存标签的访问控制模型,然后利用提出的安全性分析方法实现了 TIMBER-V 访问控制安全性分析.3638软件学报2023 年第 34 卷第 8 期本文的主要贡献如下.(1)提出一种基于内存标签的 TEE 访问控制通用模型框架 MTF:通过构建 TEE 标签域,将标签属性赋给访问控制实体并给出各实体的形式化定义,框架还分析系统访问控制状态迁移关系,描述访问控制基本操作和性质,同时利用形式化 B 方法实现该框架的抽象机模型,重点设计 4 个基本实体抽象机并递增构建了基于内存标签的 TEE访问控制模型 MTAC,形式化描述了基本实体操作,支持模型扩展和改进.(2)模型实例化:为验证(1)提出的模型框架的通用性,以 TEE 的一个典型实现 TIMBER-V 为应用案例,实现模型实例化,结合系统实现方式分别对基本实体抽象机和模型 MTAC 进行了修改和扩展,构建 TIMBER-V 访问控制模型 MTAC_TIV,包含 42 个实体操作以及 16 个安全不变式(框架和实例化模型开源在 https:/ 14699098 个状态和 37834011 个状态转移,评估结果表明无死锁及不变式冲突;同时根据威胁模型模拟了 2 个具体的攻击场景,模型检测结果可有效检测出非法操作及违反的安全性质.本文第 1 节介绍用到的一些基础知识,包括 B 方法的基本语法和符号,以及可信执行环境相关架构知识.第2 节分析威胁模型,给出安全假设以及威胁模型的形式化定义.第 3 节提出基于内存标签的 TEE 访问控制模型框架.第 4 节描述构建的抽象机模型,包括模型结构和具体操作.第 5 节重点阐述模型添加的变量及操作,给出实例化模型.第 6 节利用模型检测进行安全性分析并展示检测结果.第 7 节讨论针对不同 TEE 方案如何实例化模型并给出未来工作展望.第 8 节讨论相关工作.第 9 节总结全文.1 预备知识 1.1 B 方法ZNB 方法18是一种面向模型的形式化方法,基于一阶逻辑和集合论基础,其提供的形式化语言称为 B 语言.该方法的基本思想是从一些已知的简单抽象数学对象出发,构造目标系统的状态特征和行为特征模型,其过程覆盖了从规范说明到代码生成的整个系统开发周期,完全证明后的形式化模型能够转换为实现的可执行代码.B 方法描述系统的基本单元是抽象机,每个抽象机从关键字 MACHINE 开始到 END 结束.关键字 CONSTANTS 声明常量,PROPERTIES 声明常量类型,VARIABLES 声明变量,INVARIANT 以逻辑公式的方式描述变量的不变式关系,INITIALISATION 声明所有变量的初始值,OPERATIONS 描述抽象机操作,包括输入、输出以及对抽象机状态的影响.由于 B 方法是基于集合论的,其支持的数据类型均为集合,如表示整数集合,表示自然数集合,INT 和 NAT分别表示系统可实现的整数集合和自然数集合,以及 BOOL 表示布尔类型,其基本符号如表 1 所示.同时,B 方法通过 INCLUDES,IMPORTS 以及 SEES 等连接来描述不同抽象机之间的关联,如 INCLUDESM1 表明该抽象机包含抽象机 M1,用于从简单的抽象机组合出更为复杂的抽象机;IMPORTSM1 表明该抽象机和抽象机 M1 的实例之间的关系,用于创建 M1 的一个具体实例并完全占用 M1 中的服务;SEESM1 表明该抽象机参考抽象机 M1实例,可以以只读的方式引用抽象机 M1 中的变量.支持 B 方法的形式化验证工具包括 AtelierB 和 ProB.AtelierB19是一个定理证明工具,在对构造的抽象机进行类型检查后,它自动生成证明义务并支持交互式定理证明.ProB20是一个约束求解器,支持对 B 方法构造的抽象机进行模型检测,同时可以将规约的状态空间图形化.由于 B 方法基于严格定义的数学概念和语言,保证了规范描述简明、精确和无歧义性,且开发工具较为成熟,目前已经应用于诸多重要安全攸关的领域如无人驾驶系统、交通调度等.1.2 可信执行环境可信执行环境(TEE)是一个隔离的区域,可以在其中加载需要保护的敏感代码和数据.它提供隔离的 CPU、内存和外设访问,以及隔离执行、机密性和完整性保护等基于硬件的安全功能.该隔离机制通常在逻辑上将执行环境划分为 TEE 和富执行环境(richexecutionenvironment,REE),分别称为安全世界(secureworld)和普通世界苗新亮等:可信执行环境访问控制建模与安全性分析3639(normalworld).安全世界中的程序可以访问普通世界中的资源,但反之则不行.ARMTrustZone 是目前最主流的 TEE 之一,广泛应用于嵌入式设备中以提供高效的系统级安全保护.TrustZone 将安全敏感的代码和数据存储在安全世界中,包括可信操作系统和可信应用(TA).普通世界中运行普通的操作系统和客户端应用(CA),它们只能访问普通世界中的资源.如图 1(a)所示,TrustZone 有 3 种处理器模式:安全世界、普通世界和用于在两个世界之间切换的监视器模式(monitormode).其中普通世界中运行 Linux、Android 等普通操作系统,安全世界中运行安全子系统或定制内核.此外,安全世界中的系统内核可以利用内存管理单元将安全世界内存空间划分成多个用户空间沙箱.只要安全内核是正确实现的,来自不同厂商的 TA 就可以在不需要互相信任的情况下安全地并发执行.TrustZone 通过 SMC 指令、IRQ、FIQ 或者异常进入 MonitorMode,实现不同世界的切换.表1B 符号N1非0自然数集合x 7 y(x,y)有序对S1S2(x,y)|x S1y S2 p(y,x)|x S1y S2(x,y)pdom(p)x|x S1y.(y S2(x,y)p)ran(p)dom(p)s p(x,y)|(x,y)px ssp(x,y)|(x,y)px ss t部分函数s t全函数SecurityserviceSecurityserviceStandaloneappSchedulerKernelMonitorSecure WorldappSecurityclientSchedulerTrustZonedriverKernelNormal WorldSecurityclientuserprivilegeduserprivilegedIRQFIQIRQFIQUntrustedOperating SystemTrusted HardwareTrustedInter-worldIPC manager App 1UserSupervisorMachineEnclave 1(a)ARMv7-A TrustZone architectureRT nApp nEnclave n(U-mode)(S-mode)(M-mode)Secure monitor(SM)(b)RISC-V keystone architecture RT 1Generic图1不同处理器架构下的 TEE 实现Keystone 是一个开源 TEE 框架,它利用物理内存保护(PMP)在 RISC-V 之上构建了一个高度可定制的 TEE.如图 1(b)所示,Keystone 使用了 RISC-V 提供的 3 种处理器模式:用户模式(U-mode)、监管者模式(S-mode)和机器模式(M-mode).用户应用程序运行在 U-mode,操作系统运行在 S-mode.安全监视器(SM)运行在 M-mode,可以直接访问物理资源(如中断、内存、外设等),它利用硬件原语为 TEE 提供安全保证.每个用户程序可以创建对应的安全区(enclave),在 enclave 中加载安全敏感的程序和数据.每个 enclave 都运行在隔离的物理内存区域中,并且有自己的运行时(RT).RT 运行在 S-mode,提供用于系统调用的接口、标准 libc 支持、enclave 内虚拟内存管理等功能.安全监视器还可以利用可配置硬件来提供增强的安全机制.2 威胁模型和安全假设介于普通世界中操作系统的高复杂度,假设攻击者可以通过系统漏洞实施内核攻击以获取该操作系统的所有3640软件学报2023 年第 34 卷第 8 期权(如图 2 所示),因此攻击者不仅可以任意读写普通应用程序内存、篡改应用程序调用的返回值,还可以利用系统安全功能创建恶意的安全区(enclave)来破坏其他良好的安全区,从而泄露、篡改敏感数据以及执行任意代码.本文假设安全世界中的内核、安全监视器(SM)以及硬件是可信的,同时加密原语是安全的.针对 TEE 的硬件攻击和侧信道攻击不在考虑范围内.EnclaveEnclaveSecure kernelNormal kernelprivilegedAppAppUserNormal worldSecure world图2敌手模型本文同时对访问控制系统模型和该系统的威胁模型形式化定义如下.S=P,P0,F,TP0 Pf Ff(p)T=(pi,f,pj)|f(pi)=pj,pi P,pj P,f F定义 1.访问控制系统.访问控制系统是一个四元组,其中,P 是系统状态集合,是初始状态集合,F 是操作集合,当时,表示状态 p 在执行操作 f 后到达的一个系统状态,表示状态迁移关系的集合.S=P,P0,F,T,=1,2,.,nS|=定义 2.访问控制系统威胁模型.访问控制系统威胁模型定义为一个五元组,为包含访问控制规则的安全约束集合且集合 T 中存在攻击转移行为 t使得访问控制系统不成立,即系统不满足安全约束,其中 t由执行威胁操作 f得到的状态迁移.3 基于内存标签的访问控制模型框架 3.1 模型整体框架访问控制模型中,请求者(主体)、被访问者(客体)以及权限操作是一个访问请求中必需的 3 个要素.访问控制执行模块以这 3 个要素作为输入,通过检查是否满足访问控制规则给出请求允许或拒绝操作.在此基础上,基于内存标签的访问控制将内存标签作为一个重要属性参与访问请求的判断过程.同时,内存标签通常可以进行更新操作以满足内存管理的灵活性.结合可信执行环境提供多域隔离的特点,如图 3 所示,本文提出的基于内存标签的访问控制模型主要有以下组成部分:标签域、主体、客体、权限操作、规则和访问控制执行模块.内存标签通过对内存字预留的比特位赋值来对该内存地址空间进行标记.由于 TEE 技术将运行环境隔离为非可信域(non-trusteddomains)和可信域(trusteddomains),同时 CPU 运行模式一般分为用户模式(usermode)和监管者模式(supervisormode).因此,TEE 实现的隔离域可分为 NU 域、NS 域、TU 域和 TS 域,分别代表不可信用户空间、不可信内核空间、可信用户空间和可信内核空间.本文提出的模型框架定义标签集合 TAG=NU,NS,TU,TS,这些利用标签进行标记的隔离域称为标签域.利用标签域,可分别描述主体和客体所在的执行空间.SUBSIDsubSA=sid,stag,exe_state,ac_statesid SIDstag TAGexe_state sub EXE_STATEac_state sub AC_STATEEXE_STATEAC_STATE定义 3.主体.主体作为发起访问的个体,可以是用户,也可以认为是进程、服务、程序等对象,主体有主体集合,同时有主体标识集合.每个主体有自己的标识以及标记主体所在隔离域的标签,这些组成主体属性.主体属性是一个四元组:,其中,和均为枚举集合,表示主体的执行状态和访问状态.主体的唯一性通过主体标识属性和主体标签属性确定.同时,在可信执行环境中,隔离域可通过定义的系统调用、中断、异常以及特殊指令等方式实现域间的切换.因此,主体标签属性在执行相关域切换操作后可动态修改.定义 4.客体.客体是被请求访问的资源,在基于内存标签的访问控制模型框架中,客体认为是内存资源,客体苗新亮等:可信执行环境访问控制建模与安全性分析3641OBJOIDOA=oid,otag,statusoid OIDotag TAGstatus Status OIDStatus有客体集合,也有客体标识集合.通过客体标识以及客体所在的标签域,保证每个客体的唯一性.客体属性是一个三元组:,其中,是自然数集合,是一个枚举集合,表明该客体资源是否可用.内存标签通常支持动态更新以提高内存管理的灵活性.标签更新操作在以主体属性、客体属性为参数的更新规则下执行.同时在访问控制过程中,客体的可用状态是影响访问结果的重要因素,当客体正在被访问时,其资源状态应改为不可用以防止冲突,同时在访问结束后,其状态更改为可用以备其他主体访问.定义 5.权限操作.权限操作是定义主体行为一类对象,定义主体对客体执行访问操作的类型.用 OP 表示权限操作集合,为突出模型的通用性,该集合中仅定义读(Read)、写(Write)和执行(Exc)操作,表示为 OP=Read,Write,Exc.其他操作可在实例验证过程中根据真实环境进行添加.标签域标签更新访问控制执行模块主体属性客体属性域切换非可信域Non-trusted domains可信域Trusted domains用户模式User mode监管者模式Supervisor modeNUNSTUTS主体客体规则权限操作访问控制规则标签更新规则(SA)(OA)(OP)图3MTF:基于内存标签的 TEE 访问控制模型框架 3.2 规则定义访问控制执行模块的一个核心是检查主体对客体的访问是否满足访问控制规则.该模型框架中基于内存标签的访问控制规则如表 2 所示.依据定义 5 简写权限给出访问控制规则,其中 r 表示读(Read)、w 表示写(Write)、x 表示执行(Exc).当主体和客体在同一个标签域时,主体对客体具有操作的所有权.为提高内存保护,管理模式执行保护(SMEP)技术广泛应用于处理器中以禁止内核执行用户空间的代码,因此模型中其他标签域对 NU 域和TU 域的访问仅限于读写操作.标签更新操作用于更改客体资源所处的标签域,比如在一个非可信用户空间创建一个隔离空间来保护敏感数据和代码时,则该隔离空间从 NU 更新为 TU,当执行完毕并销毁该空间后,其标签重新标记为 NU.如表 3 所示,标签仅允许在同等或低于本身安全等级的标签域中更新以防止权限提升.表2访问控制规则NUNSTUTSNUrwxNSrw-rwxTUrw-rw-rwxTSrw-rw-rw-rwx表3标签更新规则NUNSTUTSNUNSTUTS3642软件学报2023 年第 34 卷第 8 期 3.3 状态迁移分析操作系统访问控制过程中,访问操作的执行状态记录主体执行访问时所处的状态,该状态是影响访问请求能否响应的关键因素之一.同时访问控制执行模块在响应过程中会产生对应的访问状态.访问状态是对访问执行过程中各个阶段的抽象,并最终反馈访问控制执行结果,是模型中必要的状态描述.因此,该模型框架抽象定义主体访问客体过程中的执行状态(EXE_STATE)和访问状态(AC_STATE)并附加为主体属性.执行状态包括为就绪(Ready)、运行(Run)、阻塞(Blocked)和最终状态(Final).Ready 状态是主体在创建后就进入的状态,此时主体准备或正在发起访问请求;Run 状态表示当前主体正在访问客体资源;Blocked 状态表示被请求的客体资源由于被占用而当前不可用,访问执行操作被阻塞;Final 状态表示访问操作结束.访问状态包括访问前(Pre)、访问中(Acing)、访问等待(Wait)以及访问结束(Post).在初始化时,执行状态初始化为 Ready,访问状态初始化为 Pre.模型框架中执行状态和访问状态的迁移关系如图 4 所示.ReadyRunBlockedFinalPreAcingWaitPost(a)(b)图4访问控制模型执行状态和访问状态迁移关系图主体创建后进入的状态,准备或正在发起访问请求,执行状态和访问状态保持不变;主体请求访问客体,客体资源可用,且访问请求满足访问控制策略,则执行状态进入 Run 状态,且访问状态进入 Acing 状态;主体请求访问客体,访问请求满足访问控制策略但客体资源不可用,则执行状态进入 Blocked 状态,访问状态进入 Wait 状态;主体请求访问客体,访问请求未满足访问控制策略,则执行状态变为 Final,且访问状态变为 Post,表示访问操作结束;在访问过程中,主体访问其他客体资源,访问操作满足访问控制策略且客体资源此时可用,则执行状态和访问状态均保持不变;在访问过程中,主体访问其他客体资源,满足访问控制策略但被访问资源不可用,则执行状态进入 Blocked状态,访问状态进入 Wait 状态;主体访问的客体资源一直处于不可用状态,则执行状态和访问状态保持不变;主体等到被访问的客体资源可用,则执行状态进入 Run 状态,同时访问状态进入 Acing 状态;在访问过程中,主体对其他客体资源的访问请求不满足访问控制策略,或者无其他客体资源需要访问,则执行状态变为 Final,访问状态变为 Post,表示访问结束.3.4 基本操作和性质描述访问控制模型通过定义各个实体操作以描述系统访问控制过程中的具体行为.对于主体实体,除了定义主体的创建和删除操作,还应结合可信执行环境定义主体标签域切换操作.为提高模型的通用性,这些操作不做任何安苗新亮等:可信执行环境访问控制建模与安全性分析3643全判断,仅为执行模块提供操作接口,安全判断在执行模块中实施.同理,客体实体中除了定义客体资源的初始化、创建、删除操作,也定义了客体资源状态的更改操作以及客体标签更新操作.规则实体中除了定义权限操作类型,同时根据主客体的标签属性创建了访问控制策略集合和标签更新策略集合.为提高系统安全性,访问控制规则和标签更新规则往往不允许进行任何修改,因此该实体没有规则的添加、删除和修改操作.在对真实系统进行验证时,依据系统策略文件描述这些规则即可.访问控制执行模块描述系统执行访问控制操作的整个过程,首先应该对系统环境进行初始化.当处理访问请求时,先判断请求是否满足访问控制策略,如果满足,则根据客体资源可用状态实施相应的操作,并对主体的执行状态和访问状态进行更改.此外,执行模块还应描述系统运行过程中由于系统调用和中断等事件导致的标签域切换操作以及标签更新操作.通过这些基本操作,实现对系统访问过程中状态迁移的描述.访问控制执行模块在执行实体操作进行状态转移的过程中应始终满足一些安全性质.如:(1)非可信域中的主体只能访问非可信域中的客体;(2)可信域中的主体可以访问非可信域中的客体;(3)可信域中的主体只能访问与之匹配的客体;(4)主体只能访问处于可用状态下的客体;(5)主体只有在运行状态时才可以访问客体等.这些安全性质是整个运行过程中都要满足的.通过检测这些性质的满足性,可实现对模型功能正确性和安全性分析.4 抽象机建模 4.1 模型基本结构模型框架描述了各个组成部分的基本定义和主要功能,在此基础上,本文采用 B 方法以抽象机方式对该框架进行建模.构造的抽象机模型包括标签抽象机 Tag、主体抽象机 Sub、客体抽象机 Obj、策略抽象机 Policy 和访问控制抽象机 MTAC.抽象机中的关键变量和抽象机间的结构关系如图 5 所示.MTACready_subsub_objsub_ac_objac_ policy_ flagPolicyac_ policyup_ policy.ObjobjoidotagstatusSubsubsidstag.INCLUDESINCLUDESINCLUDESTagTAGSEESSEESSEES图5B 方法构建的访问控制模型结构标签抽象机 Tag 描述 TEE 中的标签域集合,标签抽象机 Sub 描述访问请求的主体,包括主体属性和主体基本操作,同理,抽象机 Obj 描述访问请求的客体.抽象机 Policy 利用主客体标签属性描述了基于标签的访问控制规则和标签更新规则.抽象机 Sub、Obj 和 Policy 都需要引用抽象机 Tag 中定义的集合,因此与抽象机 Tag 是 SEES 关系.访问控制模型 MTAC 包含(INCLUDES)Sub、Obj 和 Policy 这 3 个抽象机,通过调用基本实体抽象机中的变量和操作形式化描述了环境初始化、隔离域切换、访问执行等具体行为.4.2 基本实体抽象机基本实体抽象机描述各实体组件,定义基本的实体属性以及可调用的实体操作.在构建的访问控制 B 模型中,3644软件学报2023 年第 34 卷第 8 期TAG=NU,NS,TU,TS基本实体抽象机包括 Tag 抽象机、Sub 抽象机、Obj 抽象机和 Policy 抽象机,分别描述标签域、主体、客体和策略实体对象.其中,Tag 抽象机根据框架中描述的隔离域定义标签域集合,该抽象机极为简单,这里不再赘述,接下来对其他 3 个抽象机模型详细阐述.sidstagexe_stateac_stateCreate_SubDelete_SubChange_Sub_StateChange_Sub_Tag抽象机 Sub 首先定义了主体集合(SUB)以声明所有的主体,然后描述主体属性以及基本操作(如表 4 所示).其中,主体属性包括主体标识()、主体标签()、执行状态()和访问状态(),主体操作包括创建()、终止()、状态切换()和标签转移().表4主体抽象机抽象机主体(Sub)SEESTagSETSSUBEXE_STATE=Ready,Run,Blocked,FinalAC_STATE=Pre,Acing,Wait,Post,VARIABLESsubSIDsidstag exe_stateac_state,INVARIANTsub SUBSID N1sid sub SIDstag sub TAGexe_state sub EXE_STATEac_state sub AC_STATEOPERATIONSCreate_SubDelete_SubChange_Sub_StateChange_Sub_Tag,Create_SubDelete_SubChange_Sub_StateChange_Sub_Tag操作创建新的主体并赋值主体属性,其执行状态和访问状态分别为 Ready 和 Pre.操作将该主体从主体集合 SUB 中删除,其映射的属性也随之删除.操作根据传入的状态参数更改指定主体的执行状态和访问状态,为访问控制模型抽象机提供操作接口.同理,操作更改指定主体所在的标签域并提供操作接口.oidotagstatusInit_ObjAdd_ObjDel_ObjChange_Obj_StatusUpdate_Obj_Tag抽象机 Obj 定义客体集合(OBJ)以声明所有的客体资源,如表 5 所示.在访问控制过程中,涉及的客体属性包括客体标识符()、客体标签()和客体资源可用状态().对客体资源的操作包括定义初始客体资源()、添加客体资源()、删除客体资源()、更改客体资源可用状态()以及客体标签更新操作().表5客体抽象机抽象机客体(Obj)SEESTagSETSOBJSTATUS=Free,Full,VARIABLESobjoidotagstatus,INVARIANTobj OBJoid obj N1otag obj TAGstatus obj STATUSOPERATIONSInit_ObjAdd_ObjDel_ObjChange_Obj_Status Update_Obj_Tag,FreeFullFreeFullInit_ObjAdd_ObjDel_ObjChange_Obj_StatusUpdate_Obj_Tag客体资源可用状态包括状态和状态,当该内存资源未被占用时,其状态为,反之,状态为.操作描述了系统初始化时的客体资源,模型默认此时的客体资源包括 NU 标签、NS 标签、TU 标签和TS 标签下的资源.操作添加客体资源并赋值客体属性,操作删除指定的客体资源.操作根据传入的状态参数更改客体资源可用状态,为访问控制模型抽象机提供操作接口.同理,执行对指定客体资源的标签更新操作.Create_Ac_PolicyTS 7 TU 7 Read抽象机 Policy 描述主体对客体的访问控制规则以及标签更新规则,通过 SEES 关系对抽象机 Tag 中的集合和变量以只读的方式引用(如表 6 所示).在定义权限操作集合 OP 时,除了框架中描述的读、写、执行操作,还定义Nop 操作,表示主体完成