These are some thoughts on the logic of security; in particular about proving correctness of the code on which security and integrity rely.
The executive summary is that the kernel does not need hardware help to avoid errors in the context of a formal proof.
Read on, however, for a more practical view.

<p>There are two models of how to create a secure system.
Design and write code according to a formal model so that the resulting code can be ‘proven correct’.
seL4 has adopted this.
The more common path is to write the code to clear specs and then find and fix bugs as they arise.
Keykos follows this approach.
We contemplate the first model here.
<p>The system structure, which I consider here, relies on a kernel which is a body of code that runs uninterrupted in privileged mode.
There is code outside the kernel that that must also be correct for most of the security requirements.
The kernel must in some sense be flawless.
Some want hardware help to make the kernel more reliable.
But if we aspire to mathematical proof, the extra hardware is superfluous.
Any correctness proof whose outlines I have seen must first prove that stores are to the data structures that the proof logic specifies.
Integrity of kernel data structures, not to mention kernel code, is a prerequisite to the proof that the abstract state those structure describe follow the correct dynamic path.
Keykos (with no such formal proof) compensated here with frequently executed code that verified invariants.
The next proof step involves a formally defined map from kernel data structure state to abstract state.
With that map one can reason about operations on the real state and how that corresponds to the evolution of the abstract state.
Then you are in a position to reason about kernel semantics as implemented by the code.
<p>The 370 Keykos project was improved when we followed an admonition to use available hardware protection features.
We allocated about 5 storage key values to several sorts of kernel memory and switched PSW keys as required.
It was a small conceptual cost.
This was also a small dynamic cost and a class of kernel bugs were found more quickly.
Even such small cost would theoretically be unnecessary with a formal proof.
Keykos experience detected transient hardware errors a few times.