I assume this can be an issue when you are managing interrupts. As far as I know, we cannot have interrupts handled by two partitions: in that case, which one acknowledges the interrupts? How to keep track of the number of ticks? And how to finally get the time?

Even if partitions are isolated, we still need to manage the hardware and answer to handle (at least some) interrupts. For example, managing the timer interrupt. Some devices can be managed without managing the timer (for example, a network driver can be implemented using polling) but it might be critical for other to acknowledge the interrupt as soon as possible.

To enable time management, you need to have a separate partition to receive the timer interrupts and keep track of the time. This partition is then connected to other partitions that need timing services. I think this is what has been done for SMACCM. If we keep partitions access the same hardware resources, this is potentially a security design flaw (access of a shared resource from partitions at different security level/domains).

Now, about the real-time extensions, I do have some questions:

1. Is there any documentation about it?

2. What are the new features? Are they documented? Is there a support with CAmkES? I remembered having seen something like _period and _budget attributes in CAmkES but no documentation. What is the unit (processor tickers, nanoseconds?)? Having documentation and/or examples would be appreciated.

3. Where to grab it, use it and experiment it?

Thanks!

On Sat, May 7, 2016 at 10:22 PM, Felix Kam <felixkam42@gmail.com> wrote:

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

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