Paper Info
Title
Formal Verification Of Gp Specification Based Embedded Operating System
Abstract
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.
Year
DOI
Venue
2018
10.1145/3207677.3277971
PROCEEDINGS OF THE 2ND INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE AND APPLICATION ENGINEERING (CSAE2018)
Keywords
DocType
Citations 
Formal Specification, Formal methods, Certifying OS, Multi-Layered Verification
Conference
0
PageRank 
References 
Authors
0.34
0
4
Name
Order
Citations
PageRank
Haiyong Sun121.13
Lei Hang2277.62
Lei Qiao325.43
Yang Zheng421633.97