Aha! Thanks very much for this information -- helps to better understand what the threat model is. :D
On Mon, Aug 1, 2022 at 5:39 PM Gerwin Klein <kle...@unsw.edu.au> wrote: > > On 2 Aug 2022, at 02:14, June Tate-Gans (ジューン) <jtg...@google.com> wrote: > > Apologies for the necro, since it's been 10 days, but can I get > clarification on this? Thanks! :D > > On Fri, Jul 22, 2022 at 7:51 AM June Tate-Gans (ジューン) <jtg...@google.com> > wrote: > >> On that note, what kinds of information leak is this domain scheduling >> supposed to provide vs. everything all in one domain? The documentation for >> seL4 alludes to "certain" kinds of information leakage, but knowing exactly >> what might better explain how and when to use this kernel feature. >> > > The normal (within one domain) scheduler provides no time-based > information guarantees, e.g., it is easy to figure out if another thread > has used its time slice or not. That means for instance a higher priority > thread can signal information to a lower priority thread that way without > having an explicit communication channel like a notification, endpoint or > shared memory. > > The domain scheduler provides non-interference on actions observable in > memory (for uni-core). This includes timing in the sense of sequence of > actions, e.g. the action a thread takes to yield is observable and in the > domain scheduler setting, a thread in domain A cannot observe if a thread > in a different domain B has yielded or not. This does not include any > guarantees about the exact real time that has passed, in particular not > about timing side channels like caching channels, branch predictors, etc. > Also not power or other side channels. It also doesn't fully take care of > jitter at a domain switch caused by a potentially longer-running kernel > operation. Removing those is part of the ongoing time protection project, > but it's not currently part of the guarantees you get from the domain > scheduler. > > Cheers, > Gerwin > > -- June Tate-Gans Software Engineer Techlead, Kata OS / AmbiML, Cerebra Hardware _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
