Also note that this might be a comment that only applies to the Haskell model, not to the C kernel.
I should double check, but I don’t think we insist in the proof on the address of the idle thread to match C, i.e. we may have chosen something different in Haskell for simulator convenience. Cheers, Gerwin > On 12 Dec 2015, at 2:42 pm, Gernot Heiser <[email protected]> wrote: > > On 12 Dec 2015, at 8:56 , Brian Mastenbrook <[email protected]> wrote: >> >> While pulling up the Haskell model to respond to the previous question, I >> noted the following statement: "The idle thread's code is at an arbitrary >> location in kernel memory. For convenience in the Haskell model, we place it >> in the globals frame, but there is no need for it to be in user-accessible >> memory." >> >> Given that the globals frame is mapped cacheable, doesn't this lead to a >> potential timing side channel? Tasks would be able to determine whether the >> idle thread's code has been evicted from cache, which may or may not reveal >> something interesting about the state of the system as a whole. > > Quite possible, but not the only potential timing channel in the present > kernel. We’re working on a systematic approach to getting rid of them > > Gernot > > > ________________________________ > > The information in this e-mail may be confidential and subject to legal > professional privilege and/or copyright. National ICT Australia Limited > accepts no liability for any damage caused by this email or its attachments. > _______________________________________________ > Devel mailing list > [email protected] > https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
