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

Refinement-based Modeling and Formal Verification for Multiple Secure Partitions of TrustZone

作　　者：曾凡浪 常瑞 许浩 潘少平 赵永望 ZENG Fan-Lang;CHANG Rui;XU Hao;PAN Shao-Ping;ZHAO Yong-Wang(College of Computer Science and Technology,Zhejiang University,Hangzhou 310027,China;ZJU-Hangzhou Global Scientific and Technological Innovation Center,Hangzhou 311200,China;Key Laboratory of Blockchain and Cyberspace Governance of Zhejiang Province,Zhejiang University,Hangzhou 310027,China)

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

出　　处：《软件学报》2023年第8期3507-3526,共20页Journal of Software

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

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

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]