(19)国家知识产权局 (12)发明 专利申请 (10)申请公布号 (43)申请公布日 (21)申请 号 202210411830.8 (22)申请日 2022.04.19 (71)申请人 浙江大学 地址 310058 浙江省杭州市西湖区余杭塘 路866号 (72)发明人 常瑞　余晨洋　苗新亮　曾凡浪　 张子君　任奎　 (74)专利代理 机构 杭州中成专利事务所有限公 司 33212 专利代理师 李亦慈　唐银益 (51)Int.Cl. G06F 12/14(2006.01) G06F 21/60(2013.01) G06F 21/62(2013.01) G06F 21/57(2013.01)G06F 21/53(2013.01) (54)发明名称 一种针对ARM架构的基于安全属性的访问控 制形式化验证方法 (57)摘要 本发明公开一种针对ARM架构的基于安全属 性的访问控制形式化验证方法， 该方法对系统中 的实体进行抽象， 为其赋予安全属性， 以实现灵 活、 细粒度的系统资源管理， 增强了ARM架构的资 源安全保护。 首先， 定义系统资源的原子安全属 性， 并基于这些原子安全属性， 为系统中的实体 指定安全属性； 其次， 定义访问控制策略， 访问控 制策略为可信执行环境和非可信执行环境中产 生的资源访问请求做出是否允许访问的判断， 它 以主体属性、 客体属性和访问属性配置为输入 等， 本发明可以实现对特权模式与用户模式的内 存读写权限的细粒度描述， 增强ARM架构的内存 隔离保护。 实验证明了本方案设计的访问控制机 制的有效性及其较低的性能开销。 权利要求书1页 说明书8页 附图2页 CN 114610658 A 2022.06.10 CN 114610658 A 1.一种针对ARM架构的基于安全属性的访问控制形式化验证方法， 其特征在于， 该方法 包括如下步骤： 步骤一： 定义系统资源的原子安全属性， 并基于这些原子安全属性， 为系统中的实体指 定安全属性， 包括主体属性、 客体属性、 用户属性和资源属性； 步骤二： 定义访问控制策略， 访问控制策略以主体属性、 客体属性和访问属性配置为输 入， 为可信执 行环境和非可信执 行环境中产生的资源访问请求做出 是否允许访问的判断； 步骤三： 对安全属性和访 问控制策略进行形式化描述与验证， 以确保访 问控制机制满 足机密性与完整性要求； 步骤四： 对ARM架构的内存访问控制机制进行修改， 以解决ARM内存访问控制机制存在 的缺陷。 2.根据权利要求1所述的针对ARM架构的基于安全属性的访问控制形式化验证方法， 其 特征在于， 所述步骤一中的原子安全属性是系统资源最为基础的属 性， 包括身份、 类型、 地 址、 特权级别， 用于对系统资源进行细粒度划分。 3.根据权利要求1所述的针对ARM架构的基于安全属性的访问控制形式化验证方法， 其 特征在于， 所述步骤一中的安全属 性所描述的是系统中实体的固有属 性， 描述了实体的系 统身份标识、 所拥有资源的属性以及与其 他实体的关系。 4.根据权利要求3所述的针对ARM架构的基于安全属性的访问控制形式化验证方法， 其 特征在于， 所述的步骤一中的安全属 性以原子安全属 性为基础， 所述的主体属 性是主体指 系统中的资源访问者、 客体属 性是客体指系统中的被访问资源， 所述的用户属 性和资源属 性都是主体属性和客体属性的组成部分。 5.根据权利要求1或2或3或4所述的针对ARM架构的基于安全属性的访问控制形式化验 证方法， 其特征在于， 所述的步骤二中的资源访问请求是指资源访问者请求对系统中的资 源进行读取、 写入或者执 行操作， 判断是指是否允许 该操作。 6.根据权利要求1所述的针对ARM架构的基于安全属性的访问控制形式化验证方法， 其 特征在于， 所述步骤二中的访问属 性配置设置了一个资源的所有访问属 性， 所述的访问属 性由包括读取、 写入、 执行的访问操作， 以及 包括用户模式、 特权模式的特权级别构成， 所述 的访问属性配置和主体属性、 客体属性共同作为访问控制策略的输入。 7.根据权利要求5所述的针对ARM架构的基于安全属性的访问控制形式化验证方法， 其 特征在于， 所述步骤四中的ARM内存访问控制机制存在的缺陷是指其不足以描述特权模式 与用户模式对某一内存空间的读写权限的16种组合,不能独立控制 两者各自的读取、 写入 权限。 8.根据权利要求1所述的针对ARM架构的基于安全属性的访问控制形式化验证方法， 其 特征在于， 所述步骤四中对ARM架构的内存访问机制所进 行的修改， 是指保持页 表描述符的 执行权限控制位不变， 选取页表描述符中预留位中的4个位来控制特权模式和用户模式的 读取和写入权限， 对特权模式与用户模式的内存读写权限进行细粒度描述。权　利　要　求　书 1/1 页 2 CN 114610658 A 2一种针对 ARM架构的基于安全属性的访 问控制形式化验证 方法 技术领域 [0001]本发明涉及智能设备访问控制安全领域， 具体涉及一种针对ARM架构的基于安全 属性的访问控制形式化验证方法。 背景技术 [0002]随着物联网、 边缘计算技术的迅猛发展， 使用ARM、 RISC ‑V等精简指令集的处理器 正在变得流行。 这些 处理器利用有限的资源， 尽可能为智能终端、 边缘节点等提供充足的计 算资源。 然而， 智能设备的广泛使用也凸显了它们在安全方面上的不足， 于是， 智能设备 的 安全性逐步成为了工业和学术界的研究热点。 智能设备目前采用了各种各样的访问控制机 制来抵御攻击， 如依赖于软件硬件协同设计的可信执行环 境(TEE)， 它用于提供强大的隔离 机制， 被广泛用于这些场景中以承载一些安全功能。 然而， 目前的访问控制机制经常存在缺 陷， 在智能设备所面临的各种威胁中， 利用其访问控制机制的缺陷所发起的攻击越来越多。 近年来， 许多 学者提出了增强TEE 资源安全保护的解决方案， 包括优化隔离粒度以减少攻击 面， 构建加密 模块， 以及执行运行时检查以增加攻击难度， 但这些解决方案中实现的安全机 制往往既不灵活， 也不能实现细粒度控制， 缺乏严格的安全保障。 因此， 隔离域之间的安全 边界很容易被打破。 确保软硬件功能正确 性的一种方法是使用形式化方法， 这种 方法已经 逐渐应用于TEE。 但是， 现有的工作常常只保证TA(可信应用程序)的安全属性， 也难以提供 调度程序接口。 [0003]ARM架构的内存访问机制也存在缺陷， ARMv8架构采用的访问控制机制大致如下： 该架构使用PXN和UXN分别控制特权模式、 用户模式对内存的执行权限。 对于读写权限， 使用 PSTATE.PAN位控制特权模式访问任何属于用户模式的内存， 使用页表项中的AP[2:1]属性 位来控制内存区域的读写权限。 但由于AP 两位不足以描述特权模式以及用户模式的内存读 写权限的16种组合， 该机制存在两个缺陷： 一方面， 不能单独描述读取、 写入权限； 另一方 面， 特权模式与用户模式下 的内存访问权限存在较大 的相关性， 不能独立控制它们的内存 访问权限。 发明内容 [0004]本发明公开一种针对ARM架构的基于安全属性的访问控制形式化验证方法。 该方 法对系统中的实体进行抽象， 为其赋予安全属 性， 以实现灵活、 细粒度的系统资源管理， 增 强了ARM架构的资源安全保护， 在此基础上， 将本发明提出的访问控制策 略应用在ARM处理 器中， 增强ARM架构的内存隔离保护。 具体技 术方案如下： [0005]一种针对ARM架构的基于安全属性的访问控制形式化验证方法， 该 方法步骤如下： [0006]步骤一： 定义系统资源的原子安全属性， 并基于这些原子安全属性， 为系统中的实 体指定安全属性， 包括主体属性、 客体属性、 用户属性和资源属性； [0007]步骤二： 定义访问控制策略， 访问控制策略以主体属性、 客体属性和访问属性配置说　明　书 1/8 页 3 CN 114610658 A 3