To Prove a Kernel
I suggest loading the kernel and a proof checker together into the RAM of the system that we want the kernel to securely control.
We must insure that the checker was loaded as desired.
The checker reads a proof of the desired kernel properties from an external source.
The proof is in the form of a sequence of propositions each accompanied by designators of previous propositions in the proof already proven.
The proof also announces when particular propositions need no longer be remembered.
That is to save space.
When the checker is finished the coded desired kernel properties should be in RAM.
We must insure that those properties are as required.
Then an initial PSW (Program Status Word) that was mentioned in the proof is loaded and the proven kernel is in control.
The proof could concern the kernel and initial domains for those many who need to rely on the correctness of user code.
For checking established invariants that are relied upon, a checker could consult the state of a system checkpoint that was about to be resumed.
“We must insure that” is mysterious above but it is less mysterious here than in conventional proof checking systems.
Reporting a secure hash of the checker and later of the properties is a good start.
It would be nice to think that these steps could be taken on every kernel load.