G’s partitioning system and a low-level model that directly corresponds with the AAMP7G microcode. In the low-level model, each line of microcode is modeled by how it updates the state of the partition-relevant machine. The entire AAMP7G model is approximately 3,000 lines of ACL2 definitions. The AAMP7G GWV theorem is proved using ACL2. The proofs are decomposed into three main pieces: proofs to validate the correctness theorem, proofs to show that the abstract model meets the security specification, and proofs to show that the low-level model corresponds with the abstract model.

The AAMP7G GWV theorem is shown as follows. The theorem involves abstract and functional (low-level) models of the AAMP7G. The theorem is about the behavior of the functional model, but they express the theorem about an abstract model of the AAMP7G that has been “lifted” from a functional model. In this way, the expression of the theorem is simplified. Moreover, the behavior of the most concrete model of the AAMP7G is also presented to ensure that the theorem is about the “real” AAMP7G.

& secure\_config(spex)\
& spex\_hyp(spex,fun\_st1)\
& spex\_hyp(spex,fun\_st2)\

&

$$\begin{aligned}
& (raw\_selectlist(segs,abs\_st1) \\
& = raw\_selectlist(segs,abs\_st2) \; \wedge \\
& current(abs\_st1) = current(abs\_st2) \; \wedge \\
& raw\_select(seg,abs\_st1) = raw\_select(seg,abs\_st2) \\
\end{aligned}$$ $$\begin{aligned}
&\Rightarrow \\
& raw\_select(seg, lift\_raw(spex, next(spex,fun\_st1))) \\
& = raw\_select(seg, lift\_raw(spex, next(spex,fun\_st2))) )
\end{aligned}$$

where $abs\_st1=lift\_raw(spex,fun\_st1)$, $abs\_st2=lift\_raw(spex,fun\_st2)$ and $segs=dia\_fs(seg,abs\_st1) \cap segs\_fs(current(abs\_st1),abs\_st1)$.

-   PikeOS

PikeOS [@Kaiser07] is a powerful and efficient para-virtualization real-time operating system based on a separation microkernel. The Verisoft XT [^2] project has an Avionics subproject [@Baumann09; @Baumann09b; @Baumann09c] to prove functional correctness of all system calls of the PikeOS at the sourc