[seL4] Re: Some small details in kernel code and docs

Hi Mark,

On Mon, Jun 21, 2021 at 3:32 PM Mark Jones wrote:

Here are a few minor details/questions about the kernel code & documentation. (I've confirmed that these are present in the new seL4-12.1.0 release.)

1) kernel/include/arch/x86/arch/32/mode/machine.h has the following definition (some code elided):

static inline word_t FORCE_INLINE x86_read_fs_base_impl(void) { word_t base = 0; base &= ...; base &= ...; base &= ...; return base; }

I'm pretty sure that the three &= operators here should be |= or else the result is always going to be zero. The same issue occurs in x86_read_gs_base_impl in the same file.

Some follow-up questions: Can anyone say if this would have been detected if the PC99 (32-bit) platform had been verified?

This would not have been caught by the proof itself, because this particular function is hidden behind the machine interface, i.e. the proofs don't see it (if they did see it, it would have come up that the result is always zero). It should be found during the validation part where we check that the machine interface makes sense. That part is manual, though, and has the usual problems of eyes sometimes seeing what they want to see instead of what is there. Nice catch! Cheers, Gerwin