- Devel - lists.sel4.systems

Entry of user program
by mincheol＠vt.edu 30 Sep '22

30 Sep '22

Hi, I am trying to benchmark seL4's cross core IPC. I was able to run the IPC tutorial program and am now trying to run the server and the client on different VCPU. I found seL4_TCB_SetAffinity() but need to know the entry point of user program. Can anyone point it out for me? Mincheol

2 1

I need help with the IPC tutorial
by mincheol＠vt.edu 30 Sep '22

30 Sep '22

Hi, I can't figure out what to code in server.c for the ipc tutorial. What can I code after "// TODO use cap transfer to send the badged cap in the reply" line in the tutorial template (server.c) Can anyone share the fully working source.c?

3 3

Reminder seL4 developer hangout
by Birgit Brecknell 30 Sep '22

30 Sep '22

Hi all A friendly reminder that the seL4 developer hangout is on again next week: Tue, Oct 4, 9pm (UTC), Topics: (open) * Sydney: Wed, Oct 5, 8am * Central Europe: Tue Oct 4, 11pm * US Pacific Time: Tue, Oct 4, 2pm 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

Raspberry Pi SMP?
by dave＠synergy.org 30 Sep '22

30 Sep '22

Hello, Is there any intent to enable SMP on the Raspberry Pi? I am using the Raspberry Pi 3B+. I'd like to be able to use all 4 CPUs. Thanks, David

2 2

Support for Sel4 Project
by simone cataldo 29 Sep '22

29 Sep '22

Good morning, We are a small test team, investigating seL4 microkernel to evaluate its use it as core component for a novel “open avionics” drone concept. Essentially, we are starting from scratch, basing ourselves on the provided tutorials such as “hello world”. We were trying to modify its source code for evaluating basic thing simple functions, basic programs and custom libraries. However, it looks like the memory allocation is static and embedded in the original project: once we increase the complexity of the program it evidently causes trouble. We have not found any documentation about how to set the memory allocation at compile time, and how to include external dependencies (i.e. static libraries). We would like to have some guideline to get us started and direction to some in-depth documentation to acquire enough knowledge to build a full project of our own. We are looking forward to hearing from you soon. Best regards, Simone CATALDO

5 5

Reminder seL4 developer hangout
by Birgit Brecknell 19 Sep '22

19 Sep '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Sep 21, 7am (UTC), Topics: (open) * Sydney: Wed, Sep 21, 5pm * Central Europe: Wed, Sep 21, 9am * US Pacific Time: Wed Sep 21, 12 midnight 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

Proper seL4 APi/ABI design
by Eric Jacobs 17 Sep '22

17 Sep '22

Jumping off from the recent thread, I was curious if anyone had any thoughts about how to optimally design API's for seL4. I noticed we had a bit of info about what not to do (don't do long IPC, don't implement Posix, don't use messaging as synchronization, etc.) Are there any shining examples of what _to_ do with an API? Thanks, -Eric

5 11

Reminder seL4 developer hangout
by Birgit Brecknell 05 Sep '22

05 Sep '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Sep 6, 10pm (UTC), Topics: (open) * Sydney: Wed, Sep 7, 8am * Central Europe: Wed, Sep 7, 12 midnight * US Pacific Time: Tue, Sep 9, 3pm 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

tool to report per-component memory / resource use from system.cdl
by Sam Leffler 27 Aug '22

27 Aug '22

I'm looking for a script/tool that can break down memory by component given a system.cdl file. I've been doing this by hand (sorta) but figured I should ask before doing something more organized. -Sam

1 0

Project Sparrow / KataOS Initial Open Source Release
by June Tate-Gans (ジューン) 23 Aug '22

23 Aug '22

Hey guys! Sam and I have been hard at work at releasing our source code for the Project Sparrow work we've been working on for the last year or so, and we just managed to get our first release up at < https://github.com/AmbiML/sparrow-manifest>. So, we thought we'd announce it to the devel list! A bit of background: Sparrow is a project to build an open source low-power secure embedded platform for Ambient ML applications. Our target platform leverages RISC-V and OpenTitan, and all our contributions are licensed under the Apache-2 open source license. The Sparrow software includes a home-grown operating system named KataOS, that runs on top of seL4 and is written almost entirely in Rust. We’ve pushed some foundational pieces of KataOS to GitHub together with build glue to run seL4 CAmkES test applications on a 64-bit ARM platform (running in simulation on qemu). These are intended to show the direction we’re headed and enable anyone to start building their own systems in Rust on top of seL4. This initial tranche of code includes: frameworks (e.g. the sel4-sys crate that provides seL4 syscall apis), an alternate rootserver (needed for dynamic system-wide memory management), and the kernel modifications that enable reclaiming the memory used by the rootserver. This push does not, as yet, include the CAmkES services that support dynamic loading+running of applications–that will be published as we deem it ready for sharing until eventually all of Sparrow (software and hardware designs) will be available. While we are developing for an experimental 32-bit RISC-V platform, we intend to push code that runs on aarch64 platforms. Help is welcome to make the code base run on more platforms. In the long run, we're planning on opening up everything we can, so please watch this space! -- June Tate-Gans Software Engineer Techlead, Kata OS / AmbiML, Google

4 5

Reminder seL4 developer hangout
by Birgit Brecknell 22 Aug '22

22 Aug '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Aug 24, 7am (UTC), Topics: (open) * Sydney: Wed, Aug 24, 5pm * Central Europe: Wed, Aug 24, 9am * US Pacific Time: Aug 24, 12 midnight 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

Re: QubesOS+seL4
by Gernot Heiser 11 Aug '22

11 Aug '22

[ Redirecting this inquiry to the more appropriate ailing list] On 2 Aug 2022, at 05:55, ossgroup <ossgroup(a)protonmail.com<mailto:ossgroup@protonmail.com>> wrote: I'm interested in porting QubesOS to seL4. Is there already an initiative for this? If not, would you mind pointing me in the right direction to get started? People have been playing with this on-and-off, including a honours thesis here at UNSW years ago. The closest current activity I’m aware off is our Makatea project which, in collaboration with Swiss company Neutrality, has a (presently) more limited aim of isolating servers on a private cloud: https://trustworthy.systems/projects/TS/makatea A full Qubes port would be cool but a fair bit of work. I’d definitely like to see it done, and it’s clearly a more secure approach than having Xen (and therefore a whole Linux) in your trusted computing base. Gernot

3 2

Re: QubesOS+seL4
by Demi Marie Obenour 09 Aug '22

09 Aug '22

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512 On Mon, Aug 08, 2022 at 03:24:51PM +0200, Hugo V.C. wrote: > You are absolutely rigth Demi. Anyway, I think the point here is not to > "switch" from Xen to seL4, which is an giant task, but to start > "something", some port of QubesOS, based on seL4. Obviously, it will lack > most features, bad hardware support, etc, but I guess that as soon there's > something that can be run, the community will slowly add effort to such > project. If you remember the first versions of Linux, desktop support was > horrible... But at some point there should be people starting new > challenging stuff. I don't think we can have a QubesOS based on seL4 at > short term, but if we start now, it can be a reality in few years. I can > smell lot of interest on it... - From a Qubes OS perspective, the approach I would prefer is to first get Qubes OS working on seL4, with the control plane running in a Linux VM as it does now. This is definitely less than optimal, but it is likely the quickest way to get Qubes on seL4 working at all, and therefore the solution that is the most likely to actually be finished. Over time, more and more of the code can be replaced by native seL4 components as those components become available. For instance, the firewall is currently based on Linux, but it is a stand-alone component that already has an alternative implementation based on MirageOS. Therefore, it would be an excellent candidate for replacement with a firewall running natively on seL4. - -- Sincerely, Demi Marie Obenour (she/her/hers) Invisible Things Lab -----BEGIN PGP SIGNATURE----- iQIzBAEBCgAdFiEEdodNnxM2uiJZBxxxsoi1X/+cIsEFAmLxkk0ACgkQsoi1X/+c IsH9Kg//U+FlcwVOtDXGfjJI2WCkRrLFbIC2Mvh6k1/m+f+aGtc7jvqj0xAFXxm3 JpvIYgil2LGGsdpC3dvyTH+7xqGQUVgzcYYyJDwbdRv0gBau1T+z3xkagYvOE1E8 94aEHLmvZV6GvXZ+6LdwZjkLgOQ0qnupOSkOJtmNW86tZdXC99u6cGhszejrCSG7 GzlWPaXfP7Niy16RA9QOf4nSusXvpetQwNhzTBvn1y2XrcnvitV9MNyhp23uyWMI 4VCMaA4tYbxyZdH0whQEpjrc75S2j/ewNuuiZ3VVnkOPxid0XG8UCsLGpWtoMIak /pO/JkZ25QuHAJv5ef4JpmDD5EO410vzrs70yswEb9Xcb6Fr+RnyCLmutAS1mpan zQs31KSXVOe0R5glO3p28wpkXLO80hjYrjVITnNknWv+uujHIGE1LiF8yRFaWMNa XpAUnKcTIBSqr/VkRwphBWRHkXMxKUBFbYBwV3WaUJ0fqOsGpUD4wLpLpE6N6Lb9 hRRfdM6raJ5LXNiSuheGKCh2Hxb5WejbQCH9vSCxd0Ew6j5NZf21YY84iykT47aR dO+o2XF04s4lfeBUhd8zMTSrKA6zIyAVdbtYfThT+ONXQd15YkkLWm0f7UJBCx4X kEsgYlCHXdJIQ9mkJZI4WIGRXO39sW+NCe3bs9w/YYwuVhmQKqg= =BkM1 -----END PGP SIGNATURE-----

2 4

Reminder seL4 developer hangout
by Birgit Brecknell 08 Aug '22

08 Aug '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue Aug 9, 10pm (UTC), Topics: (open) * Sydney: Wed, Aug 10, 8am * Central Europe: Wed, Aug 10, 12 midnight * US Pacific Time: Tue, Aug 9, 3pm 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

section type mismatch on aarch64
by Sam Leffler 03 Aug '22

03 Aug '22

I'm building for aarch64 and hitting: /usr/local/google/home/sleffler/camkes-aarch64-rootserver/kernel/include/arch/arm/arch/64/mode/kernel/vspace.h:55:36: error: ‘mode_reserved_region’ causes a section type conflict with ‘avail_p_regs’ 55 | static const region_t BOOT_RODATA *mode_reserved_region = NULL; ... /usr/local/google/home/sleffler/camkes-aarch64-rootserver/build/kernel/gen_headers/plat/machine/devices_gen.h:67:37: note: ‘avail_p_regs’ was declared here 67 | static const p_region_t BOOT_RODATA avail_p_regs[] = { Looking at the commit history I see this commit: https://github.com/seL4/seL4/commit/680ce96b590295c1d49db6a2a34f77ac22e8475a followed by this commit: https://github.com/seL4/seL4/commit/8a87015a7c289f8bc2b5799d61e7c91482ad1cb2 I'm using gcc 11.2 from arm's prebuilt toolchain repo: https://developer.arm.com/tools-and-software/open-source-software/developer… Removing the clang band-aid fixes things. My source tree is "tracking" upstream but not directly based off it. Have I missed a change that resolves this? Is the 11.2 release just not being used yet (assuming it's a change in gcc? -Sam

3 4

Thread Scheduling Domains
by June Tate-Gans (ジューン) 02 Aug '22

02 Aug '22

Hey folks, So Sam and I are at the point now where we're attempting to get our untrusted user threads running in a different scheduling domain, and it's not exactly clear how this is supposed to work in terms of enabling more than one domain in the kernel. So far, I've set KernelNumDomains to 2 in the easy-settings.cmake for our project, but unless I provide a separate implementation of kernel/config/default_domain.c by overriding KernelDomainSchedule, the resulting kernel will only think it has one domain and only ever schedule domain 0 for execution. Are we expected to override the default_domain.c file with our own in the project, like sel4test seems to do? Thanks! -- June Tate-Gans Software Engineer

2 5

Reminder seL4 developer hangout
by Birgit Brecknell 25 Jul '22

25 Jul '22

Hi all A friendly reminder that the seL4 developer hangout is on again next week: Wed, Jul 27, 7am (UTC), Topics: (open) * Sydney: Wed, Jul 27, 5pm * Central Europe: Wed, Jul 27, 9am * US Pacific Time: Wed, Jul 27, 12 midnight * 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 1

Sydney get-together on seL4 Day?
by Gernot Heiser 20 Jul '22

20 Jul '22

This is only of interest for those physically in Sydney. We have seL4 Day coming up (29 July, the 13th anniversary of completion of the seL4 verification and 8th anniversary of its open-sourcing). It would be great to use the occasion to get together. The continuing abnormal (i.e. very wet) weather in Sydney makes planning such an event difficult (and I’ll be on leave and out of town until the evening of the 28th), so things may have to happen on short notice. But weather permitting, a BYO BBQ in Maroubra would be great, and I would really love to catch up with the rest of the Sydney-based seL4 community. So I suggest people interested save the date (and let us know if you’re interested). Gernot

1 0

