trates on formal specifying/developing/modeling separation kernels and *Verification* on formally verifying separation kernels. Some work aims at these two aspects together. The “Property” indicates the policies or properties specified or verified in each work. The “Formal Language” indicates what’s the formal language used when specifying or verifying the separation kernels. The “Approach” indicates the formal specification or verification approaches used. The “Size” shows the scale of the formal specification or verification proofs. The “Tools” shows the software tools used in each work.

[|p[3.5cm]{}|p[3.2cm]{}|p[1.5cm]{}|p[2.0cm]{}|p[2.8cm]{}|p[2.0cm]{}|p[1.8cm]{}|p[3.0cm]{}|]{} **Related Work** & **Target Kernel** & **Objective** & **Property** & **Formal Language** & **Approach** & **Size** & **Tools**\
Department of Defense [@Martin00; @Martin02] & MASK separation kernel &

  ---------------
  Specification
  Verification
  ---------------

& Data separation & SPECWARE &

  -----------------
  Refinement
  Theorem proving
  -----------------

& [$\divideontimes$]{}& SPECWARE environment\
GWV, GWVr2 and extensions [@Greve03; @Rushby04; @Alves04; @Tverdy11; @Richards10] & Applicable for generic separation kernels & Specification & Information flow security & ACL2, PVS & Theorem proving & [$\divideontimes$]{}& ACL2, PVS theorem prover\
Naval Research Lab [@Heitmeyer06; @Heitmeyer08] & ED separation kernel &

  ---------------
  Specification
  Verification
  ---------------

& Data separation & TAME &

  -----------------
  Refinement
  Theorem proving
  -----------------

& 368 LOC of TAME spec. & TAME, PVS theorem prover\
Craig’s book [@Craig06; @Craig07] & A separation kernel & Specification & & Z notation & Refinement & $\approx$100 pages & By hand\
Verified software project [@Velykis09; @Velykis10] & A separation kernel &

  ---------------
  Specification
  Verification
  ---------------

& PIFP & Z notation &

  -----------------
  Refinement
  Theorem proving
  ----------------