I know that the integrity proof guarantees a policy of integrity. But I wonder whether malicious calls of the kernel’s interfaces (i.e. vspace) that could interpolate the kernel’s code is allowed, though those callsalso follow the integrity policy.
Yes, the integrity of the kernel’s code and data structures is included, and is in fact required to show that integrity holds for user-level data.
Note that all of this is modulo the usual kernel verification assumptions, in particular that DMA is trusted/controlled and so on.
Thanks! I just realized that I may have asked a dumb question: the memory region where the kernel binary sits have higher authority levels than userland apps and this is enough to guarantee the integrity of the kernel’s binary. Is it?
That would hold for Linux as well, but doesn’t stop bugs violating kernel integrity.
seL4’s proofs establish that (subject to assumptions) the kernel always behaves as specified. This implies integrity of kernel data: if arbitrary changes to kernel data were possible, then the kernel’s behaviour would be undefined.
Now I’ve got the full picture. Thanks!