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

I will definitively have a look a the RT document and the related CAmkES extensions. For now, how the kernel schedules tasks and handle time isolation is definitively confusing, especially for a kernel that is focused on security and reliability. If there is no timing service and no way to get a reliable concept of time, how can I implement a control law or a periodic tasks (that is potentially critical)? I understand that drivers should be implemented in their own address spaces but we also want to make sure that the driver is executed. And for now, I do not see how I can do that with seL4 and from what I have read, it seems that if I am using domains, the driver might miss some interruptions (and so, not have an accurate/consistent value of time). On Mon, May 16, 2016 at 5:57 PM, Gernot Heiser wrote:

Hi Julien,

We’ll provide some answers to your RT questions shortly.

For now just this re the domain scheduler: this is definitely aimed at high-paranoia scenarios, and actually requires polled I/O, rather than interrupts.

We’re working on a better solution to confidentiality isolation. However, the problem you identify with interrupt latencies and acknowledgment is inherent in any partitioning approach, there’s no way around.

Gernot

On 17 May 2016, at 1:28 , Julien Delange wrote:

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

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

------------------------------

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

On 17 May 2016, at 8:28 am, Gernot Heiser wrote:

On 17 May 2016, at 1:28 , Julien Delange wrote:

...

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?

We’ll make our latest RT branch publicly available, probably this week. It comes with an updated manual that describes the mechanisms. But note that it is experimental, and details are likely to change before it is merged into mainline. However, it’s overall very mature, and will start to be merged into mainline fairly soon.

In a nutshell, the new model replaces the time slice with a scheduling context (which is a new cap-protected object). An SC is essentially a pair of period and budget, where a thread is restricted to use no more than its budget every period. If period=budget, you get the old time slice back.

Scheduling contexts have a well-defined semantics of donation, they can be passed over IPC, so you can run a server on the budget of its clients with correct accounting (i.e. the client gets charged for the server time), essentially simulating a migrating threads model. There are other goodies, such as timeout exceptions…

The seL4 manual in the RT branch documents all the new kernel objects, syscalls, and behaviours. You can have a look at the manual in the current RT branch while waiting for the newest version to come out: https://github.com/seL4/seL4/tree/rt/manual We are currently preparing to push out a public version of the CAmkES support for the seL4 RT features. This basically makes the scheduling contexts available to be set and initialised from CAmkES. This will also include some examples that show how to do this in CAmkES. Ihor. ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.