A formal proof of such claims is not out of the question but goes rather beyond any budget that I have seen proposed so far. I have in mind something that goes beyond the kernel correctness proof of seL4. I have unconventional opinions on the utility of such proofs, especially understanding what has been proven. Such proofs are very useful, however, and even the Keykos system avoided one bug by the very activity of imagining such a proof. I highly recommend this book for the real world of formal proofs.

The key objective fact to be proven is that the secrecy and integrity of your critical information within a computer is at risk to (relies on) a very small portion of the software that runs on that computer. The typical Keykos application will rely on the kernel, of course, and also several software components outside the kernel. If formal security assurance is required for this application then we must deal formally with the behavior of these additional components.

I resist the project of “implementing Unix within Keykos” for it would probably lead to a situation where applications would typically rely on something like a Unix kernel and I find it unlikely that suitable theorems for Unix exist. The Capsicum project may shed light on this. Also I would rather implement necessary Unix kernel function by small units and connect these units with capability discipline. This will cause Unix bugs but few if any security bugs. In short: I do not understand Unix.