verb15]. The formal API specification covers the IPC, memory, file provider, port, and event, etc.

Formal Verification of Separation Kernels
-----------------------------------------

As introduced in [[[Section]{}]{}]{} \[sec:bg\], the typical properties of separation kernels are data separation, information flow security, fault isolation, and temporal separation. The first three properties are collectively called “spatial separation” properties. Therefore, we categorize formal verification work on separation kernels into spatial and temporal separation verification in this subsection.

### Spatial Separation Verification

Most related work on formally verifying separation kernels consider both the data separation and information flow security. Here, we present significant research work of spatial separation verification. Due to the importance of data separation and information flow security properties for separation kernels, we finally highlight a general verification approach for these properties.

-   ED Separation Kenrel

A novel and practical approach to verify security of separation kernels code which substantially reduces the cost of verification is presented in [@Heitmeyer06; @Heitmeyer08]. The objective of this project is to provide evidence for a CC evaluation of the ED (Embedded Devices) separation kernel to enforce data separation. The ED separation kernel contains 3,000 lines of C and assembly code.

The code verification process consists of five steps: (1) Producing a Top-Level Specification (TLS) using a state machine model. (2) Formally expressing the security property as the data separation property of the state machine model. (3) Formally verifying that the TLS enforces data separation in TAME (Timed Automata Modeling Environment), a front end to the PVS theorem prover. (4) Partitioning the code into three categories, in which it is identified as “Other Code” such code not corresponding to any behavior defined by the TLS; “Other Code” is ignored in the verification, therefore great