Biblio

Global Platform (GP)1 specifications accepted as de facto industry standards are widely used for the development of embedded operating system running on secure chip devices. A promising approach to demonstrating the implementation of an OS meets its specification is formal verification. However, most previous work on operating system verification targets high-level source programs proving the correspondence between abstract specification and high-level implementation but ignoring the machine-code level implementation parts. Thus, this kind of correspondence proofs stay in a shallow level. In this paper, we present a novel methodology for formal specifying and certifying the implementation of an embedded operating system strictly follows the GP specification. We establish a multiple abstraction layers framework that has four layers, from up to down, which are Formal Global Platform Layer (FGPL), Formal Specification High Layer (FSHL), Formal Specification Low Layer (FSLL) and Formal Assembly Machine Layer (FAML). To demonstrate the effectiveness of our methodology, we take the communication module of our Trust-E operating system (running on an extended CompCert ARM assembly machine model) as a case study and have successfully constructed a multi-layered proof, fully formalized in the Coq proof assistant. Some parts of the module are written in C and some are written in assembly; we certify that all codes implementation follow Global Platform specification.