Build a trusted storage system on a mobile phone

The authors introduce their design, implementation and formally verification of a Trusted Execution Environment (TEE)-based trusted storage system (TSS) in mobile devices, which conforms to GlobalPlatform specifications. The authors' TSS provides not only authenticating the integrity and freshness of data but also many security storage operation properties like atomicity operations of a persistent object. To improve data store efficient when a big persistent object is read or written, a new mechanism that dynamic allocate continuous memory in REE's kernel memory space and map the address to the TEE through a communication pipe is proposed. This method can reduce switching times, allocating memory times and copy memory overloads between two worlds. A formal method is used in their design and development to guarantee the correctness and security of TSS. They consider the functional correctness mainly in this study, and use traditional formal verification tool - VCC verify the functional correctness of TSS. Their evaluation demonstrates its advantage compared to existing systems in addition.