i,s}^1 = 0, ...,  D_{i,s}^k = 0$ means that all data areas in the partition $i$ are clear. Satisfaction of this property implies that no data stored in the partition during one configuration of this partition can remain in any memory area of a later configuration.

### Formal Comparison of Policies and Properties

As presented in previous subsections, security policies and properties for separation kernels have been studied in literature. They are formalized in different specification and verification systems, such as ACL2, Isabelle/HOL, and PVS. Formal comparison of them to clarify the relationships can establish a substantial foundation for formal specification and verification of separation kernels.

In [@von04], the notions of noninterference, nonleakage, and noninfluence are defined based on the same state machine and formally compared. The author states that noninfluence is semantically equal to the conjunction of noninterference and nonleakage.

In [@Bond14], the GWV policy and Rushby’s noninterference are formally compared in detail. The authors present a mapping between the objects and relations of the two models. The conclusion is that GWV is stronger than Rushby’s noninterference, i.e., all systems satisfying GWV’s separation also satisfy Rushby’s noninterference.

Formal Specification and Models of Separation Kernels
-----------------------------------------------------

The formal specification and models of separation kernels present a significant contribution to formal verification. Here, we only discuss the models for formally developing separation kernels. Models targeted at formal verification are surveyed in the next subsection. In formal development, the specification may be used as a guide while the concrete implementation is developed during the design process. We present typical specification and models of separation kernels in turn.

-   Craig’s Z model of separation kernel

Following the earlier book on modeling operating system kernels [@Craig06] that shows it is possible and r