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 (ジューン) <jtgans@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.

On Thu, Jul 21, 2022 at 5:44 PM Gerwin Klein <kleing@unsw.edu.au> wrote:

...

Hi June,

yes, if you're using the static domain scheduler, then that file needs to be overridden with the schedule you want.

Depending on what you're trying to do, the domain scheduler might not be the right tool for the job. It really is fully compile-time static.

Cheers, Gerwin

...

On 22 Jul 2022, at 01:35, June Tate-Gans (ジューン) via Devel <devel@sel4.systems> wrote:

Hey folks,

So Sam and I are at the point now where we're attempting to get our untrusted user threads running in a different scheduling domain, and it's not exactly clear how this is supposed to work in terms of enabling more than one domain in the kernel.

So far, I've set KernelNumDomains to 2 in the easy-settings.cmake for our project, but unless I provide a separate implementation of kernel/config/default_domain.c by overriding KernelDomainSchedule, the resulting kernel will only think it has one domain and only ever schedule domain 0 for execution.

Are we expected to override the default_domain.c file with our own in the project, like sel4test seems to do?

Thanks!

-- June Tate-Gans Software Engineer _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

-- June Tate-Gans Software Engineer Techlead, Kata OS / AmbiML, Cerebra Hardware

-- June Tate-Gans Software Engineer Techlead, Kata OS / AmbiML, Cerebra Hardware

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 <kleing@unsw.edu.au> wrote:

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