suggestion; update faq reference to ODROID-C2
by Van Ly 18 Jul '22

18 Jul '22

Hello, The faq section on "How can I build a system with seL4?" [1] has an obsoleted/discountinued product pointing to ODROID-C2 [2] a current product such as the one from OnLogic can replace, perhaps. [3] ``` If you have access to an Odroid-C2, you should be able to do the project work yourself as a way of familiarising yourself with seL4. ``` [1] https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html [2] https://www.hardkernel.com/shop/odroid-c2/ [3] https://www.onlogic.com/industrial-raspberry-pi/ -- vl

6 7

Systems with multiple PCI root complexes
by Peter Chubb 18 Jul '22

18 Jul '22

Has anyone extended the code in https://github.com/seL4/util_libs libpci to handle multiple root complexes? See bug https://github.com/seL4/util_libs/issues/131 I know genode added code to handle this, but they don't use that library. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW

1 0

seL4 kernel memory footprint
by Sam Leffler 14 Jul '22

14 Jul '22

I'm trying to figure out the physical memory used by the kernel. This is for riscv if it matters. -Sam

4 13

sel4 smmuv2.0 on tx2 related questions
by Tao Heng 陶恒-SW 13 Jul '22

13 Jul '22

Hi sel4-devs, I have been trying to make some understandings of smmuv2.0 features provided by sel4. According to the vmm project for the tx2 platform, such as the vm_minimal apps, after all the compiling, there will be two caps,vm0_sid and vm0_cb,which is supposed to be used for stage2 address translation. My questions are as followed: 1. Which smmu device was the sid cap assigned to ? 2. How were these two caps created in the cdl file? There seems no special configuration for Cmakes that is related to the caps. 3. According to the tx2.dts, there are many sid numbers assigned to the smmu device. Why was there just one sid cap created by sel4? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

2 2

Anyone using capability transfer in an seL4 project? Looking for examples for research
by sjwebb＠student.unimelb.edu.au 12 Jul '22

12 Jul '22

Hi all, I'm working on a Masters research project looking into mapping an object-capability programming language onto seL4, in a way that includes some kind of mapping from the language object capabilities onto seL4's capabilities (or vice versa). I'm at a stage of the project now where it would be really helpful to have some 'motivating examples' for transferring caps between threads/CSpaces. So I was hoping I could reach out to other seL4 developers to see if they had built any systems that made extensive use of moving capabilities around. Ideally, in an ocap language, these examples would be much easier to program than they currently would be in C... The simplest example I can think of is a memory allocation server, but that wouldn't necessarily involve handing caps on beyond the one (requesting) process, which is the kind of thing I think more interesting examples would comprise of. Cheers, Stewart Webb [Masters Research student at University of Melbourne]

2 2

Re: Running RISC-V seL4 in QEMU 7.0.50
by Ahmed Charles 12 Jul '22

12 Jul '22

I'm having similar issues getting seL4test to work on riscv32/64 on QEMU 6.0.0 and 7.0.0. I tried debugging with a connected gdb, but I'm new at this and setting breakpoints in user mode seems to fail, so I'm not sure what happens once the root task starts, other than it eventually runs an infinite loop (0: j 0b, specifically). Any ideas? Thanks.

5 7

How to boot sel4 with a VGA output
by Cong Guo 12 Jul '22

12 Jul '22

Hi, I am new to sel4. I find how to run sel4test on an x86_64 machine, but with only serial output. How can I run sel4test or another sel4 system image using a normal VGA output? Thank you.

2 1

Reminder seL4 developer hangout
by Birgit Brecknell 11 Jul '22

11 Jul '22

Hi all A friendly reminder that the seL4 developer hangout is on again next week: Tue, Jul 12, 10pm (UTC), Topics: (open) * Sydney: Wed, Jul 13, 8am * Central Europe: Wed, Jul 13, midnight * US Pacific Time: Tue, Jul 12, 3pm 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

How to Get Input Via Keyboard -SeL4
by Sriram 07 Jul '22

07 Jul '22

Im new to SeL4 and figuring out how to get input from a keyboard and print it as of now What api calls do I use and How to do it Thanks and Regards R.Sriram

2 1

CAmkES components for security auditing.
by Comet 06 Jul '22

06 Jul '22

Hi, Is there an existing CAmkES component that can persistently store seL4 logs for security auditing? So that I can audit data in real time. Comet

1 0

Re: seL4 on TX1
by Yiliang Wan 03 Jul '22

03 Jul '22

Hi! I encountered similar problem on TX1. I tried to boot via DFU, and get exactly the same output as @yjy from time to time. The artifacts in https://github.com/seL4/seL4/actions/runs/1715169793#artifacts are already expired. Could you please provide the latest available sel4test pre-build image for TX1. The original link for the post is： https://103.230.158.80/hyperkitty/list/devel@sel4.systems/message/P3Q5SDSPE… Thank you!

2 2

Camkes Cross VM Tutorial
by Sriram 30 Jun '22

30 Jun '22

Greetings, I have been trying to build Camkes Cross VM tutorial but it fails at the end, similarily when we boot Camkes VM Linux, We were not able to input anything from the keyboard and the Serial Output is as follows """ Starting network[ 0.810972] ip (679) used greatest stack depth: 6732 bytes left : OK Failed to locate device consumes_event. Failed to locate device emits_event. Welcome to Buildroot buildroot login: [ 1.431752] clocksource: tsc: mask: 0xffffffffffffffff max_cycles: 0x31015f85297, max_idle_ns: 440795334135 ns [ 1.442241] clocksource: Switched to clocksource tsc [ 2.811817] random: fast init done [ 134.023597] random: crng init done """" Is there any changes to be made in the source files or any other modifications And are there any pre-built images for x86_64 for easier implementation Keenly Awaiting for your Reply Thanks and Regards R.Sriram

1 0

Some questions about porting seL4 to CHERI(Morello)
by Sid Agrawal 29 Jun '22

29 Jun '22

Hi sel4-devs, As I had mentioned in the last developer call, I am porting seL4 to morello architecture. To be exact, I plan to run a hybrid kernel with hybrid userspace. The hybrid mode essentially means that you define CHERI capability pointers explicitly, but if not stated, everything is just a standard 64bit pointer. Based on browsing the code, I have jotted down the following list of items I need to change. 1,2 are just observations, and 3 is where I need some input. 1. Change the type of "registers" field in TCB in the kernel to store 128 bits instead of 64 bits per reg. This ties into the kernel_enter and restore_user_context code. It ensures that if a user app explicitly uses CHERI capabilities, it is not lost on a context switch.[1,2] - Done. 2. Change the syscall and IPC APIs to allow for passing CHERI caps. CHERIcaps are just 128 bits, so we should be able to pass them as arguments in IPC. The use case I have in mind is as follows - Imagine a mmap server. This server would return a VA to the caller, which in the CHERI world would be a CHERI capability. This mmap-server would allocate the memory and map it into the callee's virtual address space. Do you think this is a valid use case? 3. Update seL4_UserContext code to read and write newer regs from the user space. The seL4_UserContext struct will need to be updated to accommodate the new register DDC(default data capability reg). It will also need to be updated to accommodate 128 bit regs instead of 64 bits. This is where I ran into an issue - an assert statement in the build directory checks the size of the seL4_UserContext structure. Looks like it gets its info from the sel4arch.xml file[4]. I am not sure how to change XML processing to have it generate the correct size value for that struct. I have not created ifdef guard for morello yet, as this is just a hacky pass to get it working. My diff so far is available at [3] if anyone wants to take a look. Any help and suggestions on the approach would be greatly appreciated. Thanks, Sid [1] https://gitlab.com/arm-research/security/icecap/seL4/-/blob/morello/include… [2] https://gitlab.com/arm-research/security/icecap/seL4/-/blob/morello/include… [3] https://gitlab.com/arm-research/security/icecap/seL4/-/compare/pre-morello-… [4] https://gitlab.com/arm-research/security/icecap/seL4/-/blob/morello/libsel4…

1 0

SMP documents
by 603644559＠qq.com 23 Jun '22

23 Jun '22

I mainly want to know how threads is scheduled in SMP configuration. Is there any documents or manuals on SMP configuration?

2 1

Details on involvement of Data61/Trustworthy Systems with DARPA, esp. regarding UAVs?
by Isaac Beckett 23 Jun '22

23 Jun '22

Hello, in your answer about camkes VMs, you mentioned a collaboration with DARPA on their SMACCM/HACMS project. While seL4 is undoubtedly a good choice for mixed criticality systems like avionics on a UAV, I’m somewhat frustrated to hear y’all had done a contract for DARPA considering what they *use* those drones to do. Is there somewhere I can read more in detail about this and other military-adjacent contracts?

2 1

SeL4 Tutorial - Camkes CrossVM
by Sriram 22 Jun '22

22 Jun '22

Greetings, We have followed step by step and tried the CAMKES Linux VM tutorial, We have build it successfully but while booting via USB flash drive The Serial Output Stops after root Login and doesn't take any input SERIAL OUTPUT """ Starting network[ 0.810972] ip (679) used greatest stack depth: 6732 bytes left : OK Failed to locate device consumes_event. Failed to locate device emits_event. Welcome to Buildroot buildroot login: [ 1.431752] clocksource: tsc: mask: 0xffffffffffffffff max_cycles: 0x31015f85297, max_idle_ns: 440795334135 ns [ 1.442241] clocksource: Switched to clocksource tsc [ 2.811817] random: fast init done [ 134.023597] random: crng init done """" This is the serial output we got Is there any modifications of the source code required to make it work if so kindly provide the necessary details. Thanks and Regards R.Sriram

1 0

How can I ensure the security of a system developed by Camkes?
by Comet 22 Jun '22

22 Jun '22

Hi, I am using Camkes to develop VM virtualization, but I have a question that is how can I ensure isolation security between virtual machines? If a virus with a Trojan is installed on the VMM, will the virtual machines attack each other? and will the kernel be corrupted ? I didn't find some security instructions about the system developed by Camkes, or the implementation principle of Camkes, that is, how is resource mapping between seL4 and Camkes? Are there any related articles? Thanks, Comet959

2 1

SeL4 Source Code Documentation
by Sriram 20 Jun '22

20 Jun '22

Greetings, We are trying to understand the SeL4 Source Code, is there any documentation available that explains the source code and libraries Thanks and Regards R.Sriram

2 2

Re: SeL4 Source Code Documentation
by Isaac Beckett 20 Jun '22

20 Jun '22

Are those Haskell sources used to generate the C code, or are they an older version of the spec, or something? This is my first time hearing of them, so not sure what they’re used for.

3 2

Page fault on starting VM
by WILLIAMS Stephen 16 Jun '22

16 Jun '22

