There is an additional
requirement that any ``security kernel'' be simple enough that
independent evaluators can assess whether it will operate properly.
While we will not prove such a feature about our system here we do
attempt to keep the security model as simple as is feasible.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
