- Devel - lists.sel4.systems

Status of side-channel attack mitigation
by Demi M. Obenour 30 Jan '20

30 Jan '20

What is the current status of seL4 with respect to Meltdown, Spectre, L1TF, MDS and other CPU vulnerabilities? Thank you, Demi

2 2

(no subject)
by abdi mahmud haji 29 Jan '20

29 Jan '20

hi i have been wondering how can i install or put another OS( like , window ,linux )on the top of seL4 microkernel can some one help

2 1

Are there any plans to re-add seL4_Untyped_RetypeAtOffset?
by Andrew Warkentin 29 Jan '20

29 Jan '20

Speaking of things that would be useful for large dynamic systems, are there any plans to add seL4_Untyped_RetypeAtOffset from the old experimental branch to the current mainline kernel? I am writing a buddy untyped allocator for UX/RT, and being able to retype at arbitrary offsets would reduce overhead quite a bit because I could just retype from the highest-order untyped objects most of the time rather than having to create two child untyped objects per split. If not, I will probably end up re-adding it myself later on (sometime after UX/RT is running actual user programs).

5 20

Camkes and Memory-Mapped Peripherals
by Michael Neises 29 Jan '20

29 Jan '20

Hello, I'm trying to access a memory-mapped peripheral on the exynos5422 (ODROID XU4). I have the physical address of the peripheral's registers from the exynos5422 data sheet. As per the Camkes manual, I've used the seL4HardwareMMIO connection type to facilitate this. However, while I can use the excess bytes of the "dataport Buf" as expected, there is a data fault when I try to read from the peripheral's memory-mapped (and readable) registers: """ FAULT HANDLER: data fault from test_component.test_component_0_control (ID 0x1) on address 0, pc = 0x3250c, fsr = 0x211 """ Besides defining the hardware component and this connection in Camkes, is there anything else I must do? I will appreciate any guidance on this matter. Best, Michael Neises

2 1

Re: [seL4] Request for enhancement: Notification queues
by Millar, Curtis (Data61, Kensington NSW) 24 Jan '20

24 Jan '20

> I strongly suspect the more fundamental and general extension would be > to remove the scalability limitation of Notifications, probably by > generalising them to a hierarchy, i.e. you signal a sub-notification > which then signals the higher-level notification. I?m not claiming > having thought this through, though. Having thought about this a little, I think that it is useful to observe that the case where such cases where large numbers of notifications need to be received the receiver uses a roughly similar interface to endpoints (seL4_Send to wait for an event and seL4_NBSend to poll for events). If we allow send queues of endpoints to include notification objects in addition to threads we could multiplex notifications via an endpoint by binding the notifications to the endpoint. This could also allow for the removal of notification binding for threads; if they want to receive both notifications and synchronous IPC they can bind the notification to the endpoint. This design should also work with MCS whereby donation of scheduling contexts from notification objects would become roughly the same as donation from a thread with a scheduling context. I think the cleanest implementation would be to allow a notification to contain its own endpoint capability, similar to the manner in which TCBs conatain capabilities. Any time an idle notification is invoked with a send it then queues on the endpoint to which is capability refers if one exists. Send invocations of 'active' (potentially queued) notifications would perform the same XOR operation as currently occurs. When receiving on an endpoint where the first blocked object is a notification the badge received is the badge of the endpoint capability owned by the notification and the notification word is simply placed in the first message register. Whilst I think that this (or something similar) is the most simple case for implementing multiplexing it would have some impact on the semantics and implementation of some objects. Even at this small a scale the verification burden will still be considerable as this change would impact all verified builds. I think further discussion and evaluation of a solution is needed before we can determine that it is sufficiently beneficial to have this feature in the kernel and to commit to maintaining the feature and including it in the verified configurations. Cheers, Curtis Millar

2 1

Request for enhancement: Notification queues
by Demi M. Obenour 23 Jan '20

23 Jan '20

While studying seL4, I noticed that there is no mechanism to wait for one of many notifications. This proposal solves this with a new type of capability, which I call a notification queue. I don’t have the knowledge to determine how they should be implemented, so instead I will describe the general idea. A notification queue is a capability to which notification objects can be attached. When an attached endpoint is notified, a user-provided pointer is pushed onto the queue. Notification queues are edge-triggered, so subsequent notifications do not cause further entries to be added to the queue unless the notification has been read. The queue is implemented as a buffer which is read-only to userspace, but read-write to seL4. When creating a notification queue, userspace must provide sufficient untyped memory to ensure that the queue will not fill up. This ensures that sending a notification cannot fail due to resource exhaustion. Queues can be resized by the application if needed. Attempts to add too many endpoints to a queue results in an error being returned. A notification object can only be attached to one notification queue at a time. It can be detached from a queue and later attached to another. Notification queues can be used whenever a notification object is expected, except that they cannot be badged. Badging a notification queue would make no sense. When polled, a notification queue returns the number of events that have been added to it since it was last polled. Adding one notification queue to another may or may not be allowed. Allowing it would increase flexibility, but also increase implementation complexity. It is also possible to attach a TCB to a queue; the queue is notified when the TCB exits. Only seL4 can send to a notification queue. No userspace process can ever possess a send capability to such a queue. While a notification queue can be accessed from any number of tasks, performance on multi-core systems may be improved if each queue is used from the same core that its attached notifications are used on. Constructive feedback on this proposal is welcome. Sincerely, Demi

3 8

seL4 on unverified ARM platforms
by Demi M. Obenour 23 Jan '20

23 Jan '20

My understanding is that seL4 is currently only verified for one particular ARM platform. Is it considered production-ready on other ARM boards? Sincerely, Demi

2 3

Re: [seL4] Request for enhancement: Notification queues
by Heiser, Gernot (Data61, Kensington NSW) 23 Jan '20

23 Jan '20

On 22 Jan 2020, at 14:44, Demi Obenour <demiobenour(a)gmail.com<mailto:demiobenour@gmail.com>> wrote: But everything needs a really convincing argument, that’s based on a functional limitation that prevents implementation of certain important classes of systems. If it’s only a performance argument, we’ll need to be convinced that it really is a performance bottleneck in realistic systems. Do you believe it is likely to be? I haven’t seen a convincing use case where it is. Gernot

1 0

Plans for verification of IOMMU support on x86? Binary verification?
by Demi M. Obenour 21 Jan '20

21 Jan '20

Are there plans to verify the IOMMU support on x86? x86 without DMA is not very useful, so IOMMU support is needed for the proofs to apply in practice. Sincerely, Demi

2 1

Initializing of the sel4 tutorials fails because of missing the CMakeLists.txt
by Florian Berenbrinker 16 Jan '20

16 Jan '20

2 3