We’re currently working on formalising VM support for an iMX8 platform (the Avnet MaaXBoard) building upon the existing sylvain/imx8 and sylvain/gicv3 branches. However on start of the VM we’re seeing the following page fault: >>>>>> Booting all finished, dropped to user space .[0m.[30;1m<<.[0m.[32mseL4(CPU 0).[0m.[30;1m [decodeUntypedInvocation/205 T0x80bf81c400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>.[0m Install gic v3 Loading Linux: 'linux' dtb: 'linux-dtb' install_linux_devices(a)main.c<mailto:install_linux_devices@main.c>:652 module name: map_frame_hack install_linux_devices(a)main.c<mailto:install_linux_devices@main.c>:652 module name: init_ram libsel4muslcsys: Error attempting syscall 215 libsel4muslcsys: Error attempting syscall 215 libsel4muslcsys: Error attempting syscall 215 Waiting recv Ok -------- .[31;1mPagefault from [Linux]: read prefetch fault @ PC: 0x200 IPA: 0x200, FSR: 0x82000005 Context: x0: 0xb2000000 x1: 0x0 x2: 0xff058169ac x3: 0x3ec6 x4: 0x5527eb8 x5: 0x80000 x6: 0x58169c0 x7: 0x45dad8 x8: 0x5816a00 x9: 0x8c3a000038000000 x10: 0x1100000028000000 x11: 0x10000000 x12: 0x543a00003a040000 pc: 0x200 x14: 0x0 sp: 0x480a58 spsr: 0x3c5 x13: 0x0 x15: 0x1000000 x16: 0xb2000000 x17: 0x480a58 x18: 0x5816bd0 x19: 0x664616f6c x20: 0xb2000000 x21: 0xb0080000 x22: 0x5816a10 x23: 0x405524 x24: 0x5816ab0 x25: 0x5816a40 x26: 0x0 x27: 0xb2000000 x28: 0x480a58 x29: 0x480a50 x30: 0xc63e0000edfe0dd0 .[3.[0mm-------- main_continued(a)main.c<mailto:main_continued@main.c>:1134 Failed to run VM <<<<<< From existing reports it is my understanding that the “insufficient memory” and the “error attempting sys call 215” errors are to be expected and are not a concern; please correct me if that is not the case! Any suggestions as to the possible cause of the page fault or hints on how to progress with debugging this issue would be greatly appreciated. Thanks for your help, Stephen This message contains information that may be privileged or confidential and is the property of the Capgemini Group. It is intended only for the person to whom it is addressed. If you are not the intended recipient, you are not authorized to read, print, retain, copy, disseminate, distribute, or use this message or any part thereof. If you receive this message in error, please notify the sender immediately and delete all copies of this message.

3 5

seL4 gdb + renode support
by Sam Leffler 16 Jun '22

16 Jun '22

As I mentioned on yesterday's zoom call Antmicro has released support for debugging seL4 applications (esp CAmkES). https://antmicro.com/blog/2022/06/sel4-userspace-debugging-with-gdb-extensi… I've used it extensively and find it very useful. -Sam

2 1

Invitation: Reminder seL4 developer hangout @ Tue Jun 14, 2022 3pm - 4pm (PDT) (devel@sel4.systems)
by agrawal.sidhartha＠gmail.com 15 Jun '22

15 Jun '22

You have been invited to the following event. Title: [seL4] Reminder seL4 developer hangout - rump kernel - arm assembly question. When: Tue Jun 14, 2022 3pm – 4pm Pacific Time - Vancouver Where: https://unsw.zoom.us/j/82640784431 Calendar: devel(a)sel4.systems Who: * agrawal.sidhartha(a)gmail.com - organizer * birgit.brecknell(a)unsw.edu.au * devel(a)sel4.systems Event details: https://calendar.google.com/calendar/event?action=VIEW&eid=NWozdWplbDZwZmk3… Invitation from Google Calendar: https://calendar.google.com/calendar/ You are receiving this courtesy email at the account devel(a)sel4.systems because you are an attendee of this event. To stop receiving future updates for this event, decline this event. Alternatively you can sign up for a Google account at https://calendar.google.com/calendar/ and control your notification settings for your entire calendar. Forwarding this invitation could allow any recipient to send a response to the organizer and be added to the guest list, or invite others regardless of their own invitation status, or to modify your RSVP. Learn more at https://support.google.com/calendar/answer/37135#forwarding

3 2

Question about rumpkernel on seL4
by Sid Agrawal 15 Jun '22

15 Jun '22

Hello sel4-devs, I came across the rumprun-sel4-demo apps [1] repo. There seems to be some bitrot as the kernel version keeps moving forward, But after moving the kernel back to 12.0 and some cmake fixes, I could get many apps(LevelDB, Redis, Memcached) to compile. Though "hello" ran fine, the few others I tried failed with various errors in the simulate step(such as page faults and invalid syscall number). I plan to debug these at some point, but I had a few questions about the setup before that. 1. Is this repo considered abandoned? 2. Is the rumpkernel+app running as a Virtual Machine or as a user process in this setup? Phrased differently, is seL4 acting like an OS or a Hypervisor? 3. Is there a known effort to run another libOS on seL4, such as Unikraft? The current mental model I have for running real apps on seL4 is something like this diagram below: 3. App+LibOS(Redis + rump) ------------------------------------- 2. RootTask + other services* ------------------------------------- 1. sel4 ===================== 0. Hardware Most of my contributions would be in layer-2, i.e. (rootTask + other services). I would then want to expose these new functionalities to the libc inside layer 3. The kernel itself should be mostly untouched. Thanks, Sid [1] https://github.com/seL4/rumprun-sel4-demoapps

2 2

Query about the aarch64 Context Switch Code
by Sid Agrawal 15 Jun '22

15 Jun '22

Hi, I had a few questions about the context switch code in seL4 for aarch64. I spent a couple of days trying to make sense of it, so I thought it would be better to ask as I might be missing something that is not obvious. It looks like kernel_enter in traps.S [1] saves the user process's register immediately after an exception. And restore_user_context() in c_traps.c [2] is restoring them. Looks like the regs are stored in the TCB in the "tcbContext.registers" array. The restore code makes sense to me. It puts the ptr value of "(NODE_STATE(ksCurThread)->tcbArch.tcbContext.registers" in to the sp and starts loading the regs from there. However, the code in kernel_enter is a bit unclear to me. 1. What is the value of sp when executing the kernel_enter macro? Is that the SP_EL1, or somewhere else the sp was set to the address of the faulting thread's "tcbContext.registers". On reading the arm32's arm_swi_syscall [3] function, it looks like it is the latter, but I am unsure how that is being accomplished. It might be more to do with aarch64 than seL4. 2 Furthermore, when not specified, does sp mean SP_EL1 in EL1 and SP_EL0 in EL0, Or does lower case "sp" have a special meaning? I know that seL4 is configured to use SP_ELx at ELx based on value of SPEL in [4] 3 Lastly, what is lsp_i trying to do? Are we switching the value of sp from something else to the real kernel stack by storing the kernel's stack address in tpidr_el1? Thanks a lot, as always! Sid [1] https://github.com/seL4/seL4/blob/master/src/arch/arm/64/traps.S#L72 [2] https://github.com/seL4/seL4/blob/master/src/arch/arm/64/c_traps.c#L29 [3] https://github.com/seL4/seL4/blob/master/src/arch/arm/32/traps.S#L51 [4] https://github.com/seL4/seL4/blob/master/src/arch/arm/64/head.S#L78

1 1

SeL4: Cannot Input after booting VM Linux (x86_64)
by Sriram 15 Jun '22

15 Jun '22

Greetings, We built hello world program and recieved exact output as given in the tutorial while booting. Then we built the seL4 CamKes VM Linux and Optiplex 9020 for x86_64 platform and got the following results while booting through usb using syslinux commands "" Welcome to Buildroot buildroot login: [ 1.431752] clocksource: tsc: mask: 0xffffffffffffffff max_cycles: 0x31015f85297, max_idle_ns: 440795334135 ns [ 1.442241] clocksource: Switched to clocksource tsc [ 2.811817] random: fast init done [ 134.023597] random: crng init done "" After this we are not able to type anything (username and password to login ) We have both VTd and VTx enabled, What changes or approach should be done to solve this. Thanks and Regards R.Sriram

3 3

Canceled event: Reminder seL4 developer hangout @ Tue Jun 14, 2022 3pm - 4pm (PDT) (devel@sel4.systems)
by agrawal.sidhartha＠gmail.com 14 Jun '22

14 Jun '22

This event has been canceled. Title: [seL4] Reminder seL4 developer hangout - rump kernel - arm assembly question. When: Tue Jun 14, 2022 3pm – 4pm Pacific Time - Vancouver Where: https://unsw.zoom.us/j/82640784431 Calendar: devel(a)sel4.systems Who: * agrawal.sidhartha(a)gmail.com - organizer Invitation from Google Calendar: https://calendar.google.com/calendar/ You are receiving this courtesy email at the account devel(a)sel4.systems because you are an attendee of this event. To stop receiving future updates for this event, decline this event. Alternatively you can sign up for a Google account at https://calendar.google.com/calendar/ and control your notification settings for your entire calendar. Forwarding this invitation could allow any recipient to send a response to the organizer and be added to the guest list, or invite others regardless of their own invitation status, or to modify your RSVP. Learn more at https://support.google.com/calendar/answer/37135#forwarding

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 10 Jun '22

10 Jun '22

Hi all A friendly reminder that the seL4 developer hangout is on again next week: Tue, Jun 14, 10pm (UTC), Topics: (open) * Sydney: Wed, Jun 15, 8am * Central Europe: Wed, Jun 15, midnight * US Pacific Time: Tue, Jun 14, 3pm 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 on bare-metal | Questions and comments
by Sid Agrawal 10 Jun '22

10 Jun '22

Hi, As per instructions from here[1, 2], I tried booting seL4 on an x86_64-desktop, x86_64-server as RPi4. I was able to get it to work on RPi4 with one minor change to the instructions, but I could not boot it on the x86_64-desktop or the x86_64-server. Below is my experience and the issues I faced. RPi4 ------ Spec: 8GB standard Rpi4 The final command "fatload mmc 0 0x10000000 sel4test-driver-image-arm-bcm2711" gave the following error: ** Reading file would overwrite reserved memory ** Failed to load 'sel4test-driver-image-arm-bcm2711 I could get around it by using a load address that was smaller by a factor of 0x10.( 0x1000000 instead of 0x10000000 i.e. one less zero). I cannot claim I understand why the first address failed and the second worked. Any pointers on that would help. After the change in the address, I saw the sel4 tests run as expected. x86_64 server ------------------ Spec: Dell R520, two quad-core Xeons (E5-2407 v2 @ 2.40GHz), 32GB of memory. The server's serial is redirected to the IPMI console. On the IPMI console, I see many messages related to the bios, etc. And finally, I see this: MBR SYSLINUX 6.04 EDD [...] Loading sel4kernel... ok Loading rootserver... ok But nothing after this. Any thoughts of what could be going wrong here? I did not see any sel4 prints. x86_64 Desktop ---------------------- Spec: Core 2 Quad, 4 GB ram It was able to find the pinout for the serial port on the motherboard and connected to it(just like for RP). There was no output on the serial console. Even when bios-related messages were printed on the monitor, there was no output on the serial pins. I might need to enable the serial output on those pins in the bios or something similar. Fortunately, even though the serial pins did not have any output, the monitor output was the same as for the server. Unfortunately, it did not get any farther along than the server. MBR SYSLINUX 6.04 EDD [...] Loading sel4kernel... ok Loading rootserver... ok Any pointers here would be helpful. Thanks, Sid UBC Graduate Student ARM Research Intern [1] https://docs.sel4.systems/Hardware/IA32 [2] https://docs.sel4.systems/Hardware/Rpi4.html

2 5

Implementation of SeL4
by Sriram 10 Jun '22

10 Jun '22

Greetings This is Sriram Prakash, currently working on a project on secure system applications for avioics and found the concept and key use case of seL4 microkernel aligned to our main application : creating a secure OS on bareboard application We are facing certain issues as follows: - Booting via flashdrive, Output on Screen shows "Loading sel4 OK","Loading rootserver OK" and no other output in display, we recieved junk values using serial port Output. - We have put up a query on sel4Discourse : https://sel4.discourse.group/t/sel4-vm-linux-boot-in-x86-64-platform-pc/527, about the issues we are facing. - How to receive output in Display - Booting Linux VM on top of seL4 Any insights regarding the issues would be grateful, thank you for your time Regards R.Sriram Prakash

3 2

Running RISC-V seL4 in QEMU 7.0.50
by porter.188＠osu.edu 03 Jun '22

03 Jun '22

Hello, I'm trying to run sel4test in QEMU 7.0.50. I can compile successfully but sel4test hangs at "Jumping to kernel-image entry point...". Is there something different required now that sel4 is using OpenSBI? $ qemu-system-riscv64 -nographic -serial mon:stdio -m size=4095M -bios none -kernel images/sel4test-driver-image-riscv-spike OpenSBI v0.8 ____ _____ ____ _____ / __ \ / ____| _ \_ _| | | | |_ __ ___ _ __ | (___ | |_) || | | | | | '_ \ / _ \ '_ \ \___ \| _ < | | | |__| | |_) | __/ | | |____) | |_) || |_ \____/| .__/ \___|_| |_|_____/|____/_____| | | |_| Platform Name : ucbbar,spike-bare,qemu Platform Features : timer,mfdeleg Platform HART Count : 1 Boot HART ID : 0 Boot HART ISA : rv64imafdcsuh BOOT HART Features : pmp,scounteren,mcounteren BOOT HART PMP Count : 16 Firmware Base : 0x80000000 Firmware Size : 96 KB Runtime SBI Version : 0.2 MIDELEG : 0x0000000000001666 MEDELEG : 0x0000000000f0b509 PMP0 : 0x0000000080000000-0x000000008001ffff (A) PMP1 : 0x0000000000000000-0xffffffffffffffff (A,R,W,X) ELF-loader started on (HART 0) (NODES 1) paddr=[80200000..8066a037] Looking for DTB in CPIO archive...found at 802d2128. Loaded DTB from 802d2128. paddr=[84020000..84020fff] ELF-loading image 'kernel' to 84000000 paddr=[84000000..8401ffff] vaddr=[ffffffff84000000..ffffffff8401ffff] virt_entry=ffffffff84000000 ELF-loading image 'sel4test-driver' to 84021000 paddr=[84021000..843f6fff] vaddr=[10000..3e5fff] virt_entry=1b982 Enabling MMU and paging Jumping to kernel-image entry point...

3 4

UNSW tenure-track position
by Gernot Heiser 01 Jun '22

01 Jun '22

Any recent or soon PhD graduates whose work is around seL4? If os you might be interested in the operating system faculty position we have open at UNSW: https://external-careers.jobs.unsw.edu.au/cw/en/job/502766/lecturersenior-l… Gernot

1 0

Re: Reminder seL4 developer hangout
by Isaac Beckett 31 May '22

31 May '22

Oh boy, 3AM! I hope to make it, but if I sound tired, that’s why. > Date: Mon, 30 May 2022 00:08:16 +0000 > From: Birgit Brecknell <birgit.brecknell(a)unsw.edu.au> > Subject: [seL4] Reminder seL4 developer hangout > To: "devel(a)sel4.systems" <devel(a)sel4.systems> > Message-ID: <MEAPR01MB44693624005ED9CB8CFDD3A7DEDD9(a)MEAPR01MB4469.aus > prd01.prod.outlook.com> > Content-Type: text/plain; charset="iso-8859-1" > > Hi all > > A friendly reminder that the seL4 developer hangout is on again this week: > > Wed, Jun 1, 7am (UTC), Topics: (open) > > * Sydney: Wed, Jun 1, 5pm > * Central Europe: Wed, Jun 1, 9am > * US Pacific Time: Wed, Jun 1, 12 midnight > > 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

2 1

Reminder seL4 developer hangout
by Birgit Brecknell 30 May '22

30 May '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Jun 1, 7am (UTC), Topics: (open) * Sydney: Wed, Jun 1, 5pm * Central Europe: Wed, Jun 1, 9am * US Pacific Time: Wed, Jun 1, 12 midnight 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

Running RISC-V seL4 in QEMU 7.0.50
by porter.188＠osu.edu 28 May '22

28 May '22

Hello, I am trying to run a simple hello world project in seL4 RISC-V in QEMU. It seems to hang at "Jumping to kernel-image entry point..." This same behavior happens on sel4test as well. In the past this was due to a bios option in QEMU changing. Is there something else going on here? I know seL4 uses OpenSBI instead of BBL for RISC-V but is there something else in QEMU or some other switch we need to add? The commands I run are: $ qemu-system-riscv64 -machine spike -cpu rv64 -nographic -serial mon:stdio -m size=4095M -bios none -kernel images/sel4test-driver-image-riscv-spike OpenSBI v0.8 ____ _____ ____ _____ / __ \ / ____| _ \_ _| | | | |_ __ ___ _ __ | (___ | |_) || | | | | | '_ \ / _ \ '_ \ \___ \| _ < | | | |__| | |_) | __/ | | |____) | |_) || |_ \____/| .__/ \___|_| |_|_____/|____/_____| | | |_| Platform Name : ucbbar,spike-bare,qemu Platform Features : timer,mfdeleg Platform HART Count : 1 Boot HART ID : 0 Boot HART ISA : rv64imafdcsuh BOOT HART Features : pmp,scounteren,mcounteren BOOT HART PMP Count : 16 Firmware Base : 0x80000000 Firmware Size : 96 KB Runtime SBI Version : 0.2 MIDELEG : 0x0000000000001666 MEDELEG : 0x0000000000f0b509 PMP0 : 0x0000000080000000-0x000000008001ffff (A) PMP1 : 0x0000000000000000-0xffffffffffffffff (A,R,W,X) ELF-loader started on (HART 0) (NODES 1) paddr=[80200000..8066a037] Looking for DTB in CPIO archive...found at 802d2128. Loaded DTB from 802d2128. paddr=[84020000..84020fff] ELF-loading image 'kernel' to 84000000 paddr=[84000000..8401ffff] vaddr=[ffffffff84000000..ffffffff8401ffff] virt_entry=ffffffff84000000 ELF-loading image 'sel4test-driver' to 84021000 paddr=[84021000..843f6fff] vaddr=[10000..3e5fff] virt_entry=1b982 Enabling MMU and paging Jumping to kernel-image entry point...

1 0

Getting Badge Value of a badged EP capability
by Sid Agrawal 22 May '22

22 May '22

Hi seL4-devs and users, I have a question about implementing server and client using badged endpoints. Below I have laid out the scenario, the issue, and some questions. *Scenario* I have a userspace server that implements the functionality for an object(say type obj_T1). The server hands out badged-endpoints to clients to interact with this object. The badge is the virtual address of the object's struct in the server’s virtual address space. A client can interact with the object by sending messages on this badged endpoint. The client never learns the badge value. The kernel extracts the badged value when the server receives a message on this endpoint. By using the badge value, the server knows which object the client is trying to manipulate. The same PD, which implements the 1st server, also implements another server(in a separate thread, but same address space) for another object type (say type obj_T2). The server follows the same paradigm of handing out badged endpoints and using the badges values to keep track of the object. *Issue* I have a scenario where the client wants to invoke the functionality of obj_T1. This functionality needs access to obj_T2 as well. The client has badged EP caps to both objects. The client can invoke the badged EP handed out by server-1 for obj_T1 and give the badged EP of obj_T2 as an extraCap in the IPC message(or vice versa). Since the server has no way to look up the badge of the second cap, it cannot look up the underlying object for obj_T2. So my questions are: 1. Is there a way for a PD to look up the badge value of badged EP? I think the answer is no, but I thought I would still ask. 2. Is my idea of using the badge to keep track of the underlying object on the right track? Is there a better way of going about doing it? 3. As a potential solution, I can extend my server to add a new function, say GETID, which returns the badge value of a given object(i.e., EP). Since I know that the server always badges the EP with the virtual address of the struct, it is a trivial call to implement. But I somehow feel like this is not a neat idea, not quite sure why. Thanks for the help, everyone! Sid CS Graduate Student @ UBC sid-agrawal.ca

3 7

Untyped tutorial on RISC-V
by inf19109＠lehre.dhbw-stuttgart.de 18 May '22

18 May '22

Dear seL4 devs and community, I'm trying to do the seL4-tutorials on a RISC-V architecture. Now I'm stuck on the untyped tutorial. I tried to run the solution of the tutorial but I get the following error: <<seL4(CPU 0) [decodeUntypedInvocation/128 T0xffffffc17fee7200 "rootserver" @103fc]: Untyped Retype: Destination cap invalid or read-only.>> main@main.c:48 [Cond failed: error != seL4_NoError] Failed to retype seL4 root server abort()ed Debug halt syscall from user thread 0xffffffc17fee7200 "rootserver" halting... I'm calling the function as follows: seL4_Untyped_Retype(parent_untyped, seL4_UntypedObject, // type untyped_size_bits, //size seL4_CapInitThreadCNode, // root 0, // node_index 0, // node_depth child_untyped, // node_offset 1 // num_caps ); parent_untyped = info->untyped.start + i (where i is incremented until (info->untypedList[i].sizeBits >= untyped_size_bits && !info->untypedList[i].isDevice) untyped_size_bits = seL4_TCBBits+1 child_untyped = info->empty.start It seams as if the function is not allowed for RISC-V. I don't know where the problem lies and I would appreciate any help or ideas. Best regards Miriam

2 3

Reminder seL4 developer hangout
by Birgit Brecknell 16 May '22

16 May '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, May 17, 10pm (UTC), Topics: (open) * Sydney: Wed, May 18, 8am * Central Europe: Wed, May 18, 12 midnight * US Pacific Time: Tue, May 17, 3pm 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

VPPI IRQ 27 dropped on vcpu 3
by Han JingLong 韩景龙 11 May '22

11 May '22

Dear seL4 devs and community, I had made VMM work well on my platform(armv8, six A55 cpus, RAM is 8G) based on vm_multi with Linux Guest OS(vm0.num_vcpus = 4;) and Android Guest OS(vm1.num_vcpus = 6;). But I meet an error(vm_vppi_event_handler@vm.c:97 VPPI IRQ 27 dropped on vcpu 3) when I enable SMP support with -DNUM_NODES=6. Actually, VPPI IRQ 27 dropped on some vcpu number is not fixed, maybe 1 or 2 or 3. Once this error appears, it will brush the screen crazily, the recurrence rate is about 10%. 1.Some logs are added for debugging this issue: --- a/seL4_projects_libs/libsel4vmmplatsupport/src/arch/arm/psci.c +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/arch/arm/psci.c @@ -53,18 +53,24 @@ int handle_psci(vm_vcpu_t *vcpu, seL4_Word fn_number, bool convention) uintptr_t target_cpu = smc_get_arg(&regs, 1); uintptr_t entry_point_address = smc_get_arg(&regs, 2); uintptr_t context_id = smc_get_arg(&regs, 3); + printf("[hjl] handle_psci target_cpu:%d\n", target_cpu); vm_vcpu_t *target_vcpu = vm_vcpu_for_target_cpu(vcpu->vm, target_cpu); if (target_vcpu == NULL) { target_vcpu = vm_find_free_unassigned_vcpu(vcpu->vm); if (target_vcpu && start_new_vcpu(target_vcpu, entry_point_address, context_id, target_cpu) == 0) { + printf("[hjl] handle_psci vm:%p vcpu_id:%d on success\n", vcpu->vm, target_vcpu->vcpu_id); smc_set_return_value(&regs, PSCI_SUCCESS); } else { + printf("[hjl] handle_psci vm:%p vcpu_id:%d on failure\n", vcpu->vm, target_vcpu->vcpu_id); smc_set_return_value(&regs, PSCI_INTERNAL_FAILURE); } } else { if (is_vcpu_online(target_vcpu)) { + printf("[hjl] handle_psci vm:%p target_cpu is online\n", vcpu->vm); smc_set_return_value(&regs, PSCI_ALREADY_ON); } else { + printf("[hjl] handle_psci vm:%p target_cpu is not online\n", vcpu->vm); smc_set_return_value(&regs, PSCI_INTERNAL_FAILURE); } } --- a/seL4_projects_libs/libsel4vm/src/arch/arm/vgic/vgic.c +++ b/seL4_projects_libs/libsel4vm/src/arch/arm/vgic/vgic.c @@ -570,6 +570,9 @@ static int vgic_dist_enable_irq(struct vgic_dist_device *d, vm_vcpu_t *vcpu, int vgic = vgic_device_get_vgic(d); DDIST("enabling irq %d\n", irq); set_enable(gic_dist, irq, true, vcpu->vcpu_id); + if (irq == 27) { + printf("[hjl] enabling irq:%d on vcpu:%d\n", irq, vcpu->vcpu_id); + } virq_data = virq_find_irq_data(vgic, vcpu, irq); if (virq_data) { /* STATE b) */ @@ -619,6 +622,7 @@ static int vgic_dist_set_pending_irq(struct vgic_dist_device *d, vm_vcpu_t *vcpu return err; } else { + printf("[hjl] virq_data:%p, gic_dist->enable:%d, is_enabled:%d\n", virq_data, gic_dist->enable, is_enabled(gic_dist, irq, vcpu->vcpu_id)); /* No further action */ DDIST("IRQ not enabled (%d) on vcpu %d\n", irq, vcpu->vcpu_id); return -1; } 2.The detailed log is as follows: [hjl] enabling irq 27, vcpu->vcpu_id:0 [hjl] handle_psci target_cpu:256 [hjl] handle_psci vm:0x1584bbb0 vcpu_id:1 on success [hjl] enabling irq 27, vcpu->vcpu_id:1 [hjl] handle_psci target_cpu:512 [hjl] handle_psci vm:0x1584bbb0 vcpu_id:2 on success [hjl] enabling irq 27, vcpu->vcpu_id:2 [hjl] handle_psci target_cpu:768 [hjl] handle_psci vm:0x1584bbb0 vcpu_id:3 on success [hjl] enabling irq 27, vcpu->vcpu_id:3 [hjl] enabling irq 27, vcpu->vcpu_id:0 [hjl] handle_psci target_cpu:256 [hjl] handle_psci vm:0x1584fbb0 vcpu_id:1 on success [hjl] enabling irq 27, vcpu->vcpu_id:1 [hjl] handle_psci target_cpu:512 [hjl] handle_psci vm:0x1584fbb0 vcpu_id:2 on success [hjl] enabling irq 27, vcpu->vcpu_id:2 [hjl] handle_psci target_cpu:768 [hjl] handle_psci vm:0x1584fbb0 vcpu_id:3 on success [hjl] enabling irq 27, vcpu->vcpu_id:3 [hjl] IRQ not enabled (27) on vcpu 3 virq_data:0x15794ad0, gic_dist->enable:1, is_enabled:0 vm_vppi_event_handler@vm.c:97 VPPI IRQ 27 dropped on vcpu 3 [hjl] IRQ not enabled (27) on vcpu 3 virq_data:0x15794ad0, gic_dist->enable:1, is_enabled:0 vm_vppi_event_handler@vm.c:97 VPPI IRQ 27 dropped on vcpu 3 ...... 3.Present situation: At present, I tracked and found that secondary cpus has been on by Host, but Guest OS's secondary_start_kernel function seem like not excuted. Does anyone know what caused it? BR. Allen 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

camkes q's
by Sam Leffler 11 May '22

11 May '22

1. I need multiple VSpace "holes" to map page frames. This is the equivalent of what capdl_loader_app sets up in init_copy_frame. To do this I setup named static arrays and unmap the frame caps in camkes.c:post_main. This works but using a per-component attribute to enable this was awkward so I ended up adding a "copyregion" primitive to camkes. Is there a way to do this without adding to the camkes' syntax? It would also be nice not to allocate page frames only to release them at start but I didn't see a way to do this in capdl; is it possible (e.g. an easy way to leave an empty slot in the pt/pd)? 2. I pass capabilities with ipc msgs using camkes' rpc-connector templates. This requires multiple small changes that I want to enable only when being used (e.g. parameters to seL4_MessageInfo_new). My current plan is to add an optional keyword to a connection defn to enable support; e.g. connection seL4RPCCall foo(xfer_caps, from a, to b); Does this make sense or is there a better way? I rejected creating new connector templates that enable xfer_caps because I see this as a concept that applies to any ipc-based connector.

2 2

Information for Smmuv3 support of Sel4
by Tao Heng 陶恒-SW 06 May '22

06 May '22

Hi, list We are trying to porting Sel4 Vmm project on our platform.But we found there was no information about smmuv3 support of Sel4. Do you have some related development work for supporting this? Or can you give us some advice for supporting Smmuv3 on Sel4? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

One week left to propose a talk at the seL4 summit 2022!
by June Andronick (seL4 Foundation) 06 May '22

06 May '22

A reminder that you have until Monday 9th of May 2022 to propose a talk for the seL4 Summit 2022 :) http://sel4.systems/news/2022 <http://sel4.systems/news/2022> http://sel4.systems/Foundation/Summit/ <http://sel4.systems/Foundation/Summit/> http://sel4.systems/Foundation/Summit/cfp <http://sel4.systems/Foundation/Summit/cfp>

1 1

Reminder seL4 developer hangout
by Birgit Brecknell 02 May '22

02 May '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, May 4, 7am (UTC), Topics: (open) * Sydney: Wed, May 4, 5pm * Central Europe: Wed, May 4, 9am * US Pacific Time: Wed, May 4, 12 midnight 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

The seL4 Summit 2022 will be in Munich, Germany, on 10-12 Oct 2022
by June Andronick (seL4 Foundation) 29 Apr '22

29 Apr '22

It is our pleasure to confirm that the seL4 Summit 2022 will be in: Munich, Germany in the week of Oct 10th, 2022 It will be hosted by seL4 Foundation member Hensoldt Cyber. It will be a hybrid in-person/online event (if you'd like to propose a talk to be delivered remotely, please notify it in the submission). Remember that you have until Monday 9th of May 2022 to propose a talk. https://sel4.systems/news/2022 https://sel4.systems/Foundation/Summit/ https://sel4.systems/Foundation/Summit/cfp

1 0

Sending extraCaps over IPC | Unable to send 2 caps
by Sid Agrawal 29 Apr '22

29 Apr '22

Hello seL4 devs and users, I am trying to send two capabilities from one process to another via the extraCaps mechanism in the IPC. I can get it working when I send just 1 cap, but when I am sending 2 caps, the 2nd one never makes it. The extraCaps field on the receiver side is somehow always 1. Looking at the seL4 manual, I understood that I could send more than 1 capability via an IPC. But since on the receiver side, I can only specify one receive slot, I assumed that if more than 1 capability is received, it will be put in the consecutive slots. Not sure if this is a valid assumption. Looking at kerne/libsel4/include/sel4/constants.h <https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/constants.h#L…>, I see that seL4_MsgMaxExtraCaps is set to 2, so I think I should be able to send 2 caps. I have spent about 3 days trying to make this work and thought that at this stage, it would be best to ask :) My C code on the sender side looks something like this: seL4_CPtr cap1 = <alloc some capability> seL4_CPtr cap2 = <alloc some capability> seL4_SetMR(0, 0xabcd); seL4_SetCap(0, cap1); seL4_SetCap(1, cap2); seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 2, 1); tag = seL4_Call(receivers_ep_cap, tag); On the receive side, the code looks something like this: /* Allocate one csapce slot */ cspacepath_t received_cap_path_1; error = vka_cspace_alloc_path(simple-vka, &received_cap_path_1); <- slot = 2786 assert(error == 0); /* Allocate another csapce slot */ cspacepath_t received_cap_path_2; error = vka_cspace_alloc_path(simple-vka, &received_cap_path_2); <- slot = 2785(somehow decreasing) assert(error == 0); /* Since the allocated slots are decreasing in count, I pick the lesser one as my first slot * assuming that if more than 1 cap is received it will be put in the next slot */ seL4_CPtr min_cptr = MIN(received_cap_path_1.capPtr, received_cap_path_2.capPtr); seL4_SetCapReceivePath( /* _service */ received_cap_path.root, /* index */ min_cptr, /* depth */ received_cap_path.capDepth); tag = recv(&sender_badge); assert(seL4_MessageInfo_get_extraCaps(tag) == 2); <--- This asser fails. Thanks again!! Sid Graduate Student @ UBC

2 2

RTReply and cap xfer
by Sam Leffler 22 Apr '22

22 Apr '22

The kernel supports attaching a capability to an RTReply xfer. sel4test even checks this WAI. But capdl doesn't seem to support it as I see no way to express the set of rights associated with a capability to an RTReply object. I added capdl support so I can mark the Grant right and verified cap xfer works. TWas this intentional? -Sam

1 0

Running vm_multi app on qemu-arm-virt platform, udhcpc can not return
by ybbekele＠aggies.ncat.edu 22 Apr '22

22 Apr '22

Hi, I tried to build vm_multi for qemu-arm-virt using the procedures in this link https://docs.sel4.systems/projects/camkes-vm/. After building, I used the generated simulation file to do ./simulate in my build directory. After displaying 'welcome to buildroot', the console always prints the log "udhcpc: sending discover",which indicates udhcpc can not return. The related log was shown below: Starting syslogd: OK Starting syslogd: OK Starting syslogd: OK Starting klogd: OK Starting klogd: OK Starting klogd: OK Running sysctl: OK Running sysctl: OK Running sysctl: OK Initializing random number generator... [ 7.195263] random: dd: uninitialized urandom read (512 bytes read) done. Initializing random number generator... [ 7.315113] random: dd: uninitialized urandom read (512 bytes read) done. Initializing random number generator... [ 7.300770] random: dd: uninitialized urandom read (512 bytes read) done. Starting network: OK Starting network: OK Starting network: OK udhcpc: started, v1.31.0 udhcpc: started, v1.31.0 ifconfig: SIOCGIFFLAGS: No such device [ 9.077855] random: mktemp: uninitialized urandom read (6 bytes read) [ 9.177878] random: mktemp: uninitialized urandom read (6 bytes read) Welcome to Buildroot udhcpc: sending discover udhcpc: sending discover udhcpc: sending discover udhcpc: sending discover As the simulation process progresses there was an error: _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0x10080000 alloc_vm_device_cap@main.c:938 Grabbing the entire cap for device memory alloc_vm_device_cap@main.c:941 Failed to grab the entire cap My question is: 1. Is the two things have dependencies (The error and the hang at booting the system up)? 2. How can this issue be solved? 3. Is this issue related to the TimeServer component being imported to Qemu (as this is indicated as a requirement to run multi_vm on qemu-arm-virt)? Thank you for your time

1 0

Why vppi is sent from kernel to vmm by fault endpoint but not by notification ?
by wtliang785 21 Apr '22

21 Apr '22

hello devel, Why vppi , such as vtimer interrupt to guest, is sent from kernel to vmm by fault endpoint but not by notification? I see that spi to guest is sent from kernel to vmm by notification. thank you.

1 0

Reminder seL4 developer hangout/video call
by Gerwin Klein 19 Apr '22

19 Apr '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Apr 19, 10pm (UTC) * Sydney: Wed, Apr 20, 8am * Central Europe: Wed, Apr 20, 12 midnight * US Pacific Time: Tue, Apr 19, 3pm Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

1 0

Re: Combatting spam on this list
by Isaac Beckett 13 Apr '22

13 Apr '22

Thanks Peter! In my experience posts like that, linking to pornographic websites, are not made by humans anyway, but rather by bots. I don’t think this will effect humans too much except at the very beginning. It may make sense to implement a different captcha, as often the developers of those bots can outsource solving common captcha providers to underpaid humans. Using an uncommon or home-grown captcha solution will make it less likely that bots will be able to get around them using that method. And attacks like these aren’t targeted, usually, so I doubt the bot writers will adapt for one specific mailing list. That will stop bots from signing up in the first place, hopefully. We could also maybe report abuse of free email services like Gmail or Hotmail or similar in a semi-automated fashion. Would not surprise me if there is some sort of API for that. But on the other hand with the way those companies work it could be a waste of time and effort, since they might not do anything. And it may also make sense to keep track of which domains non-malicious users are sending email from. That way we can ban entire domains without worrying about getting rid of legitimate users unintentionally. For example, a small webmail service that we may not realize is a public email service at first, could be used by both a malicious user and a legitimate one. That way we’re only banning domains controlled by spammers exclusively. There’s lots of resources for this stuff thankfully, you can go on a whole tangent reading about email spam prevention on Wikipedia. I wish you luck with figuring out how to stop this annoying nonsense.

3 2

Unrecognized OPCODE fence.i/csrw
by porter.188＠osu.edu 13 Apr '22

13 Apr '22

I'm trying to setup a development machine for seL4 work. I would like to use v12.1.0. I setup seL4test-manifest per instructions here https://docs.sel4.systems/Hardware/spike.html repo init -u https://github.com/seL4/sel4test-manifest.git repo sync mkdir cbuild cd cbuild ../init-build.sh -DPLATFORM=spike -DRISCV64=1 # The default cmake wrapper sets up a default configuration for the target platform. # To change individual settings, run `ccmake` and change the configuration # parameters to suit your needs. ninja # If your target binaries can be executed in an emulator/simulator, and if # our build system happens to support that target emulator, then this script # might work for you: ./simulate I used repo init -u https://github.com/seL4/sel4test-manifest.git -b refs/tags/12.1.0 to be sure I got 12.1.0 but it doesn't matter, both branches/tags give the same error when I configure/compile. $ ../init-build.sh -DPLATFORM=spike -DRISCV64=1 -DSIMULATION=1 loading initial cache file /mnt/data/sel4test/projects/sel4test/settings.cmake -- Set platform details from PLATFORM=spike -- KernelPlatform: spike -- Setting from flags KernelSel4Arch: riscv64 -- Found seL4: /mnt/data/sel4test/kernel -- Found GCC with prefix riscv64-unknown-linux-gnu- -- Found GCC with prefix riscv64-unknown-linux-gnu- -- The C compiler identification is GNU 10.2.0 -- The CXX compiler identification is GNU 10.2.0 -- The ASM compiler identification is GNU -- Found assembler: /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-gcc -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Check for working C compiler: /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-gcc - skipped -- Detecting C compile features -- Detecting C compile features - done -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Check for working CXX compiler: /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-g++ - skipped -- Detecting CXX compile features -- Detecting CXX compile features - done -- Found elfloader-tool: /mnt/data/sel4test/tools/seL4/elfloader-tool -- /mnt/data/sel4test/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating... -- CPIO test cpio_reproducible_flag PASSED -- Found musllibc: /mnt/data/sel4test/projects/musllibc -- Found util_libs: /mnt/data/sel4test/projects/util_libs -- Found seL4_libs: /mnt/data/sel4test/projects/seL4_libs -- Found sel4_projects_libs: /mnt/data/sel4test/projects/sel4_projects_libs -- Found sel4runtime: /mnt/data/sel4test/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- libmuslc architecture: 'riscv' (from KernelSel4Arch 'riscv64') -- Detecting cached version of: musllibc -- Found Git: /usr/bin/git (found version "2.25.1") -- Not found cache entry for musllibc - will build from source -- Found PythonInterp: /usr/bin/python (found version "2.7.18") CMake Warning (dev) at /home/user/.local/lib/python3.8/site-packages/cmake/data/share/cmake-3.22/Modules/FindPackageHandleStandardArgs.cmake:438 (message): The package name passed to `find_package_handle_standard_args` (NANOPB) does not match the name of the calling package (Nanopb). This can lead to problems in calling code that expects `find_package` result variables (e.g., `_FOUND`) to follow a certain pattern. Call Stack (most recent call first): /mnt/data/sel4test/tools/nanopb/extra/FindNanopb.cmake:340 (FIND_PACKAGE_HANDLE_STANDARD_ARGS) /mnt/data/sel4test/tools/seL4/cmake-tool/helpers/nanopb.cmake:29 (find_package) /mnt/data/sel4test/projects/sel4_projects_libs/libsel4nanopb/CMakeLists.txt:11 (include) This warning is for project developers. Use -Wno-dev to suppress it. -- Found NANOPB: /mnt/data/sel4test/tools/nanopb -- Configuring done -- Generating done -- Build files have been written to: /mnt/data/sel4test/build user@user-KVM:/mnt/data/sel4test/build$ ninja [42/267] Building ASM object kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj FAILED: kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj /usr/bin/ccache /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-gcc --sysroot=/mnt/data/sel4test/build -I/mnt/data/sel4test/kernel/include/plat/default -I/mnt/data/sel4test/kernel/include -I/mnt/data/sel4test/kernel/include/64 -I/mnt/data/sel4test/kernel/include/arch/riscv -I/mnt/data/sel4test/kernel/include/arch/riscv/arch/64 -I/mnt/data/sel4test/kernel/include/plat/spike -I/mnt/data/sel4test/kernel/include/plat/spike/plat/64 -I/mnt/data/sel4test/kernel/libsel4/include -I/mnt/data/sel4test/kernel/libsel4/arch_include/riscv -I/mnt/data/sel4test/kernel/libsel4/sel4_arch_include/riscv64 -I/mnt/data/sel4test/kernel/libsel4/sel4_plat_include/spike -I/mnt/data/sel4test/kernel/libsel4/mode_include/64 -I/mnt/data/sel4test/build/kernel/gen_config -I/mnt/data/sel4test/build/kernel/autoconf -I/mnt/data/sel4test/build/kernel/gen_headers -I/mnt/data/sel4test/build/kernel/generated -march=rv64imac -mabi=lp64 -D__KERNEL_64__ -O2 -g -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mcmodel=medany -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -MD -MT kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj -MF kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj.d -o kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj -c /mnt/data/sel4test/kernel/src/arch/riscv/head.S /mnt/data/sel4test/kernel/src/arch/riscv/head.S: Assembler messages: /mnt/data/sel4test/kernel/src/arch/riscv/head.S:24: Error: unrecognized opcode `fence.i' /mnt/data/sel4test/kernel/src/arch/riscv/head.S:31: Error: unrecognized opcode `csrw sscratch,x0' [44/267] Invoking muslc build system /mnt/data/sel4test/projects/musllibc/src/unistd/getcwd.c: In function 'getcwd': cc1: warning: function may return address of local variable [-Wreturn-local-addr] /mnt/data/sel4test/projects/musllibc/src/unistd/getcwd.c:9:7: note: declared here 9 | char tmp[PATH_MAX]; | ^~~ ninja: build stopped: subcommand failed. I tried riscv-gcc 10.2.0 and 11.1.0 with the same results. $ riscv64-unknown-linux-gnu-gcc --version riscv64-unknown-linux-gnu-gcc (gca312387ab1) 10.2.0 Copyright (C) 2020 Free Software Foundation, Inc. This is free software; see the source for copying conditions. There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. Is there some extension I need to add to get this working? Where do I do that?

2 2

答复: Report "Failed to touch ram region" error using virtio_console when assigned for Arm-VM more than 3G memory
by Han JingLong 韩景龙 12 Apr '22

12 Apr '22

Hi The root cause of this problem has been found, when Guest OS do the virtio console driver probe, if virtqueue's desc addr allocated by alloc_pages_exact() in the setup_vq() function is >= 0x100000000 (it is common when the memory of VM allocated exceeds 3G), at first It will be shifted right 12 bits by Guest OS(turn into a value >= 0x100000), and then use iowrite32(iobase + VIRTIO_PCI_QUEUE_PFN) to notify Host, after unsigned int type data be shifted left 12 bits by Host, the higest bits 0x1 of virtqueue's desc addr will be lost. I have submitted a PR for the amendment, waiting for the review and merge into the main branch. https://github.com/seL4/seL4_projects_libs/pull/43 BR. Allen 发件人: Han JingLong 韩景龙发送时间: 2022年3月21日 20:27 收件人: 'devel(a)sel4.systems' <devel(a)sel4.systems> 主题: Report "Failed to touch ram region" error using virtio_console when assigned for Arm-VM more than 3G memory Hi I had make virtio_console work well on my environment(armv8, RAM is 8G) based on vm_multi with Linux Guest OS(512M) and Android Guest OS(<= 3G) But I meet an error(vm_ram_touch@guest_ram.c:157<mailto:vm_ram_touch@guest_ram.c:157> Failed to touch ram region: Not registered RAM region) when assign for a VM(Android Guest OS) more than 3G memory. 1. Some logs are added for debugging this issue： +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c @@ -86,6 +86,7 @@ static int emul_io_out(virtio_emul_t *emul, unsigned int offset, unsigned int si assert(size == 4); int queue = emul->virtq.queue; emul->virtq.queue_pfn[queue] = value; + printf("[hjl] queue_size:%d desc:%p\n", emul->virtq.queue_size[queue], (void *)(uintptr_t)(value << 12)); vring_init(&emul->virtq.vring[queue], emul->virtq.queue_size[queue], (void *)(uintptr_t)(value << 12), VIRTIO_PCI_VRING_ALIGN); break; +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul_helpers.c @@ -25,10 +25,43 @@ static int write_guest_mem(vm_t *vm, uintptr_t phys, void *vaddr, size_t size, s int vm_guest_write_mem(vm_t *vm, void *data, uintptr_t address, size_t size) { + bool is_inram = false; + vm_mem_t *guest_memory = &vm->mem; + for (int i = 0; i < guest_memory->num_ram_regions; i++) { + if (guest_memory->ram_regions[i].start <= address && + guest_memory->ram_regions[i].start + guest_memory->ram_regions[i].size >= address + size) { + /* We are within a ram region*/ + is_inram = true; + } + } + + if (!is_inram) { + printf("[hjl] write mem addr:%p size:0x%lx\n", address, size); + for (int index = 0; index < guest_memory->num_ram_regions; index++) { + printf("[hjl] write mem ram_regions start:%p size:0x%lx\n", guest_memory->ram_regions[index].start, guest_memory->ram_regions[index].size); + } + } + return vm_ram_touch(vm, address, size, write_guest_mem, data); } int vm_guest_read_mem(vm_t *vm, void *data, uintptr_t address, size_t size) { + bool is_inram = false; + vm_mem_t *guest_memory = &vm->mem; + for (int i = 0; i < guest_memory->num_ram_regions; i++) { + if (guest_memory->ram_regions[i].start <= address && + guest_memory->ram_regions[i].start + guest_memory->ram_regions[i].size >= address + size) { + /* We are within a ram region*/ + is_inram = true; + } + } + + if (!is_inram) { + printf("[hjl] read mem addr:%p size:0x%lx\n", address, size); + for (int index = 0; index < guest_memory->num_ram_regions; index++) { + printf("[hjl] read mem ram_regions start:%p size:0x%lx\n", guest_memory->ram_regions[index].start, guest_memory->ram_regions[index].size); + } + } return vm_ram_touch(vm, address, size, read_guest_mem, data); } 2. The detailed log is as follows: [hjl] queue_size:128 desc:0x8eb6000 [hjl] queue_size:128 desc:0x8eb8000 [hjl] read mem addr:0x8eb8802 size:0x2 [hjl] read mem ram_regions start:0x80000000 size:0x80000 [hjl] read mem ram_regions start:0x80080000 size:0x17cda00 [hjl] read mem ram_regions start:0x8184da00 size:0xa5b2600 [hjl] read mem ram_regions start:0x8be00000 size:0x83ae98 [hjl] read mem ram_regions start:0x8c63ae98 size:0x29c5168 [hjl] read mem ram_regions start:0x8f000000 size:0x26d35 [hjl] read mem ram_regions start:0x8f026d35 size:0xc0fd92cb vm_ram_touch@guest_ram.c:157<mailto:vm_ram_touch@guest_ram.c:157> Failed to touch ram region: Not registered RAM region 3. devices.camkes configuration reference is as follows: #define VM1_RAM_BASE 0x80000000 #define VM1_RAM_SIZE 0xD0000000 #define VM1_DTB_ADDR 0x8F000000 //VM1_RAM_BASE + 0xF000000 #define VM1_INITRD_ADDR 0x8BE00000 //VM1_DTB_ADDR - VM1_INITRD_MAX_SIZE vm1.untyped_mmios = [ "0x80000000:28", // RAM "0x90000000:28", // RAM "0xa0000000:28", // RAM "0xb0000000:28", // RAM "0xc0000000:28", // RAM "0xd0000000:28", // RAM "0xe0000000:28", // RAM "0xf0000000:28", // RAM "0x100000000:28", // RAM "0x110000000:28", // RAM "0x120000000:28", // RAM "0x130000000:28", // RAM "0x140000000:28", // RAM /* "0x150000000:28", // RAM "0x160000000:28", // RAM "0x170000000:28", // RAM "0x180000000:28", // RAM "0x190000000:28", // RAM "0x1a0000000:28", // RAM "0x1b0000000:28", // RAM */ ]; 4. Present situation: At present, I tracked and found that When the Guest OS's virtio_console driver do the probe, it created the vring and iowrite to notify VMM of the virtqueue desc 's physical address in setup_vq() /* create the vring */ static void *vring_alloc_queue(struct virtio_device *vdev, size_t size, dma_addr_t *dma_handle, gfp_t flag) { ...... void *queue = alloc_pages_exact(PAGE_ALIGN(size), flag); if (queue) { phys_addr_t phys_addr = virt_to_phys(queue); *dma_handle = (dma_addr_t)phys_addr; /* activate the queue */ iowrite32(virtqueue_get_desc_addr(vq) >> VIRTIO_PCI_QUEUE_ADDR_SHIFT, vp_dev->ioaddr + VIRTIO_PCI_QUEUE_PFN); I'm very confused why is the physical memory allocated for virtqueue desc not within the effective memory range of VM when assign the memory to it exceeds 3G? BR. Allen 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

Combatting spam
by David Barrass 12 Apr '22

12 Apr '22

Hi Peter, Thank you for raising this issue - it is an annoying distraction. The general standard of the list is very high as one would expect and it is a shame to see this kind of behaviour polluting the discussions. I am very happy to have to earn a privilege to post and am happy for anything I post to be moderated. I would welcome any proposition to keep spammers off the list whilst keeping it open but I don't think any solution should impose additional burdens on the moderators. I think that this warrants a bit of thought and will give this some consideration. Your proposal sounds good and I support it. In the meantime thank you and many thanks to all the team who make this happen. I find the work on seL4 very valuable and relevant. best regards to all, David

1 0

Combatting spam on this list
by Peter Chubb 12 Apr '22

12 Apr '22

Hi Folks, We're trying hard to avoid spam coming through this list. In particular we moderate all emails coming from non-members, and only let through on-topic postings. Recently, however, we've had some people join the list, and then posting spam. I'm proposing that the first post a person makes will always be moderated; and we'll turn off the moderation after the first on-topic posting. Anyone who posts spam will have that address marked as discard immediately. This means that *all* next posts will be moderated until I or one of the other moderators lets them through, because I'll be changing the default processing. Comments? I'd rather keep things as open as possible, but spammers are making it hard. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

1 0

RFC 10
by Gerwin Klein 11 Apr '22

11 Apr '22

This is a last call for comments for RFC-10 before the TSC votes on it this week: https://sel4.atlassian.net/browse/RFC-10 The RFC is about consolidating AArch64 page table objects and has been uncontroversial so far, just wanted to make sure people are aware of it. Cheers, Gerwin

2 1

Does the lastest master branch support gic v3 virtulization?
by wtliang785 10 Apr '22

10 Apr '22

hello devel, We want to use Sel4 in our project, but the gic version is v3. I know sel4 kernel 12.1.0 version does not support v3 virtuliazation. My question is that what is the status for supporting the v3 virtulization in lastest sel4 kernel master branch? Does the lastest master branch support gic v3 virtulization? thank you Peter Wang

2 1

capDL-tool fix for empty CNode slots
by Sam Leffler 07 Apr '22

07 Apr '22

If you generate capdl for a CNode with empty slots, capDL-tool incorrectly calculates CDL_CapMap::num because it uses Map.size which doesn't include empty slots. The right way to calculate "num" is by taking the max of the key values +1. diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs index ec0eda9..b4a2cbb 100644 --- a/capDL-tool/CapDL/PrintC.hs +++ b/capDL-tool/CapDL/PrintC.hs @@ -224,7 +224,7 @@ memberSlots objs obj_id slots irqNode cdt ms = showSlots objs obj_id (Map.toList slots) irqNode cdt ms +++ "}," where - slot_count = Map.size slots + slot_count = if Map.null slots then 0 else (fst $ Map.findMax slots) + 1 printInit :: [Word] -> String printInit argv = -Sam

2 3

Interrupt handling - General Purpose Timer
by JENKINSON Mark 07 Apr '22

07 Apr '22

Hi seL4 Devel, We are trying to use the General Purpose Timer1 for our i.MX8MQ-based board within a simple CAmkES app. GPT1 is initialising and starting OK, but the interrupt handler for handling rollover is not being triggered. Through instrumenting the code with printf's, the GPT initialisation looks reasonable, and the expected rollover interrupt is being generated and seen within handleInterrupt(); however, the interrupt handler routine that has been registered is not being called. I'm hoping that someone can give me some ideas where to investigate next please? A few more details: From gpt_init() (in util_libs/libplatsupport/src/mach/imx/gpt.c), instrumentation within allocate_irq_callback() confirms that, for: gpt->irq_id = ps_irq_register(&gpt->io_ops.irq_ops, irq, gpt_handle_irq, gpt); our values are: irq->type = 3; // PS_INTERRUPT irq->irq.number = 87 (0x57); // 55 (0x37) + 32 = 87 (0x57) which agrees with the GPT1 entry from our dts file (when combined with the offset of 32, which I've seen explained elsewhere): gpt@302d0000 {... reg = < 0x302d0000 0x10000 >; interrupts = < 0x00 0x37 0x04 >;... And gpt_handle_irq() is registered as the interrupt handler, which resets the rollover flag and manages the counter's high_bits variable. Resulting from this call to ps_irq_register(), gpt->irq_id = 27 (0x1b), although I'm not sure of the significance of this irq_id value. Our test app starts GPT1. After ~3 mins, the timer rolls over, as expected. Instrumentation in handleInterrupt(irq) is triggered with: irq = 87 (0x57); // as expected, the GPT1 rollover interrupt However, gpt_handle_irq() is never called, despite being associated with irq 87 back in the ps_irq_register() call. Instrumentation in handleInterrupt() shows that the IRQSignal case is executed and sendSignal() is called. Within sendSignal, the NtfnState_Idle case is executed, calling ntfn_set_active(ntfnPtr, badge), with badge = 1. I stop tracking the flow there, but pick up again that ackInterrupt() is visited with irq = 87 (0x57). Everything looks in order (the right interrupt is generated at the right time and is detected) except gpt_handle_irq() is not called. The timer app keeps ticking away, but without the rollover management, time ends up skipping. Thanks for your help, Mark. This message contains information that may be privileged or confidential and is the property of the Capgemini Group. It is intended only for the person to whom it is addressed. If you are not the intended recipient, you are not authorized to read, print, retain, copy, disseminate, distribute, or use this message or any part thereof. If you receive this message in error, please notify the sender immediately and delete all copies of this message.

1 0

OpenPower/PowerPC/ppc64le port: major concerns and obstacles
by Isaac Beckett 06 Apr '22

06 Apr '22

Hello seL4 devel! Recently I was on the developer hangout meeting and brought up a ppc port. Interest seemed low, and some even called ppc a “niche” architecture which seems unfair. There was also the much more concrete concerns of funding and overall maintenance. I believe an PPC port would be very valuable, and I plan to do a whole essay/write up of some sort, but I am also not the most familiar with the technical challenges, and could use more information on those. I do think there is definitely people who would want to run seL4 on PowerPC platforms. PowerPC is one of the few ISAs that has existing, modern hardware without closed-source binary blobs, which I believe pose a real threat to the trustworthiness of the hardware seL4 is currently capable of running on.

2 1

A way to reclaim initial thread resources
by Marcin Witkowski 06 Apr '22

06 Apr '22

Hey, I am currently looking for a way to reclaim resources allocated by kernel for the rootserver thread, i.e. memory for CNode, TCB, BootInfo, etc. My current approach looks like this: * in rootserver instead of calling seL4_TCB_Suspend, call custom syscall seL4_ReclaimRootserverResources. This sycall as parameters takes CNode and slot no. after which kernel should be able to freely write new caps. This CNode is main CNode of some component initialized by the rootserver. * implmenetation of this syscall then suspends initial thread, schedules new thread, revokes most of rootserver's resources, notably TCB, BootInfo, IPCBuffer, VSpace and CNode. Then for those now free memory regions new untyped capabilities are created, with the same sizes as the original objects. Lastly, new capabilities are written to subsequent slots in CNode a'la boot.c, so with null MDBNode; mdbRevocable and mdbFirstBadged set to true. This solution has couple of problems. First and foremost, it requires creating additional syscall to handle this. Secondly, even though the component _technically_ has access to this newly created capabilities, it doesn't know where they are, or how big they are. This could be partially band-aided by hardcoding this information in relevant component, but that is far from elegant. This component also recives rest of the untyped memory from rootserver, including bootinfo entries about this memory specification, so that renders solution with hardcoding spec even worse. Last but not least, before the seL4_ReclaimRootserverResources is called, all the components are resumed using seL4_TCB_Resume as part of rootserver's work, so there could be race-condition between calling reclaiming syscall, and component initialization (although I am not 100% sure about that part) Is there maybe a better way to do it, and I am doing it all round? The perfect solution would be to somehow extend bootinfo and/or remaining untypeds that were given by the kernel to the rootserver.

2 3

Reminder seL4 developer hangout/video call
by Birgit Brecknell 04 Apr '22

04 Apr '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: Wed, Apr 6, 7am (UTC), Topics: (open) * Sydney: Wed, Apr 6, 5pm * Central Europe: Wed, Apr 6, 9am * US Pacific Time: Wed, Apr 6, 12 midnight (There are too many time zones in the world to cite them all :-)) 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

3 2

The Call for Presentations for the seL4 summit 2022 is out!
by June Andronick (seL4 Foundation) 01 Apr '22

01 Apr '22

We are calling for proposals to present at the seL4 Summit 2022! Share your seL4 work. Share your seL4 experience. Share your seL4 thoughts. Share your seL4 questions. Check the full Call For Presentations and topics of interest at: https://sel4.systems/Foundation/Summit/cfp <https://sel4.systems/Foundation/Summit/cfp> To propose a talk, send an abstract of one page or less by Monday 9th of May 2022 to summit(a)sel4.systems <mailto:summit@sel4.systems>. Please do spread the word and also encourage others to submit a talk if you like their work! Thanks, June

1 0

Overlapping pointer returned by memalign
by WILLIAMS Stephen 01 Apr '22

01 Apr '22

Hi, I’m currently working on a project porting drivers from U-Boot to seL4 and have run into an unexpected problem seemingly triggered by use of the memalign within the U-Boot drivers. What I am seeing is that calls to memalign from within my CAmkES component can return pointers to regions which overlap with those previously returned by malloc. Obviously this leads to the two allocated regions trampling over each other and resulting corruption of data. I’m at a complete loss to explain this behaviour and would be very grateful to receive any suggestions or pointers. Thanks for your help, Stephen This message contains information that may be privileged or confidential and is the property of the Capgemini Group. It is intended only for the person to whom it is addressed. If you are not the intended recipient, you are not authorized to read, print, retain, copy, disseminate, distribute, or use this message or any part thereof. If you receive this message in error, please notify the sender immediately and delete all copies of this message.

3 9

Re: How to switch virtual machines linux in vm_multi from camkes-vm-example?
by Peter Chubb 31 Mar '22

31 Mar '22

>>>>> "yjy" == yjy <yjy7894(a)126.com> writes: yjy> `screen /dev/ttyUSB0 115200`. I have a shell terminal that can yjy> see the output from VM0. I input @1 to shell, which is useless. It only works at the start of a line. Peter C yjy> At 2022-03-31 14:12:16, peter(a)chubb.wattle.id.au wrote: >>>>>>> "yjy" == yjy <yjy7894(a)126.com> writes: >> yjy> Hi, I have already run the camkes-vm-example vm_multi on my yjy> board, but i don't know how to switch linux vm shell from another yjy> linux vm, Can anyone help me solve this? >> >> If you're talking about controlling the serial console to talk to >> different VMs, the instructions are >> https://github.com/seL4/camkes-vm in the README.md under 'Serial' >> >> >> In brief, output from different VMs is colour coded. Switch >> between them for input with @0, @1, @2 etc. >> >> Peter C _______________________________________________ Devel >> mailing list -- devel(a)sel4.systems To unsubscribe send an email to >> devel-leave(a)sel4.systems yjy> [2 <text/html; GBK (base64)>] -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

1 0

How to switch virtual machines linux in vm_multi from camkes-vm-example?
by yjy 31 Mar '22

31 Mar '22

Hi, I have already run the camkes-vm-example vm_multi on my board, but i don't know how to switch linux vm shell from another linux vm, Can anyone help me solve this? Best, Comet

2 1

Question for student research
by Seth Nielson 31 Mar '22

31 Mar '22

Hi. I am mentoring a student group trying to do some work on SEL4. We are trying to setup basic TCP/IP networking and are really struggling to find documentation or up-to-date guides. We found a project that has networking (it even has some filesystem and a small webserver as part of the project). We thought we just about had the networking component working for QEMU but there seems to be issues with QEMU and networking, at least the way we did it. Does anyone have any how-to guides for getting basic networking up and running? If QEMU is not great for networking, please suggest a development board. Thanks much.

2 2

Information for Additional Virtio Driver Support of Sel4
by Tao Heng 陶恒-SW 28 Mar '22

28 Mar '22

Hi list， Is there any specific plan or some related development for supporting the Additional Virtio Driver (* e.g Virtio Blk, Virtio RNG, Virtio Balloon), as you mentioned in READ.md of libsel4vmmplatsupport, especially for the Virtio Blk? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

2 2

propagating initial thread's capabilities
by Sam Leffler 28 Mar '22

28 Mar '22

The rootserver gets various caps setup for it by the kernel (see Table 9.1 in the manual). This includes the gobal ASID, IRQ, Domain, and Sched controllers. I need these caps in a process created by the rootserver. This is within a CAmkES environment. So far I've created CAmkES component attributes that signal the rootserver should hand-off a cap by moving the rootserver's cap to the designated CNode just before it terminates. This involves modifications to CAmkES, capDL, and the rootserver. Is there a better way? Is there an existing example of doing this? Are any of these global objects accessible some other way than hand-off from the rootserver? -Sam

2 4

Questions about Kscurdomain variable.
by 603644559＠qq.com 25 Mar '22

25 Mar '22

In the case of multiple cores, is the scheduling of each core judged according to the kscurdomain, that is, the scheduling table of the domain is maintained by an operating system, rather than an independent kscurdomain in a core and a scheduling table of the domain in each core?

1 0

Hi,
by ezabujpz＠uuf.me 23 Mar '22

23 Mar '22

Hi, https://www.assortlist.com I would like to use network (TCP) on seL4, I know that I should probably be using lwip, however I have no idea how to properly initialize it (this is the first time I'm working in such a hardware close environment), so I need some help or some kind of example, but I don't know where to look. I'm working on ia32.

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 22 Mar '22

22 Mar '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: Tue, Mar 22, 9pm (UTC), Topics: (open) * Sydney: Wed, Mar 23, 8am * Central Europe: Tue, Mar 22, 10pm * US Pacific Time: Tue, Mar 22, 2pm (There are too many time zones in the world to cite them all :-)) 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

3 2

Report "Failed to touch ram region" error using virtio_console when assigned for Arm-VM more than 3G memory
by Han JingLong 韩景龙 21 Mar '22

21 Mar '22

Hi I had make virtio_console work well on my environment(armv8, RAM is 8G) based on vm_multi with Linux Guest OS(512M) and Android Guest OS(<= 3G) But I meet an error(vm_ram_touch@guest_ram.c:157 Failed to touch ram region: Not registered RAM region) when assign for a VM(Android Guest OS) more than 3G memory. 1. Some logs are added for debugging this issue： +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c @@ -86,6 +86,7 @@ static int emul_io_out(virtio_emul_t *emul, unsigned int offset, unsigned int si assert(size == 4); int queue = emul->virtq.queue; emul->virtq.queue_pfn[queue] = value; + printf("[hjl] queue_size:%d desc:%p\n", emul->virtq.queue_size[queue], (void *)(uintptr_t)(value << 12)); vring_init(&emul->virtq.vring[queue], emul->virtq.queue_size[queue], (void *)(uintptr_t)(value << 12), VIRTIO_PCI_VRING_ALIGN); break; +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul_helpers.c @@ -25,10 +25,43 @@ static int write_guest_mem(vm_t *vm, uintptr_t phys, void *vaddr, size_t size, s int vm_guest_write_mem(vm_t *vm, void *data, uintptr_t address, size_t size) { + bool is_inram = false; + vm_mem_t *guest_memory = &vm->mem; + for (int i = 0; i < guest_memory->num_ram_regions; i++) { + if (guest_memory->ram_regions[i].start <= address && + guest_memory->ram_regions[i].start + guest_memory->ram_regions[i].size >= address + size) { + /* We are within a ram region*/ + is_inram = true; + } + } + + if (!is_inram) { + printf("[hjl] write mem addr:%p size:0x%lx\n", address, size); + for (int index = 0; index < guest_memory->num_ram_regions; index++) { + printf("[hjl] write mem ram_regions start:%p size:0x%lx\n", guest_memory->ram_regions[index].start, guest_memory->ram_regions[index].size); + } + } + return vm_ram_touch(vm, address, size, write_guest_mem, data); } int vm_guest_read_mem(vm_t *vm, void *data, uintptr_t address, size_t size) { + bool is_inram = false; + vm_mem_t *guest_memory = &vm->mem; + for (int i = 0; i < guest_memory->num_ram_regions; i++) { + if (guest_memory->ram_regions[i].start <= address && + guest_memory->ram_regions[i].start + guest_memory->ram_regions[i].size >= address + size) { + /* We are within a ram region*/ + is_inram = true; + } + } + + if (!is_inram) { + printf("[hjl] read mem addr:%p size:0x%lx\n", address, size); + for (int index = 0; index < guest_memory->num_ram_regions; index++) { + printf("[hjl] read mem ram_regions start:%p size:0x%lx\n", guest_memory->ram_regions[index].start, guest_memory->ram_regions[index].size); + } + } return vm_ram_touch(vm, address, size, read_guest_mem, data); } 2. The detailed log is as follows: [hjl] queue_size:128 desc:0x8eb6000 [hjl] queue_size:128 desc:0x8eb8000 [hjl] read mem addr:0x8eb8802 size:0x2 [hjl] read mem ram_regions start:0x80000000 size:0x80000 [hjl] read mem ram_regions start:0x80080000 size:0x17cda00 [hjl] read mem ram_regions start:0x8184da00 size:0xa5b2600 [hjl] read mem ram_regions start:0x8be00000 size:0x83ae98 [hjl] read mem ram_regions start:0x8c63ae98 size:0x29c5168 [hjl] read mem ram_regions start:0x8f000000 size:0x26d35 [hjl] read mem ram_regions start:0x8f026d35 size:0xc0fd92cb vm_ram_touch@guest_ram.c:157 Failed to touch ram region: Not registered RAM region 3. devices.camkes configuration reference is as follows: #define VM1_RAM_BASE 0x80000000 #define VM1_RAM_SIZE 0xD0000000 #define VM1_DTB_ADDR 0x8F000000 //VM1_RAM_BASE + 0xF000000 #define VM1_INITRD_ADDR 0x8BE00000 //VM1_DTB_ADDR - VM1_INITRD_MAX_SIZE vm1.untyped_mmios = [ "0x80000000:28", // RAM "0x90000000:28", // RAM "0xa0000000:28", // RAM "0xb0000000:28", // RAM "0xc0000000:28", // RAM "0xd0000000:28", // RAM "0xe0000000:28", // RAM "0xf0000000:28", // RAM "0x100000000:28", // RAM "0x110000000:28", // RAM "0x120000000:28", // RAM "0x130000000:28", // RAM "0x140000000:28", // RAM /* "0x150000000:28", // RAM "0x160000000:28", // RAM "0x170000000:28", // RAM "0x180000000:28", // RAM "0x190000000:28", // RAM "0x1a0000000:28", // RAM "0x1b0000000:28", // RAM */ ]; 4. Present situation: At present, I tracked and found that When the Guest OS's virtio_console driver do the probe, it created the vring and iowrite to notify VMM of the virtqueue desc 's physical address in setup_vq() /* create the vring */ static void *vring_alloc_queue(struct virtio_device *vdev, size_t size, dma_addr_t *dma_handle, gfp_t flag) { ...... void *queue = alloc_pages_exact(PAGE_ALIGN(size), flag); if (queue) { phys_addr_t phys_addr = virt_to_phys(queue); *dma_handle = (dma_addr_t)phys_addr; /* activate the queue */ iowrite32(virtqueue_get_desc_addr(vq) >> VIRTIO_PCI_QUEUE_ADDR_SHIFT, vp_dev->ioaddr + VIRTIO_PCI_QUEUE_PFN); I'm very confused why is the physical memory allocated for virtqueue desc not within the effective memory range of VM when assign the memory to it exceeds 3G? BR. Allen 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

A question about capability derivation tree
by Chang Liu 18 Mar '22

18 Mar '22

Hi list, Here is a question about capability derivation trees, in particular when it comes to seL4_CNode_Copy and seL4_CNode_Mint. Suppose I have an untyped cap Untyped0, and I create a page cap by retyping Untyped0 into Frame0 (with seL4_AllRights). I then call CNode_Mint to mint Frame0 into Frame1 with restricted rights (say read-only). Finally, I call CNode_Copy to copy Frame1 into Frame2. What would the capability derivation tree look like at the end? Case 1: |--------| |Untyped0| |--------| / | \ / | \ / | \ |------| |------| |------| |Frame0| |Frame1| |Frame2| |------| |------| |------| Case 2: |--------| |Untyped0| |--------| | |------| |Frame0| |------| | |------| |Frame1| |------| | |------| |Frame2| |------| Case 3: |--------| |Untyped0| |--------| | |------| |Frame0| |------| / \ / \ |------| |------| |Frame1| |Frame2| |------| |------| Which one of the above is the correct answer? I suspect it's case 3, but I'm not sure. Best, Chang

1 0

Sel4 VMM Virtio Net Related Porting on Other SOC
by Tao Heng 陶恒-SW 11 Mar '22

11 Mar '22

Finally, I figured out the root cause of this issue. It happened when I changed the mac address of the virtio net probed for the vm guest. According to the issue, It seemed that the virtio_net driver of the libsel4vmmsupport did not support emulating the io control for changing the mac addess of the virtio net in the guest. 发件人: Tao Heng 陶恒-SW 发送时间: 2022年3月9日 14:49 收件人: 'devel(a)sel4.systems' <devel(a)sel4.systems> 主题: Sel4 VMM Virtio Net Related Porting on Other SOC Hi everyone , Background: I was porting vm_virtio_net project on other platforms with Cortex-A55. I met a run error with : ----------------------------------------- Unhandled offset of 0x14 of size 1, writing 0x2 Assertion failed: !"panic" (/home/kuang/workspace/penoy/system/core/seL4_projects_libs/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_out: 109) --------------------------------------------------- While it ran well on qemu with linux kernel version 4.9.189, my linux kernel version for the SOC is 4.14.61. If I replaced the qemu linux kernel with my kernel, the vm_virtio_net project also ran well on the qemu platform. To my analyzation, your virtio_net driver should be able to support for my platform. Is this related to my dts configuration for PCI node? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

2 1

Sel4 VMM Virtio Net Related Porting on Other SOC
by Tao Heng 陶恒-SW 09 Mar '22

09 Mar '22

Hi everyone , Background: I was porting vm_virtio_net project on other platforms with Cortex-A55. I met a run error with : ----------------------------------------- Unhandled offset of 0x14 of size 1, writing 0x2 Assertion failed: !"panic" (/home/kuang/workspace/penoy/system/core/seL4_projects_libs/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_out: 109) --------------------------------------------------- While it ran well on qemu with linux kernel version 4.9.189, my linux kernel version for the SOC is 4.14.61. If I replaced the qemu linux kernel with my kernel, the vm_virtio_net project also ran well on the qemu platform. To my analyzation, your virtio_net driver should be able to support for my platform. Is this related to my dts configuration for PCI node? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

Does the CSpace needs to have a cap to the TCB
by Sid Agrawal 09 Mar '22

09 Mar '22

Hi, We roughly do the following steps when setting up a new process in seL4: - Allocate a new TCB - Allocate new CSpace - Make the TCB point to the CSpace - Construct the VSpace and add the relevant caps in the new CSpace - Update the VSpace cap in the TCB. - Add a copy of the TCB cap in the new CSpace. (I am looking at the process spawn function in libesel4utils at: https://github.com/seL4/seL4_libs/blob/master/libsel4utils/src/process.c#L4…) My question is about the last point i.e. copying of TCB to the new CSpace. If I want to restrict the new domain from changing its VSpace, suspend itself, and change its fault handlers, I would simply not do the last step. Will that work? Is there any fundamental need for the TCB cap to be in the cspace it points to? Thanks, Sidhartha Agrawal

2 1

vm_multi usage
by Michael Neises 08 Mar '22

08 Mar '22

Hi, I'm just beginning to use multiple VMs at once, and I have a simple question. When I simulate my image, two VMs are running, and I get a terminal interface to one of them. Can I also switch my terminal to interface with the second VM? Cheers, Michael Neises

2 1

Re: I Have some questions about the domain mechanism in the seL4
by Isaac Beckett 08 Mar '22

08 Mar '22

> Date: Sat, 5 Mar 2022 19:15:05 +1100 > From: Kent Mcleod <kent.mcleod72(a)gmail.com> > Subject: [seL4] Re: I Have some questions about the domain mechanism > in the seL4 > To: 603644559(a)qq.com > Cc: devel <devel(a)sel4.systems> > Message-ID: > <CA+-ozWdgMgBin34WBUoVL+uHSNfU=e852ekPgrNGZ5J7+nyN0g(a)mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > >> On Sat, Mar 5, 2022 at 6:11 PM 603644559--- via Devel >> <devel(a)sel4.systems> wrote: >> >> For some reason, i m learning the scheduling module in seL4. I have read the manual and the source code, and i have already read the answer in the link https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/VYRTG3… >> But i still do not know the purpose of adding the domain mechanism in seL4, >> Can anyone explain what kind of requirement led to the design of the domain mechanism? >> Please explain it more specifically, and it would be best if there were relevant documents and papers on the domain mechanism. > > It was added in order to enable the completion of the info-flow proofs. > >> From the infoflow proof paper > (https://trustworthy.systems/publications/nicta_full_text/6464.pdf) > where it is called the partition scheduler: > "Similarly, the original seL4 scheduler, before partition > scheduling was implemented, was known not to enforce > isolation. We could not prove information flow security until > we had fully and correctly specified the partition scheduler > in the updated abstract specification. Proving information > flow security then required us to show that the scheduler’s > choice about which partition to schedule next can never be > affected by any other partition, as one would expect." Hello! It was my understanding that seL4 used to not have an in-kernel scheduler, and scheduling was up to the root task. How did that work? And why was the choice made to add the MCS features? Basically, why the change from having scheduling in the kernel vs. in userspace? It’s probably more convenient, especially since most operating systems are used to having scheduling in the kernel itself (so easier for people to think about). There are probably more technical reasons too. What are those?

2 3

I Have some questions about the domain mechanism in the seL4
by 603644559＠qq.com 07 Mar '22

07 Mar '22

For some reason, i m learning the scheduling module in seL4. I have read the manual and the source code, and i have already read the answer in the link https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/VYRTG3… But i still do not know the purpose of adding the domain mechanism in seL4, Can anyone explain what kind of requirement led to the design of the domain mechanism? Please explain it more specifically, and it would be best if there were relevant documents and papers on the domain mechanism.

2 2

Reminder: sel4 developer hangout
by Birgit Brecknell 07 Mar '22

07 Mar '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: Tue, Mar 22, 9pm (UTC), Topics: (open) * Sydney: Wed, Mar 23, 8am * Central Europe: Tue, Mar 22, 10pm * US Pacific Time: Tue, Mar 22, 1pm (There are too many time zones in the world to cite them all :)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au seL4 Foundation, birgit(a)sel4.systems 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Questions about shared page tables and Intel's MPK
by Sid Agrawal 06 Mar '22

06 Mar '22

Hi, I have a couple of questions about the virtual memory subsystem in seL4. 1. Intel's Memory Protection keys let a process restrict the access to given virtual address ranges based on a key. This key is the bit 62:59 of the virtual address. It is stored in the PTE of the level 4/5 Page Table. I want to use this feature in my project. Does seL4 support the setting of Memory Protection keys for virtual addresses? I couldn't find any mention of it in the source. I understand that if I use the current API of "seL4_X86_PageTable_Map" with those higher bits of the vaddr set, the kernel will ignore them. Is my understanding correct? Furthermore, was a decision made not to support MPK at some point? 2. As per section 7.3 of the seL4 manual, seL4 doesn't allow sharing of page tables. I am trying to understand the reasoning behind this. Was this done to aid verification? Thanks, Sidhartha S Agrawal

3 4

libsel4muslcsys: Error attempting syscall 215
by skydivebcn＠gmail.com 05 Mar '22

05 Mar '22

Hi guys, I was trying to boot a custom Linux 4.9.302 Kernel and fot this horrible message: "libsel4muslcsys: Error attempting syscall 215" hugo@dev:~/seL4/sel4webserver_hugusmaximus_fork/build$ sudo ./simulate --extra-qemu-args="-netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01,disable-modern=on,disable-legacy=off" [sudo] contraseña para hugo: ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=2048 -netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01,disable-modern=on,disable-legacy=off -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[61bf9000..631120af] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 61d3a2b8. Loaded DTB from 61d3a2b8. paddr=[60243000..60244fff] ELF-loading image 'kernel' to 60000000 paddr=[60000000..60242fff] vaddr=[ff8060000000..ff8060242fff] virt_entry=ff8060000000 ELF-loading image 'capdl-loader' to 60245000 paddr=[60245000..617fdfff] vaddr=[400000..19b8fff] virt_entry=408f38 Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/205 T0xff80bf815400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> Loading Linux: 'linux' dtb: 'linux-dtb' install_linux_devices@main.c:655 module name: map_frame_hack install_linux_devices@main.c:655 module name: init_ram install_linux_devices@main.c:655 module name: cross_vm_connections libsel4muslcsys: Error attempting syscall 215 libsel4muslcsys: Error attempting syscall 215 _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0x8020000 as this is purely an seL4 error message (musl libc seL4 code?) then I would appreciate any hint about what can be going on. P.S.: I have run my seL4 qemu aarch64 with several Linux kernel versions and never had this problem until now.

2 1

Sel4 VMM Virtio Net Related Porting on Other SOC
by Tao Heng 陶恒-SW 04 Mar '22

04 Mar '22

Hi everyone , Background: I was porting vm_virtio_net project on other platforms with Cortex-A55. I met a run error with : ----------------------------------------- Unhandled offset of 0x14 of size 1, writing 0x2 Assertion failed: !"panic" (/home/kuang/workspace/penoy/system/core/seL4_projects_libs/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_out: 109) --------------------------------------------------- While it ran well on qemu with linux kernel version 4.9.189, my linux kernel version for the SOC is 4.14.61. If I replaced the qemu linux kernel with my kernel, the vm_virtio_net project also ran well on the qemu platform. To my analyzation, your virtio_net driver should be able to support for my platform. Is this related to my dts configuration for PCI node? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0