基于TrustZone的TEE设计与信息流形式化验证

基于可信硬件构建安全关键应用的可信执行环境（TEE），是嵌入式安全领域的一个研究热点。虽然底层硬件可信，但TEE软件仍可能因错误使用硬件指令或存在其他安全漏洞而导致机密信息泄露。该文基于ARM TrustZone技术提出了多层次的TEE架构，并建立了安全通信通道，用户层可信应用不能直接访问非可信环境的软硬件资源，只能通过内核层的安全通信通道API与外界通信，因此整个TEE的信息流不再受用户层影响。该文进一步提出了TEE形式化模型（TEEFM），借助Coq辅助证明器验证了TEE信息流无干扰性并证明了TEE安全监控模块不存在整型溢出、程序返回地址异常等资源边界类软件漏洞，以此保证了TEE的自身安全性。

The Design of TEE Based on TrustZone and Formal Verification of Information Flow

It is a research hotspot to build a trusted execution environment(TEE) based on trusted hardware for security critical application in the security embedded area. Although the underlying hardware is trusted, vulnerabilities in the TEE software, such as the incorrect use of hardware instructions or other security vulnerabilities, can be exploited to divulge secrets. Based on ARM TrustZone, a multilayer architecture is proposed and a secure communication channel is built. The trusted applications from user layer can not access the memory of non-trusted environment directly, but communicate with external environment through the secure communication channel API. Thus, all of the information flow of TEE can hardly be influenced by the user layer. Furthermore, TEE formal module(TEEFM) is proposed and TEE information flow noninterference is verified by using Coq proof assistant. Besides, the absence of the software errors about resource boundary (e.g. integer overflow, function return address incorrect) in TEE secure monitor module is proved, which ensures the security of TEE itself.