- Devel - lists.sel4.systems

Reminder seL4 developer hangout
by Birgit Brecknell 29 May '23

29 May '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, May 31, 7am (UTC), Topics: (open) * Sydney: Wed, May 31, 5pm * Central Europe: Wed, May 31, 9am * US Pacific Time: Wed, May 31, 12pm (midnight) Calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Ring 3 iopl is going away, seL4 is ok
by William ML Leslie 21 May '23

21 May '23

Hello, I just noticed in the new x86-S rfc that Intel published that there will be no further support for io port access for processes in ring 3. Thankfully, this doesn't look like it will impact seL4, which provides capabilities to special objects representing port ranges on x86, which are then implemented in the kernel. Just in case anyone was wondering if there will be any impact, since this is the one thing that stuck out to me. Here's Intel's RFC: https://www.intel.com/content/www/us/en/developer/articles/technical/envisi… I think I might steal your IO port API for newer versions of Coyotos, which /is/ impacted by the change. TBF, I think seL4 has a better IRQ handling interface than the one we currently have too. I guess it's only fair it goes both ways! -- William ML Leslie

3 3

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

Reminder seL4 developer hangout
by Birgit Brecknell 15 May '23

15 May '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, May 16, 10pm (UTC), Topics: (open) * Sydney: Wed, May 17, 8am * Central Europe: Wed, May 17 12pm midnight * US Pacific Time: Tue, May 16, 3pm Calendar link: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 01 May '23

01 May '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, May 3, 7am (UTC), Topics: (open) * Sydney: Wed, May 3, 5pm * Central Europe: Wed, May 3, 9am * US Pacific Time: Wed, May 3, 12pm (midnight) Calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW birgit.brecknell(a)unsw.edu.au 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

One week to go to submit a talk for seL4 summit 2023!
by Birgit Brecknell 17 Apr '23

17 Apr '23

One week to go to submit a talk for seL4 summit 2023 [0]! If you'd like to submit a talk, please upload an abstract of one page or less to the submission portal [1]. The seL4 Summit 2023 will be held 19 - 21 September 2023 at the Elliot Park Hotel, Minneapolis, USA. The summit will be hosted by the Linux Foundation, and will be an in-person event. Registration details to follow soon. We're looking forward to many exciting proposals! [0] https://sel4.systems/Foundation/Summit/2023/cfp [1] https://sel4.systems/Foundation/Summit/2023/submit --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 17 Apr '23

17 Apr '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Apr 18, 10pm (UTC), Topics: (open) * Sydney: Wed, Apr 19, 8am * Central Europe: Wed, Apr 19, 12pm midnight * US Pacific Time: Tue, Apr 18, 3pm Calendar link: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Release of the CAmkES to seL4CP Transition Guide
by Jingyao Zhou 14 Apr '23

14 Apr '23

Hi all, The initial version of the CAmkES to seL4CP Transition Guide has been released. The guide aims to provide information and advice for those who are migrating applications built using CAmkES to the seL4 Core Platform. The main focus of this guide is on device driver development and virtual machine (monitor) development. The PDF version of this guide can be found on the Trustworthy Systems web page: https://stage.trustworthy.systems/projects/TS/sel4cp/2304-11-camkes-to-sel4… <https://stage.trustworthy.systems/projects/TS/sel4cp/2304-11-camkes-to-sel4…> The source of this guide can be found in the Trustworthy Systems GitHub repository: https://github.com/au-ts/camkes_to_sel4cp_guide <https://github.com/au-ts/camkes_to_sel4cp_guide> Please don’t hesitate to provide feedback! Regards, Jade.

2 4

Reminder seL4 developer hangout
by Birgit Brecknell 03 Apr '23

03 Apr '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Apr 5, 7am (UTC), Topics: (open) * Sydney: Wed, Apr 5, 5pm * Central Europe: Wed, Apr 5, 9am * US Pacific Time: Wed, Apr 5, 12pm (midnight) Calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

seL4 summit: deadline extension to 24th of April
by June Andronick (seL4 Foundation) 31 Mar '23

31 Mar '23

The deadline to submit a presentation to the seL4 summit 2023 is extended by 2 weeks. You now have until the 24th of April 2023 to propose a talk, by uploading an abstract of one page or less to: https://sel4.systems/Foundation/Summit/2023/submit The reason for the extension is that we want to let you know the definite dates for the summit before the deadline :) Current tentative (and very likely) dates are 19-20-21 September 2023, to be confirmed very soon. Looking forward to receiving your proposals. We want to hear about your cool seL4 work! And spread the word! If you want to hear about specific seL4 work, ping people around you or let us know at summit(a)sel4.systems <mailto:summit@sel4.systems> June

1 0