基于精化的TrustZone多安全分区建模与形式化验证.pdf

软件学报 ISSN 1000-9825,CODEN RUXUEW E-mail: Journal of Software,2023,34(8):35073526 doi:10.13328/ki.jos.006866 http:/ 中国科学院软件研究所版权所有.Tel:[phone] 基于精化的 TrustZone 多安全分区建模与形式化验证 曾凡浪1,2,常 瑞1,3,许 浩1,2,潘少平1,2,赵永望1,3 1(浙江大学 计算机科学与技术学院,浙江 杭州 310027)2(浙江大学 杭州国际科创中心,浙江 杭州 311200)3(浙江省区块链与网络空间治理重点实验室,浙江 杭州 310027)通信作者:常瑞,E-mail: 摘 要:TrustZone 作为 ARM 处理器上的可信执行环境技术,为设备上安全敏感的程序和数据提供一个隔离的独立执行环境.然而,可信操作系统与所有可信应用运行在同一个可信环境中,任意组件上的漏洞被利用都会波及系统中的其他组件.虽然ARM提出了S-EL2虚拟化技术,支持在安全世界建立多个隔离分区来缓解这个问题,但实际分区管理器中仍可能存在分区间信息泄漏等安全威胁.当前的分区管理器设计及实现缺乏严格的数学证明来保证隔离分区的安全性.详细研究了ARM TrustZone多隔离分区架构,提出一种基于精化的TrustZone多安全分区建模与安全性分析方法,并基于定理证明器 Isabelle/HOL 完成了分区管理器的建模和形式化验证.首先,基于逐层精化的方法构建了多安全分区模型 RMTEE,使用抽象状态机描述系统运行过程和安全策略要求,建立多安全分区的抽象模型并实例化实现分区管理器的具体模型,遵循FF-A规范在具体模型中实现了事件规约;其次,针对现有分区管理器设计无法满足信息流安全性验证的不足,设计了基于 DAC 的分区间通信访问控制,并将其应用到 TrustZone 安全分区管理器的建模与验证中;再次,证明了具体模型对抽象模型精化的正确性以及具体模型中事件规约的正确性和安全性,从而完成模型所述 137 个定义和 201 个定理的形式化证明(超过 11 000 行 Isabelle/HOL 代码).结果表明:该模型满足机密性和完整性,并可有效防御分区的恶意攻击.关键词:可信执行环境;安全分区;定理证明;精化;安全性分析 中图法分类号:TP311 中文引用格式:曾凡浪,常瑞,许浩,潘少平,赵永望.基于精化的 TrustZone 多安全分区建模与形式化验证.软件学报,2023,34(8):35073526.http:/ 英文引用格式:Zeng FL,Chang R,Xu H,Pan SP,Zhao YW.Refinement-based Modeling and Formal Verification for Multiple Secure Partitions of TrustZone.Ruan Jian Xue Bao/Journal of Software,2023,34(8):35073526(in Chinese).http:/ Refinement-based Modeling and Formal Verification for Multiple Secure Partitions of TrustZone ZENG Fan-Lang1,2,CHANG Rui1,3,XU Hao1,2,PAN Shao-Ping1,2,ZHAO Yong-Wang1,3 1(College of Computer Science and Technology,Zhejiang University,Hangzhou 310027,China)2(ZJU-Hangzhou Global Scientific and Technological Innovation Center,Hangzhou 311200,China)3(Key Laboratory of Blockchain and Cyberspace Governance of Zhejiang Province,Zhejiang University,Hangzhou 310027,China)Abstract:As a trusted execution environment technology on ARM processor,TrustZone provides an isolated and independent execution environment for security sensitive programs and data on the device.However,making trusted OS and all trusted applications run in the 基金项目:浙江省重点研发计划(2022C01165);国家自然科学基金(62132014);浙江省尖兵计划(2022C01045);中央高校基本 科研业务费(NGICS)专项资金 本文由“约束求解与定理证明”专题特约编辑蔡少伟研究员、陈振邦教授、王戟研究员、詹博华副研究员、赵永望教授推荐.收稿时间:2022-09-04;修改时间:2022-10-13;采用时间:2022-12-14;jos 在线出版时间:2022-12-30 3508 软件学报 2023 年第 34 卷第 8 期 same trusted environment may cause problemsthe exploitation of vulnerabilities on any component will affect the others in the system.Although ARM proposed S-EL2 virtualization technology,which supports multiple isolated partitions in the security world to alleviate this problem,there may still be security threats such as information leakage between partitions in the actual partition manager.Current secure partition manager designs and implementations lack rigorous mathematical proofs to guarantee the security of isolated partitions.This study analyzes the multiple secure partitions architecture of ARM TrustZone in detail,proposes a refinement-based modeling and security analysis method for multiple secure partitions of TrustZone,and completes the modeling and formal verification of the secure partition manager based on the theorem prover Isabelle/HOL.First,a multiple security partitions model named RMTEE is built based on refinement,an abstract state machine is used to describe the system running process and security policy requirements,and the abstract model of multiple secure partitions is established and instantiated.Then the concrete model of the secure partition manager is implemented,in which the event specification is implemented following the FF-A specification.Secondly,in view of the problem that the existing partition manager design cannot meet the goal of information flow security verification,a DAC-based inter-partition communication access control is designed and applied to the modeling and verification of TrustZone security partition manager.Finally,the correctness of the concrete models refinement of the abstract model and the correctness and security of the event specification in the concrete model are proved,thus completing the formal proof of 137 definitions and 201 lemmas in the model(more than 11 000 lines of Isabelle/HOL code).The results show that the model satisfies confidentiality and integrity,and can effectively defend against malicious attacks of partitions.Key words:trusted execution environment;security partition;theorem proving;refinement;security analysis 随着计算设备广泛应用和种类的多样化,计算系统变得愈发复杂,给病毒软件和恶意攻击提供了更大的利用空间.软件提供商和用户需要可靠的防御机制来保护自己的代码和数据的安全.基于 ARM TrustZone1实现的可信执行环境2利用硬件隔离机制为代码和数据提供有效防护.然而,在实际应用中,基于 TrustZone的隔离机制也暴露了一些不足.Pinto 等人3,4分析了主流的商用 TrustZone 系统中存在的安全问题,在安全监视器、可信操作系统和可信应用中发现了数量可观的漏洞和错误.最新的 CVE 漏洞也持续披露了 TrustZone中存在的问题,比如:CVE-2021-343895发现,英伟达 TEE 的 TA 中不正确的边界检查导致本地用户可以通过恶意客户端访问 TrustZone 中的堆内存;CVE-2021-441496发现,OPTEE-OS 的 CSU 驱动中的漏洞导致普通世界可以绕过 TrustZone 任意读写安全世界内存.ARM 为了缓解上述问题,在 v8.4 新架构中提出了 S-EL2 虚拟化架构7及 FF-A(firmware framework for arm a-profile)8分区管理器 ABI 接口规范,将安全世界划分为多个隔离分区(secure partition,SP),不同的Trusted OS 和 TA 运行在不同的分区中,并由更高特权级别的分区管理器(secure partition manager,SPM)来管理,系统 TCB 为分区管理器和安全监视器.分区管理器还提供分区间的消息通信接口,以支持分区间的功能调用和数据传输.然而,该架构设计缺乏严格的数学证明保证其设计与实现的一致性,仍存在非法内存访问和恶意接口调用等安全威胁,具体表现为:(1)分区管理器是保证分区安全隔离的关键组件,如果其实现不当,有可能会被恶意程序利用,从而导致系统级的安全风险.比如:CVE-2021-302789发现,高通 TrustZone 中内存转让接口的输入验证不当,可能导致多款系统程序的信息泄露;(2)在 ARM 的多分区系统设计中,分区间可以任意通信,意味着信息在分区间是任意流动的,分区隔离也就失去了意义,无法满足信息流安全形式化验证的要求.为了解决上述问题,本文提出一种基于精化的 TrustZone 多安全分区建模和验证方法,构建了 TrustZone多安全分区模型 RMTEE(refinement-based multiple secure partitions trusted execution environment),并在Isabelle/HOL 定理证明器中,以机器可检查的方式证明了其功能正确性和信息流安全性.本文借鉴程序开发中的精化方法10,在形式化模型中使用精化演算11,从抽象的高层描述出发,对系统功能和数据逐步增加细节,每一步精化都得到一个更贴近底层实现的规约,逐步得到底层规约.同时,为实现安全的分区间通信,本文提出了基于自主访问控制(discretionary access control,DAC)的分区间通信访问控制,在系统配置中定义分区间通信访问控制矩阵(access control matrix,ACM),并在接口调用时查询访问控制矩阵,验证调用的合法性,曾凡浪 等:基于精化的 TrustZone 多安全分区建模与形式化验证 3509 确保系统满足信息流安全要求.本文的主要贡献如下:(1)提出一种基于精化的 TrustZone 多安全分区形式化建模方法.本文构建了 TrustZone 多安全分区模型RMTEE,该模型包含抽象模型和具体模型:抽象模型由抽象参数状态机和安全属性组成,具体模型包括执行模型和事件规约.执行模型使用具体变量和函数实例化了抽象模型,事件规约依据 ARM FF-A 规范所描述的分区管理器标准实现了具体事件接口.RMTEE 模型包含 137 个定义,1 462 LOC的 Isabelle/HOL 代码;(2)设计了分区间调用安全增强机制.通过形式化验证,发现了 FF-A规范中存在的信息流安全隐患,针对该不足设计了分区间调用自主访问控制安全增强机制,应用到模型开发和验证中,并分析了该机制可以抵御的两种攻击类型;(3)验证了 RMTEE 模型的正确性和安全性.使用定理证明方法验证 RMTEE 抽象模型与具体模型间的精化关系及具体模型中事件接口的正确性和信息流安全性.证明工作使用了 201 个定理,9 715 LOC的 Isar 代码.结果表明,RMTEE 模型符合机密性和完整性.本文第 1 节介绍与本工作研究内容相关的工作.第 2 节分析威胁模型及安全假设.第 3 节提出本工作的形式化建模和验证方法.第 46 节描述系统建模和安全属性验证过程,分别阐述抽象模型、具体模型规约和具体模型证明.第 7 节对本工作进行安全性分析和评估.第 8 节总结全文.1 研究现状 1.1 TrustZone多安全区隔离 学术界和工业界已经有一些工作利用 TrustZone 的隔离特性建立安全分区.在有些工作中,分区也称为虚拟机(VM).TZ-RKP12将 Hypervisor 运行在安全世界来提供高特权级别和隔离,它在运行时拦截并检查来自普通世界的系统调用,防止目标系统运行未授权的特权代码.TEEv13设计了一种在安全世界内运行多个 VM 的方法,由于安全世界没有专门用于运行 Hypervisor 的特权级别,它将专门实现的 Hypervisor 与 VM 运行在相同的特权级别 S-EL1.为了保证 Hypervisor 的高特权以管理 VM,需要修改 VM 内核,限制其对某些特权指令的访问.此前的工作由于没有硬件支持,都需要通过扫描二进制文件或软件拦截的方式来检查或修改 VM 指令,带来实现和运行的开销.ReZone14利用现有 ARM 平台上的辅助硬件设计了一种安全架构,将安全世界划分为隔离分区,并且由硬件保障的内存访问控制限制分区对其他分区以及普通世界的访问权限,以此来削减S-EL1 的非必要特权,进而缓解 S-EL1 被劫持所引发的系统级威胁.ARMv8.4 架构引入了 S-EL2 硬件隔离机制7,在安全世界隔离出多个分区,使得单个分区出现安全漏洞被利用后产生的影响范围更小.TwinVisor15利用 S-EL2 扩展实现了安全世界内的隔离分区,但它的设计与 ARMv8.4 标准有所不同,它在安全世界内运行一个实现简单的 Hypervisor 来保证 VM 的安全性,而复用普通世界的 Hypervisor 来管理硬件资源.TwinVisor设计了一些方案来支持安全世界 Hypervisor 和普通世界 Hypervisor 协同管理 VM 资源以及减少系统开销,但是它没有像 ARM 标准设计那样提供 VM 之间的通信机制.表 1 比较了不同 TrustZone 多分区隔离机制之间的区别.表 1 TrustZone 多安全区机制比较 多分区隔离机制 硬件支持无系统修改 分区间通信性能开销 TZ-RKP 运行时拦截并检查分区指令,开销高 TEEv 纯软件方案,开销高 ReZone 安全分区运行时,处理器其他核心空转,开销高 TwinVisor 需要两个世界的 Hypervisor 协作,开销中等 ARM S-EL2 硬件支持的虚拟化,开销低 ARMv9 提出了机密计算架构(confidential compute architecture,CCA)1618,增强了 ARM 对机密计算的支持,以应对大型计算密集型任务.CCA 基于硬件 RME(realm management extension)扩展和软件 RMM(realm 3510 软件学报 2023 年第 34 卷第 8 期 management monitor).CCA 在 TrustZone 的安全基础之上构建了 realm 的概念,realm 是由 RMM 管理的可以动态创建的安全分区.此外,RME 支持向安全世界动态分配和回收物理内存.由于 ARM 尚未公布 CCA 的细节规范,其实际落地商用还需要一段时间.1.2 分区隔离系统的形式化验证 在分区隔离系统的形式化验证领域存在着数量可观的成果.seL4 项目19针对一种高性能操作系统微内核展开了全面的形式化验证.seL4 是世界上第一个经过形式化验证的操作系统内核,而且仍然是唯一经过验证的具有细粒度的基于能力的高安全性和高性能操作系统.该项工作成功地使用逐层精化的建模方法,为后来的大量形式化验证工作提供了借鉴意义,也是本工作所用方法的来源之一.耶鲁大学邵中团队主持的CertiKOS 项目20验证了一个运行在多核处理器上的操作系统.传统操作系统内核中,各个部分互相联结,一个漏洞就会影响整个操作系统的安全,难以设计和验证.该团队创新性地提出以抽象层为基础的组合规约,在提高可扩展性的同时,解决了并发内核难以验证的难题.Zhao 等人21,22在 Isabelle/HOL 中实现了一个符合ARINC 653 隔离内核的顶层规范,对 ARINC 653 的分区管理、分区调度和通信服务形式化建模,并验证了ARINC 653 隔离内核的一个工业实现和两个开源实现,发现了 ARINC 653 标准及其实现中存在的 6 个可能导致信息泄露的安全缺陷.本文的建模和验证主要参考了此项工作的框架.SeKVM23,24首次对商用 Hypervisor KVM 进行了形式化验证,它将 KVM 拆分为一个核心部分和一组不可信服务,使用 Coq 通过逐层求精的方法证明了 KVM 核心的机密性和完整性,并使用 Rely-Guarantee 框架证明了其并发安全性,此方法为我们后续工作对 TrustZone 多分区系统并发安全的验证提供了一个参考方案.大多数分区内核的形式化验证的研究工作的目标都是证明数据隔离和信息流安全,采用定理证明和精化的方法.1.3 TEE的形式化验证 目前,针对可信执行环境安全隔离证明的工作较少.Jin等人25,26针对TrustZone提出了一种基于精化的内存隔离机制安全性验证方法,用于对内存隔离机制进行细粒度的形式化验证.该模型建模了 TrustZone 内存隔离机制的关键硬件和软件,包括地址空间控制器、MMU、TLB 和安全监视器等,在定理证明器 Isabelle/HOL中验证了该模型满足无干扰、无泄露、无影响等信息流安全属性.该项工作主要聚焦在验证传统 TrustZone架构下,普通世界与安全世界之间的隔离;而本文工作验证了 ARMv8.4 及其之后的新架构中,安全世界内多分区间的隔离和安全通信.Miao 等人27对利用内存标签技术在可信执行环境中实现的细粒度的内存隔离和访问控制机制提出了通用的形式化模型框架,并提出了一种基于模型检测的访问控制安全性分析方法,利用形式化语言 B,设计并实现了该框架的抽象机模型,并验证了可信执行环境中访问控制机制的正确性和安全性.此工作所针对的 RISC-V 平台的 TIMBER-V 所采用的内存标签隔离技术与本文所验证的 ARM S-EL2 隔离机制存在较大差异,其使用的模型检查方法也与本文的定理证明方法不同.在本文之前,还没有针对 TrustZone安全世界内多隔离分区的形式化建模和验证工作.2 威胁模型与假设 本文针对安全世界内的分区隔离,不考虑普通世界与安全世界间的隔离.由于安全世界内的 TA 和 OS 中存在为数不少的漏洞,它们有可能被恶意用户利用,从而成为恶意程序.因此,不信任安全世界内的分区,如图 1 所示.分区对自身的漏洞负责,形式化验证的分区管理器确保对分区所提供接口中不存在可被利用的漏洞,保证分区的私有数据不会被其他恶意分区窃取或篡改.本文不考虑侧信道攻击和复杂的物理攻击.此外,本工作对 TrustZone 多分区系统的验证基于以下假设.(1)硬件和安全监视器是可信的;(2)保存在持久化存储中的分区和分区管理器的镜像未被篡改(通过安全启动验证其完整性).攻击者通过读写任意内存地址以及发起恶意的分区间调用,达到窃取、篡改其他分区的敏感数据的目的.本文对系统威胁模型的形式化定义如下.曾凡浪 等:基于精化的 TrustZone 多安全分区建模与形式化验证 3511 定义 1(威胁模型).T=S,E,其中,S 是系统状态集合;E是敌手事件集合,E=mem_read,mem_write,ipc_call,mem_read表示内存读操作,mem_write表示内存写操作,ipc_call 表示分区间调用,且 E 中包含的事件均不符合系统安全约束,即:eE,(emem_read(s,mem,p),mem_write(s,mem,p)mem.ownerp)(eipc_call(s,p1,p2)(p1,p2,ipc_call)ipc_acm).s 表示系统状态,mem 表示一块内存,p 表示一个分区,mem_read(s,mem,p)表示分区 p 在状态 s 下读取某块内存 mem,而 mem.ownerp 表示分区 p 不是内存 mem 的所有者.ipc_call(s,p1,p2)表示在状态 s下,分区 p1向分区 p2发起接口调用,ipc_acm 是分区间调用访问控制矩阵,(p1,p2,ipc_call)ipc_acm表示访问控制配置不允许分区 p1向分区 p2发起分区间调用.安全世界普通世界操作系统内核可信操作系统分区EL0EL1EL2EL3可信应用用户程序分区可信应用安全监视器ATF分区管理器 图 1 TrustZone 多分区架构的攻击面 3 整体验证思路 由于分区系统信息流安全的自动分析受到状态空间大小的限制,使用模型检测方法来进行安全分析比较困难,因此,本工作使用基于定理证明的方法.本工作选择 Isabelle/HOL 定理证明器,Isabelle 中简单而强大的函数式语言提供了形式规约所需的形式规约语言,数学计算、数学定理证明及计算机软硬件系统都可以通过这种函数式语言来描述和实现,并且 Isabelle 内置的逻辑系统也为形式规约所需要的形式验证提供了严格推理和证明的能力.而 Isabelle/HOL 的高表达性、高度的证明自动化、强大的库等,使它可以用于真实世界商用系统的大规模形式化验证.此外,大多数分区系统使用 Isabelle/HOL 的成功验证案例,比如 seL4 和 PikeOS,这也是支撑本工作使用 Isabelle/HOL 的一个因素.图 2 所示是本文的建模和验证框架.首先定义 TrustZone 分区系统的安全资产和安全策略,抽象出分区间的干扰性,基于干扰性定义信息流安全属性,即机密性和完整性.使用参数化抽象的状态机来描述抽象模型,状态机中的定义的状态参数和函数都使用抽象类型,与系统具体实现无关.然后,将抽象模型实例化为一个具体模型,得到具体模型规约.通过这种方式,抽象模型中定义的属性、约束和安全性质都可在具体模型中保留和重用.具体模型规约分为两个部分:执行模型和事件规约.执行模型是抽象模型的实例,事件规约定义了 ARM FF-A 规范所定义的分区生命周期管理接口、分区间通信接口以及维护分区间隔离所需的内存管理接 3512 软件学报 2023 年第 34 卷第 8 期 口.事件规约中的具体接口会被执行模型调用.接着证明具体模型对抽象模型的精化关系及具体模型中所有事件接口的正确性,并且事件接口都满足抽象模型中定义的安全属性.最后对任意地址映射和未授权分区间通信这两种攻击行为建模,验证模型能够防御分区的攻击行为.4 RMTEE抽象模型5 RMTEE具体模型规约6 RMTEE 具体模型证明4.1 抽象状态机6.3 安全属性证明7 分析与评估模拟攻击分区安全策略定义6.1 实例化证明6.2 正确性证明4.2 安全属性机密性完整性证明任意地址映射未授权分区间通信评估实例化阶段二页表映射分区间隔离分区生命周期管理IPC访问控制矩阵分区间安全通信ARM FF-A Spec实现 图 2 基于精化 TrustZone 多安全分区建模与验证 4 RMTEE 抽象模型 本节定义 RMTEE 抽象模型,它由状态机、安全属性以及安全属性的推导关系组成.在状态机模型中,状态变量表示系统的状态,转移函数和辅助函数用以描述状态变量的变化过程.状态转移函数是系统对外暴露接口的抽象,它们描述了系统状态如何变化.安全属性是系统安全需求的形式化描述,在形式化的安全模型中,最为关键的部分就是安全性证明,它的核心证明为对安全属性的可满足性证明.抽象模型使用 Isabelle 的locale 关键字定义,其中的参数都是抽象类型,而不涉及具体的数据结构和函数实现,以便聚焦于系统性质的描述,这些抽象参数在具体模型中被精化为具体实现.4.1 抽象状态机 本文使用基于状态-事件的抽象状态机来描述系统模型,系统状态机模型包含确定模型的要素(变量、函数、操作规则等)、安全初始状态与安全策略.系统状态机是一个由抽象数据类型组成的元组,定义如下.定义 2(系统状态机).M=S,D,E,?,D,s0,SPM,其中,S表示系统所有状态的集合;D表示所有安全域的集合.每个分区是一个安全域,分区管理器也是一个安全域;E表示系统有限的事件集合.事件是系统接口的抽象,由于系统提供确定数量的接口,因此,事件集 合是有限的;是状态转移函数,(e)SS,表示系统在一个状态下执行单个事件 e 后到达一个新的状态;?表示安全域间的干扰关系,?DD,d1?d2表示允许信息从分区 d1流向分区 d2.不可干扰记为?;表示状态等价,两个状态 s 和 t 对于一个安全域 d 等价记为 sdt,意味着在状态 s 和状态 t 下,安全域 d 的私有数据完全相同.在一些文献中,等价(equivalence)也表述为不可区分(indistinguishable),即分区无法区分两个状态;曾凡浪 等:基于精化的 TrustZone 多安全分区建模与形式化验证 3513 D表示事件的执行域.事件是由分区发起接口调用产生的,在状态 s 下产生的事件 e 关联一个执行分区,记为D(s,e)D;s0表示系统初始状态,s0S;SPM 表示分区管理器,SPMD,区别于普通分区,拥有最高权限.分区的干扰关系描述了系统所允许的信息流向,表示授予后一个分区对前一个分区的数据读权限以及前一个分区对后一个分区的数据写权限.干扰关系和状态等价是描述系统状态变化特征的基础,基于它们的定义和系统安全策略,定义以下 6 条安全策略规约.(1)s,d,(sds);(2)s,t,d,(sdt)(tds);(3)s,t,r,d,(sdt)(tdr)(sdr);(4)dD,(d?d);(5)dD,(SPM?d);(6)dD,(d?SPM)d=SPM.前 3 条规约分别描述了状态等价的自反性、对称性和传递性,后 3 条规约描述了系统安全策略,即分区间信息流动的规则:分区可以干扰自身;分区管理器可干扰任意分区;普通分区不能干扰分区管理器.由于分区管理器拥有最高权限,因此允许分区管理器向任意分区的信息流动.4.2 安全属性 本文在状态机模型的基础上定义系统安全属性.此前,已有工作使用无干扰(noninterference)和无泄漏(nonleakage)来定义信息流安全性.无干扰28是指系统中不能干扰分区 d 的那些分区所产生的事件不会影响分区 d 的状态.无泄漏29的含义是在执行事件的过程中不向其他分区传递期望外的信息.文献29证明了无干扰和无泄漏的结合等价于无影响(noninfluence)属性.文献22对这些安全属性进行了扩展,并推导论证了所有这些属性之间的蕴含关系,然后证明了基于一组解旋条件可以推导出系统的无影响属性.本文遵循文献22的推理框架,在抽象模型中定义系统的机密性和完整性来描述信息流安全属性.定义 3(事件的机密性).confidentiality(e)d,s,t,s,t,(sdt)(D(s,e)=D(t,e)(D(s,e)?d)(sD(s,e)t)(s,s)(e)(t,t)(e)(sdt)机密性保证不存在未预期的信息泄漏.分区调用系统接口向其他分区发起分区间通信,产生分区间的信息流动.机密性定义要求在任意两个状态 s 和 t 下,执行同个事件后,对于其他分区产生的影响是相同的,即向其他分区传递的信息相同,从而保证分区没有泄露期望外的信息.如果事件执行时依据其他分区的数据产生不同的结果,就会导致结果状态 s和 t不等价,这样就泄漏了其他分区的数据.定义 4(事件的完整性).integrity(e)d,s,s,(D(s,e)?d)(s,s)(e)(sds)完整性防止未授权的数据篡改.任何分区执行任意事件的过程中,不允许修改在系统安全策略中定义的 3514 软件学报 2023 年第 34 卷第 8 期 该分区所不能干扰的其他分区的私有数据,事件执行前后的状态,对于该分区不能干扰的那些分区是等价的.换言之,分区只能向系统允许其干扰的分区发送数据.总而言之,机密性定义了对分区的读访问控制,完整性定义了对分区的写访问控制.基于单个事件的机密性和完整性,可以定义系统的机密性 confidentialitye.confidentiality(e)和完整性 integritye.integrity(e).5 RMTEE 具体模型规约 RMTEE 具体模型由执行模型和事件规约组成.执行模型是抽象模型的实例,使用 interpretation 关键字将抽象模型 locale 中的抽象参数和函数实例化为具体实现.事件规约将事件具体化为一组 FF-A 接口函数,用于建模目标模块的功能和服务.locale 类似于面向对象语言中的接口,为本文实现由抽象到具体的精化模型提供支持;interpretation 则对应接口的实现,使用具体参数将 locale 中的信息解释到当前上下文,同时,借助Isabelle 的自动定理证明器证明具体化的模型仍然满足抽象模型中定义的规约.5.1 自主访问控制 ARM S-EL2 规范定义了分区间通信与调用的标准接口,但没有定义具体消息内容,任意分区间可以预先定义通信协议设计消息体结构,然后使用同一个标准接口完成不同的功能调用.然而,这种宽松的管理模式存在潜在风险:(1)如果某个分区的具体功能实现没有对消息体中的输入参数进行合法性检查,就有可能产生除零、整数溢出或命令注入等错误;(2)恶意分区可以无限制地向特定分区发起请求,占满其 vCPU,从而实现拒绝服务攻击.由于分区管理器不干涉消息体的结构和内容,因此无法在分区管理器中完成消息内容的合法性检查.为此,本文设计了分区间调用的自主访问控制,分区在其配置文件中定义其所信任的分区,以及它们可以向本分区发起哪些接口调用.通过访问控制机制定义系统的信息流安全策略,为分区增加一层安全保障,缓解漏洞利用和恶意攻击的风险.分区间调用访问控制在逻辑上它可以表示为一个访问控制矩阵,即:定义 5(分区间调用访问控制矩阵).IPC_ACM=S,O,A,其中,S=D,表示主体集合,代表发起分区间调用的分区;O=D,表示客体集合,代表接受调用的分区;A 是访问控制矩阵,AsoP(E),sS,oO,P 是幂集运算,Aso是事件集合的一个子集,表示主体分区可以向客体分区发起哪些接口调用.表 2 是访问控制矩阵的一个示例,其中,E表示所有事件集合,表示空集.表 2 分区间调用访问控制矩阵示例 分区 P1 P2 P3 P4 P1 E FFA_MSG_SEND_ DIRECT_RESP FFA_MSG_SEND2 FFA_RUN P2 FFA_MSG_SEND_DIRECT_REQE FFA_MEM_RELINQUISH P3 FFA_MSG_SEND2 E P4 FFA_MEM_DONATE,FFA_MEM_LEND,FFA_MEM_SHARE E 表 2 所示的访问控制矩阵规定,分区 P2可向 P1发起直接消息通信,P2可向 P1返回结果;P1和 P3之间可以发起异步消息通信;P1可以调用 P4运行;P4可以将内存块转让或共享给 P2,P2可以返回 P4共享的内存访问权限.5.2 执行模型 执行模型使用具体参数类型和函数代替抽象模型中的抽象参数:具体化的参数包括安全域(d)、状态(s)、事件(e),具体化的函数包括干扰性(?)、状态等价()和事件的执行域(D).它们在具体模型中的精化实现如表 曾凡浪 等:基于精化的 TrustZone 多安全分区建模与形式化验证 3515 3 所示.其中,安全域(domain)和状态(state)使用 Isabelle 的 record 关键字定义,类似于结构体类型,由多个字段组成.通过 record 的扩展语法(类似于面向对象的继承),又进一步定义了分区类型(partition)和分区管理器类型(SPM),它们继承了安全域中的字段,同时又包含各自独有的扩展字段.系统状态描述系统全局的数据,包括分区和分区管理器的运行时状态数据.事件(event)通过 datatype 关键字定义,类似于构造体.这些具体化参数的数据结构见表 4.表 3 状态机抽象参数的精化实现 状态机参数 抽象模型具体模型 安全域 d record Domain 状态 s record State 事件 e datatype Event 状态转移 definition fn_step 干扰性?definition fn_interference状态等价 definition fn_equiv 事件的执行域 D definition fn_kdom 表 4 具体模型中精化的参数数