A recent note raised the issue of expressing kernel semantics formally enough to use formal methods to prove correctness of the code. I have a proposal that may be useful for two meanings of “formal” both to the end of avoiding kernel bugs.

The Keykos kernel has many invariants, mainly in the form of assertions that hold between units of kernel operation. These invariants are indeed checked by code that runs with a frequency proportional to the ratio of one’s fear of system corruption to one’s optimism. This is a very effective way of finding bugs in code that manipulates the real system state that is kept redundantly. It is of no use for finding bugs in miscopied keys, since state, such as ‘what key is in this slot’ is not redundant within the system. (The redundancy in the underlying ECC does not help here.) Fortunately such bugs are manifest to the user code and are likely to be noticed especially user mode diagnostic code. Random clobbering by the kernel of user memory memory will be noticed, but not easily diagnosed. (The 370's crude storage key protection, inherited from the 360, was used to protect user memory from wild stores by the kernel. Only a very small part of the kernel ran with PSW-key 0.)

The vernacular form of the idea is first to describe, or build, a crude version of the kernel that eschews “all” optimization. (Alternatives to “crude” are “dumb”, “simple”, “small”, “careful”.) The aim of this crude kernel is to be as plain as possible while yet being able to actually run to some degree, which degree we will explore. Its plainness facilitates informal comparison of the crude kernel behavior to documented kernel semantics.

Second we lash up the crude kernel with the official kernel, modifying each to some degree, so as to verify that they produce the same sequence of abstract states as the systems run.

Bochs presents options which may serve some purposes better. Bochs might be modified to run two kernels and compare the acts of the two kernels as they run in tandem under Bochs. I think there are new open source virtual machines for the PC. Hacking them might be a bit harder, but much more efficient than the Bochs way.

Eshewing optimization is a slightly vague concept; in particular it is unclear whether the crude kernel builds a hardware memory map. For some architectures, (but neither the 370 nor the x86), one need not emulate machine instructions to interpret their memory accesses. The 88K, for instance, lets the trap routine provide the effect of the thwarted memory referencing instruction without the routine having to concern itself with the details of the instruction that caused the fault. In short an 88K kernel could provide the illusion of virtual memory without employing the TLB. It would be several times slower than using the real TLB. It would be several times faster that total emulation of the CPU.

In any case an invariant is that the two kernels produce the same abstract state. There is, or was, a body of literature about proving programs equivalent.

Another possibility for a crude (trusted) kernel is to mark those domains that are in the TCB of security critical applications and only let the crude kernel touch those. This has problems for the fast kernel is on its honor not to piss on the critical domains. In any case there would be some use for a cruder, slower but especially trusted kernel with semantics identical to the fast kernel.

Yet another idea is a kernel with no I/O, or merely a kernel with I/O code removed to support applications that need a smaller TCB and do not need persistence and many GB of storage.