Hi Will,

My understanding (I may be wrong here, please do correct me :) ) is that the time domains are temporally isolated in the sense that a program running in domain A is not supposed to know anything about timing that happens in domain B, so that it can't use that to infer about information.

So if you have 2 domains, A and B each with a time slice of 10ms, with some threads in both, B can't know when did A run out of runnable threads to run if it does(vice versa). If A ran out of things to do 5ms into its timeslice, I think the scheduler will just run the idle thread, until A's timeslice run out.

Given that context, why do you want to run such a timer driver in user land ? If they are mutually distrusting, I think such a driver can become a timing side channel. Why not give each of them their own timer driver ?

Cheers,

Felix

On Sun, May 8, 2016 at 11:41 AM, Will Klieber <weklieber@cert.org> wrote:

Hi,

Is there any way of obtaining the number of elapsed timer ticks from the seL4 kernel (using ARM / BeagleBoard platform)? I know the kernel uses this information internally for the scheduler, but I couldn't find any way of accessing it from userland.

Specifically, my usage scenario is as follows. Two mutually distrustful programs are running, and each wants to run an action periodically. We want to temporally isolate the two programs using seL4 time domains. In this case, interacting with the hardware timer in userland seems difficult, since we want to get the updated time whenever a new timer tick arrives, but the userland device driver for the timer can only operate in exactly one of the seL4 time domains. Please let me know if I am misunderstanding something or if there might be a better way to approach this situation.

Thanks,
Will

_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel