[seL4] Re: Thread Scheduling Domains

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

On 2 Aug 2022, at 02:14, June Tate-Gans (ジューン) 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 (ジューン) 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