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

TrustZone技术通过对硬件进行安全扩展,为软件提供了相互隔离的可信执行环境和通用执行环境.中断隔离机制是TrustZone的关键隔离机制,确保安全中断和非安全中断分别在可信执行环境和通用执行环境中被处理,该机制不正确可能导致安全中断被通用执行环境处理,从而影响可信执行环境的安全性.本文提出ARMv8 TrustZone架构中断隔离机制的形式化验证方法,在定理证明器Isabelle/HOL中建立包含中断隔离机制关键软硬件的形式化模型,该模型为状态迁移系统,包括中断处理程序、TrustZone Monitor、中断控制器等组件;在证明模型满足正确性的基础上,通过展开定理验证无干扰、无泄露、无影响等信息流安全属性,结果表明TrustZone中断隔离机制满足信息流安全属性,在中断处理过程中不存在隐蔽的信息流通道.