Hi Mark, > On Mon, Jun 21, 2021 at 3:32 PM Mark Jones <[email protected]> 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 _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
