Abstract: 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.