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 wrote:

On 12 Dec 2015, at 8:56 , Brian Mastenbrook 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 Devel@sel4.systems https://sel4.systems/lists/listinfo/devel