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

作     者：曾凡浪 常瑞 许浩 潘少平 赵永望 ZENG Fan-Lang;CHANG Rui;XU Hao;PAN Shao-Ping;ZHAO Yong-Wang

作者机构：浙江大学计算机科学与技术学院浙江杭州310027 浙江大学杭州国际科创中心浙江杭州311200 浙江省区块链与网络空间治理重点实验室浙江杭州310027 

基　　金：浙江省重点研发计划(2022C01165) 国家自然科学基金(62132014) 浙江省尖兵计划(2022C01045) 中央高校基本科研业务费(NGICS)专项资金 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2023年第34卷第8期

页      码：3507-3526页

摘      要：TrustZone作为ARM处理器上的可信执行环境技术,为设备上安全敏感的程序和数据提供一个隔离的独立执行环境.然而,可信操作系统与所有可信应用运行在同一个可信环境中,任意组件上的漏洞被利用都会波及系统中的其他组件.虽然ARM提出了S-EL2虚拟化技术,支持在安全世界建立多个隔离分区来缓解这个问题,但实际分区管理器中仍可能存在分区间信息泄漏等安全威胁.当前的分区管理器设计及实现缺乏严格的数学证明来保证隔离分区的安全性.详细研究了ARM TrustZone多隔离分区架构,提出一种基于精化的TrustZone多安全分区建模与安全性分析方法,并基于定理证明器Isabelle/HOL完成了分区管理器的建模和形式化验证.首先,基于逐层精化的方法构建了多安全分区模型RMTEE,使用抽象状态机描述系统运行过程和安全策略要求,建立多安全分区的抽象模型并实例化实现分区管理器的具体模型,遵循FF-A规范在具体模型中实现了事件规约;其次,针对现有分区管理器设计无法满足信息流安全性验证的不足,设计了基于DAC的分区间通信访问控制,并将其应用到TrustZone安全分区管理器的建模与验证中;再次,证明了具体模型对抽象模型精化的正确性以及具体模型中事件规约的正确性和安全性,从而完成模型所述137个定义和201个定理的形式化证明(超过11000行Isabelle/HOL代码).结果表明:该模型满足机密性和完整性,并可有效防御分区的恶意攻击.

主 题 词：可信执行环境 安全分区 定理证明 精化 安全性分析 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.13328/j.cnki.jos.006866

馆 藏 号：203122621...