Hi Mark, Just replying to 1 and 4 for now:
On Mon, Jun 21, 2021 at 3:32 PM Mark Jones <[email protected]> wrote: > > Hi All, > > 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? > More generally, where can I find information about how ia32 segment registers > are handled by the kernel? Why aren't they just stored/restored like other > user-level registers on kernel entry/exit? Is there something that prevents > user-level changes in the ES register, for example, from being observed in > other threads? The x86_read_fs_base_impl function does appear to have the defect that you observe. It also doesn't seem that the code can ever be called by the kernel. The kernel supports 2 ways for managing the FS/GS base address registers on ia32, CONFIG_FSGSBASE_GDT where they are written into the GDT table directly and CONFIG_FSGSBASE_MSR where msg registers are used. For both of these strategies, the kernel considers reading to be too expensive and so caches every write in a global value. Then when a read is performed it only looks up the cached value and doesn't call x86_read_fs_base_impl or x86_read_gs_base_impl. The issue that you identify was clearly missed during code review and we don't test that every line of source code is executed or even ends up in the final binary. As for whether verification would have caught it: if it was part of a verification configuration, and didn't have `/** DONT_TRANSLATE */` over the function, then it would need to be shown that it's implementation correctly refined whatever was specified in the higher spec. (Maybe someone from the proof engineering team could elaborate more). If it had DONT_TRANSLATE then it would instead need to be axiomatized and someone would have looked closely enough to hopefully see an issue. The segment selectors are cleared on entry to the kernel in src/arch/x86/32/traps.S with the RESET_SELECTORS macro. So the ES selector will be reset during any context switch between threads. > 2) A CNodeRotate will generate a FailedLookup error if the pivot slot either > doesn't exist or contains a null capability. But, in the first case the > "lookup failed for a source capability" field in the error message is 1, > while in the second it is 0. Hardly a serious problem, but this does seem > inconsistent. Is this intentional, or a mistake in the specification that > has been carried over to the implementation? > > 3) Section "3.4 Lookup Failure Description" of the manual describes how > capability lookup errors are represented in an IPC buffer. But it seems the > layout information is incorrect. For example, Section 3.4.2 says that > "Offset + 0" will contain seL4_MissingCapability while the number of bits > left will be at "Offset + seL4_CapFault_BitsLeft", which is probably supposed > to be equivalent to "Offset + 1". But, based on > kernel/libsel4/include/sel4/shared_types.h, it would seem that this gives > "Offset + 4". Sections 3.4.3 and 3.4.4 have similar problems. > > 4) On https://docs.sel4.systems/GettingStarted, in the section labeled > "Fetching, Configuring and Building seL4test", there are missing line breaks > between the commands in the text boxes for Steps 1 and 2, and there are some > tags in the text box for Step 4 that probably should not be displayed. Thanks for pointing this out. The source files have newlines in the code fragments, but they seem to be stripped by the markdown processor that is generating the site. For now the raw markdown page on GitHub may be easier to read: https://github.com/seL4/docs/blob/master/GettingStarted.md How did you find the issue with x86_read_fs_base_impl? Manual inspection or some sort of static analysis? Kind regards, Kent. > > Best wishes, and thanks for any feedback! > Mark > > _______________________________________________ > Devel mailing list -- [email protected] > To unsubscribe send an email to [email protected] _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
