TrustZone中断隔离机制的形式化验证  

Formal Verification of Interrupt Isolation Mechanism for TrustZone

作　　者：付俊仪 张倩颖[1,2,3] 王国辉 李希萌[1,4] 施智平 关永 FU Jun-yi;ZHANG Qian-ying;WANG Guo-hui;LI Xi-meng;SHI Zhi-ping;GUAN Yong(College of Information Engineering,Capital Normal University,Beijing 100048,China;Beijing Engineering Research Center of High Reliable Embedded System,Beijing 100048,China;State Key Laboratory of Computer Architecture,Institute of Computing Technology,Chinese Academy of Sciences,Beijing 100190,China;Beijing Key Laboratory of Electronic System Reliability Technology,Beijing 100048,China;Beijing Advanced Innovation Center for Imaging Theory and Technology,Beijing 100048,China)

机构地区：[1]首都师范大学信息工程学院,北京100048 [2]高可靠嵌入式系统北京市工程研究中心,北京100048 [3]中国科学院计算技术研究所计算机体系结构国家重点实验室,北京100190 [4]电子系统可靠性技术北京市重点实验室,北京100048 [5]北京成像理论与技术高精尖创新中心,北京100048

出　　处：《小型微型计算机系统》2023年第9期2105-2112,共8页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61802375,61602325,61876111,61877040)资助;北京市教委科技计划一般项目(KM201910028005)资助;中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题项目(CARCH201920)资助;国防科技创新特区项目(18-163-11-ZT-005-038-05)资助;中央支持地方建设-“双一流”建设项目(20531120005)资助.

摘　　要：TrustZone技术通过对硬件进行安全扩展,为软件提供了相互隔离的可信执行环境和通用执行环境.中断隔离机制是TrustZone的关键隔离机制,确保安全中断和非安全中断分别在可信执行环境和通用执行环境中被处理,该机制不正确可能导致安全中断被通用执行环境处理,从而影响可信执行环境的安全性.本文提出ARMv8 TrustZone架构中断隔离机制的形式化验证方法,在定理证明器Isabelle/HOL中建立包含中断隔离机制关键软硬件的形式化模型,该模型为状态迁移系统,包括中断处理程序、TrustZone Monitor、中断控制器等组件;在证明模型满足正确性的基础上,通过展开定理验证无干扰、无泄露、无影响等信息流安全属性,结果表明TrustZone中断隔离机制满足信息流安全属性,在中断处理过程中不存在隐蔽的信息流通道.TrustZone technology provides software with the trusted execution environment and rich execution environment isolated from each other by hardware security extensions.The interrupt isolation mechanism is a crucial isolation mechanism of TrustZone,which ensures that secure interrupts and non-secure interrupts are handled in the trusted execution environment and rich execution environment respectively.Its incorrect may cause secure interrupts to be handled by the rich execution environment,thus affecting the security of the trusted execution environment.This paper proposes a formal verification method for the interrupt isolation mechanism of the ARMv8 TrustZone architecture.We establish a formal model consisting of the critical software and hardware of the interrupt isolation mechanism in the theorem prover Isabelle/HOL.The model is a state transition system,including interrupt handlers,TrustZone Monitor,interrupt controller and other components.On the basis of proving the correctness of the model,this paper verifies the information flow security properties such as noninterference,nonleakage,and noninfluence by using the unwinding theorem.The results show that the TrustZone interrupt isolation mechanism satisfies information flow security properties,and there is no covert channel of information flow in the interrupt handling process.

关 键 词：TRUSTZONE 可信执行环境 中断隔离 信息流安全 形式化验证 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]