Abstract
With the rapid development of Internet of Things technology and the promotion of embedded devices' computation performance, smart devices are probably open to security threats and attacks while connecting with rich and novel Internet. Attracting lots of attention in embedded system security community recently, Trusted Execution Environment (TEE), allows for the execution of arbitrary code within environments completely isolated from the rest of a system. However, existing memory protection methods in a TEE are inadequate. In general, the software-based formal methods are not practical and the hardware-based implementation approaches lack of theoretical proof. To address the memory isolation and protection problems in TEE, in this paper, we propose a practical memory integrity protection method on an ARM-based platform, called MIPE, to defend against security threats including kernel data attacks and direct memory access attacks. MIPE utilizes TrustZone technique to create a isolated execution environment, which can protect the sensitive code and data against attacks. To present the integrity protection strategies, we provide the design of MIPE using B method, which is a practical formal method. We also implement MIPE on the Xilinx Zynq ZC702 evaluation board. The evaluation results show that the automatic proof rate of machines using B method is about 78.32%, and the proposed method is effective and feasible in terms of both load time and overhead.