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

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

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 137 definitions and 201 lemmas in the model(more than 11000 lines of Isabelle/HOL code).The results show that the model satisfies confidentiality and integrity,and can effectively defend against malicious attacks of partitions.