- Devel - lists.sel4.systems

seL4 Native Web-browser
by Daniel Douglas Dyrseth 04 Mar '22

04 Mar '22

Hi, everyone What parts are needed besides seL4 to get a fully functioning Chromium browser running in a Wayland server? (No virtual OS inside seL4). I'm talking native seL4 OS capable of running Chromium with all features. Hoping for some insightful answers, and at least a list from a Pro - of the minimum parts needed for this. Regards, Daniel Douglas Dyrseth

2 1

Call for support contract to the seL4 Foundation
by Birgit Brecknell 25 Feb '22

25 Feb '22

A friendly reminder that bids are due before March 4th, 2022 AOE: The seL4 foundation is seeking to contract support for the following duties: - address open github issues in the seL4 organisation repositories, with prioritisation directed by the TSC delegates; this includes: - documentation, tutorials - bugs - tests - docsite and possibly website in coordination with Foundation people - help keeping an eye on making sure questions on mailing lists, discourse and github issues are answered (by someone) Requirement for the person working on these tasks are: - multiple years of experience with seL4, both at kernel level and user-level code - good familiarity with the seL4 organisation repositories - active contributor to one or more seL4 repositories - fluent in written and spoken English The seL4 foundation would contract a service company, initially for 6 months. The service company should identify the person that will be performing the work, ideally on a full-time basis. To bid for the contract, send email to foundation(a)sel4.systems before March 4th, 2022 AOE, with the resume of the person that will be performing the work and a cover letter addressing the requirements. --- 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

Re: Announcing Neptune OS release v0.1.1: A Windows NT personality for seL4
by Chang Liu 24 Feb '22

24 Feb '22

Thank you both for the discussion on licensing. Seems that GPLv3 is a good choice for now. Wikipedia seems to claim that ReactOS is licensed under "GPLv2 or any later version" but I didn't find this on the reactos source code itself. If the ReactOS foundation has an objection later I can always change it to v2. Best, Chang On Wed, Feb 23, 2022 at 12:09 AM G. Branden Robinson < g.branden.robinson(a)gmail.com> wrote: > Hi Chamg, > > At 2022-02-22T23:29:21-0500, Chang Liu wrote: > > I just added a LICENSE file which is GPLv3. > > Good choice! > > > I'm honestly not sure what the difference between GPLv2 and GPLv3 > > There are modest differences, but the general thrust of both versions of > the license is the same: guaranteed access to source code under a "share > and share alike" principle. > > > is so I went with the latest version (I assume they are compatible?) > > Technically, no. But most GPLv2 software is licensed under terms that > allow promotion of the license to "any later version". One famous > example of an exception that is GPLv2-only is the Linux kernel. > So is seL4 itself[1]. Consider whether you expect to need to share code > with a GPLv2-only project. (Even if you do, I would only revisit your > decision once concrete code-sharing is imminent.) > > You're not stuck with a choice of a single license forever. The GPLv3 > is a good selection to start with (in my opinion) because most > organizations that would like to exploit a work for proprietary > advantage are allergic to that license. > > You can always relicense a work under more permissive terms later if > doing so would align better with your goals. Going from more permissive > terms (like a BSD-style license) to a copyleft (like any version of the > GPL) can be impractical, or result in unintended consequences, because > it is arguably impossible to rescind the permissive license on the older > versions of the code--unless you have an Apple- or Oracle-sized budget > for lawyers to intimidate rivals maintaining the old code base. > > There is probably a better forum for licensing discussions, but my view > is that you've made a perfectly reasonable choice, one that situates > your project squarely and clearly within the Free Software community, > while still leaving you the option to reconsider later. > > Regards, > Branden > > [1] https://microkerneldude.org/2019/12/09/what-does-sel4s-license-imply/ >

1 0

Announcing Neptune OS release v0.1.1: A Windows NT personality for seL4
by Chang Liu 23 Feb '22

23 Feb '22

Hi list, For the past several months I have been working on a project which is to implement a Windows NT personality for the seL4 microkernel, which I have now taken to call “Neptune OS”, named after the codename for Windows 2000. The project has reached the point where I have implemented enough NT primitives such that a keyboard driver stack (taken from the ReactOS source code) can be loaded (as a user process), as well as a command prompt (shell), which is also taken from the ReactOS source code (albeit a very early version of ReactOS). These are all kernel-mode Windows device drivers that I’m running as user processes under seL4. The project is now on github: github.com/cl91/NeptuneOS. The entire system fits in a floppy (download link: github.com/cl91/NeptuneOS/releases/tag/v0.1.0001) Check it out! I think it’s cool! For the next release I’m planning to port the PCI stack, the AHCI stack, and a basic file system (probably fastfat.sys).

4 5

seL4 developer hangout/video call
by Birgit Brecknell 21 Feb '22

21 Feb '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: * Sydney: Wed, Feb 23, 8am * Central Europe: Tue, Feb 22, 10pm * US Pacific Time: Tue, Feb 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

Ability to change bench app options for RiscV
by Nataliya Korovkina 12 Feb '22

12 Feb '22

Hi, Does anyone remember why sel4bench configuration for RiscV was not allowed to change bench app options? If it was skipped because it was not necessary then I'd like to fix it. I would add a line to https://github.com/seL4/sel4bench/blob/master/apps/sel4bench/CMakeLists.txt --- a/apps/sel4bench/CMakeLists.txt +++ b/apps/sel4bench/CMakeLists.txt @@ -35,14 +35,15 @@ config_string( # Default dependencies on kernel benchmarking features. Declared here so that # all the benchmark applications can use it if( (KernelArchX86 AND KernelExportPMCUser AND KernelX86DangerousMSR) OR (KernelArchARM AND KernelArmExportPMUUser) OR (KernelArchArmCortexA8 AND KernelDangerousCodeInjection) + OR (KernelArchRiscV) ) set(DefaultBenchDeps TRUE) else() set(DefaultBenchDeps FALSE) endif() find_package(musllibc REQUIRED) Thanks, Nataliya

2 1

How to build compile seL4 along with another C++ project that includes <stdlib.h>
by christinefragoso＠protonmail.com 12 Feb '22

12 Feb '22

I want to run my C++ project in a camkes image for i.mx6. This image should be statically linked. I have a camkes app in https://github.com/seL4/camkes-manifest. The app's CMakeLists.txt includes my project with add_subdirectory("${CMAKE_CURRENT_LIST_DIR}/workspace_DDSHelloWorld"), which is a simple DDS example https://fast-dds.docs.eprosima.com/en/latest/fastdds/getting_started/simple… that also uses CMake as its build system. The entire app is built with ../init-build.sh -DPLATFORM=sabre -DCAMKES_APP=dds. However, the build fails. 1. My project includes <stdint.h>, but sel4 uses the -nostdinc and -nostdinc++ flags, so I get the error "stdint.h: No such file or directory". How do I make my C++ project include seL4's musllibc instead? 2. My project includes other C++ headers like <functional>. Is there any way to build seL4 with C++ headers?

2 1

testing rust program in sel4webserver example project
by lfern70＠gmail.com 12 Feb '22

12 Feb '22

Hi, I am trying to compile a simple rust web server to be executed in the virtual machine (as lighthttpd works in this webserver project). This server works perfect (I am using qemu for testing -aarch64), but when I try to get some random bytes using the rand crate the program hangs: .... let mut key = vec![0u8; 32]; rand::thread_rng().fill_bytes(&mut key); ... Do anybody knows if this could be related to some missing settings (in qemu command line or in some device.camkes file) or some rust features that don't work in a sel4 VM?? Thanks

2 1

Call for support contract to the seL4 Foundation
by June Andronick (seL4 Foundation) 11 Feb '22

11 Feb '22

The seL4 foundation is seeking to contract support for the following duties: - address open github issues in the seL4 organisation repositories, with prioritisation directed by the TSC delegates; this includes: - documentation, tutorials - bugs - tests - docsite and possibly website in coordination with Foundation people - help keeping an eye on making sure questions on mailing lists, discourse and github issues are answered (by someone) Requirement for the person working on these tasks are: - multiple years of experience with seL4, both at kernel level and user-level code - good familiarity with the seL4 organisation repositories - active contributor to one or more seL4 repositories - fluent in written and spoken English The seL4 foundation would contract a service company, initially for 6 months. The service company should identify the person that will be performing the work, ideally on a full-time basis. To bid for the contract, send email to foundation(a)sel4.systems before March 4th, 2022 AOE, with the resume of the person that will be performing the work and a cover letter addressing the requirements.

1 0

picoserver and qemu
by lfern70＠gmail.com 08 Feb '22

08 Feb '22

Hi, I am trying to test picoserver app in qemu, but I am not able to connect to the echo component on port 1234. These are the steps I am following, please, let me know if I am doing something wrong. Thanks in advance: $ repo init -u https://github.com/seL4/camkes-manifest.git $ repo sync # use docker container to compile $ container @in-container:/host$ mkdir build @in-container:/host$ cd build @in-container:/host$ ../init_build.sh -DCAMKES_APP=picoserver -DPICOSERVER_IP_ADDR=127.0.0.1 -DSIMULATION=1 @in-container:/host$ ninja Everything seems to be ok, but when I tried to execute in qemu: $ sudo ./simulate --machine q35,accel=kvm,kernel-irqchip=split --mem-size 2G --extra-cpu-opts "+vmx" --extra-qemu-args="--enable-kvm -device intel-iommu,intremap=on,caching-mode=on -netdev user,id=network0,hostfwd=tcp::1234-:1234 -device e1000e,netdev=network0" It seems the echo component is listening on port 1234, but if I try to send data with "netcat 127.0.0.1 1234" I can't reach the echo component ...... IOMMU 0x0: enabling... enabled Booting all finished, dropped to user space Protocol ethernet registered (layer: 2). Protocol ipv4 registered (layer: 3). Protocol ipv6 registered (layer: 3). Protocol icmp4 registered (layer: 4). Protocol icmp6 registered (layer: 4). Protocol igmp registered (layer: 4). Protocol udp registered (layer: 4). Protocol tcp registered (layer: 4). listener instance starting up, going to be listening on 192.168.0.21:4321 echo instance starting up, going to be listening on 192.168.0.21:1234

2 3

seL4 developer hangout/video call
by June Andronick (seL4 Foundation) 07 Feb '22

07 Feb '22

Friendly reminder that the seL4 developer hangout is on this week: - Sydney: Wed, Feb 9, 8am - Central Europe: Tue, Feb 8, 10pm - US Pacific Time: Tue, Feb 8, 1pm (There are too many time zones in the world to cite them all :)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, June

1 0

seL4 on TX1
by yjy 31 Jan '22

31 Jan '22

Help me! I am running sel4test on my TX1 according to the official tutorial, but I get a problem again and again. For the newly purchased TX1, I directly connected my Ubuntu host with UART serial port. At the same time, I follow this instruction ( https://docs.sel4.systems/Hardware/jetsontx1.html ), pulled the latest sel4test project code, successfully ran ninja command and built images "sel4test-driver-image-arm-tx1". Everything seemed to be going very smoothly. I use the newly purchased SanDisk 64GB SD card to boot my image, which has been formatted in ext4 format. Then I use command `sudo screen / dev / ttyusb0 115200` to open the UART serial port. After pressing and holding the power key for 1 second, and TX1 starts. Then I hit the Enter key to make TX1 cancel the auto boot default image and enter the u-boot interactive command line. Then, according to the instruction, under uboot, I typed the following command to load the image and start from the address 0x82000000: ``` ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 go 0x82000000 ``` Finally, I failed to start sel4test as I wanted. After many repetitions, I got the same error. This is my output： ------------------------------------------------------------------------------------------------------------------------------------------ Tegra210 (P2371-2180) # ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 5247256 bytes read in 260 ms (19.2 MiB/s) Tegra210 (P2371-2180) # go 0x82000000 ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p1 paddr=[80a57000..80f58117] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 80b825e0. Loaded DTB from 80b825e0. paddr=[8023d000..8024afff] ELF-loading image 'kernel' to 80000000 paddr=[80000000..8023cfff] vaddr=[ffffff8080000000..ffffff808023cfff] virt_entry=ffffff8080000000 ELF-loading image 'sel4test-driver' to 8024b000 paddr=[8024b000..80661fff] vaddr=[400000..816fff] virt_entry=40f0b8 Enabling MMU and paging Jumping to kernel-image entry point... Warning: gpt_cntfrq 19200000, expected 12000000 Bootstrapping kernel available phys memory regions: 2 [80000000..ff000000] [100000000..180000000] reserved virt address space regions: 3 [ffffff8080000000..ffffff808023d000] [ffffff808023d000..ffffff808024b000] [ffffff808024b000..ffffff8080662000] seL4 failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap' at /home/yjy/Desktop/sel4-rpi/sel4test_newv2/kernel/src/object/cnode.c:426 in function cteInsert halting... Kernel entry via Interrupt, irq 0 ------------------------------------------------------------------------------------------------------------------------------------------ I'm about to collapse. I really need your help. How can I solve this problem? 1. Why did I get this warning？ "Warning: gpt_cntfrq 19200000, expected 12000000" , It exists in this file "/sel4test/kernel/src/drivers/timer/generic_timer.c:21" 2. About reporting errors "failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap'". I found that the variable "(slot_ptr_t) (rootserver.tcb) ) -> cap.words[0] " is equals to 0xffffffffffffffff, so that the cap_get_capType(destSlot->cap) <=> (slot_ptr_t) (rootserver.tcb) ) -> cap.words[0] & 0x1full != 0 . I guess it caused the mistake, but i don't know why. I'm about to collapse. I really need your help. How can I solve this problem? I'm sorry for sending this email again!

2 3

Re: seL4 on TX1
by 杨竣轶 30 Jan '22

30 Jan '22

I did’t get any difference about my error except the address. Is my Uboot precedure errored? 从 Windows 版邮件发送

1 0

seL4test on Nvidia TX1
by yjy7894＠126.com 28 Jan '22

28 Jan '22

Help me! I am running sel4test on my TX1 according to the official tutorial, but I get a problem again and again. For the newly purchased TX1, I directly connected my Ubuntu host with UART serial port. At the same time, I follow this instruction ( https://docs.sel4.systems/Hardware/jetsontx1.html ), pulled the latest sel4test project code, successfully ran ninja command and built images "sel4test-driver-image-arm-tx1". Everything seemed to be going very smoothly. I use the newly purchased SanDisk 64GB SD card to boot my image, which has been formatted in ext4 format. Then I use command `sudo screen / dev / ttyusb0 115200` to open the UART serial port. After pressing and holding the power key for 1 second, and TX1 starts. Then I hit the Enter key to make TX1 cancel the auto boot default image and enter the u-boot interactive command line. Then, according to the instruction, under uboot, I typed the following command to load the image and start from the address 0x82000000: ``` ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 go 0x82000000 ``` Finally, I failed to start sel4test as I wanted. After many repetitions, I got the same error. This is my output： ------------------------------------------------------------------------------------------------------------------------------------------ Tegra210 (P2371-2180) # ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 5247256 bytes read in 260 ms (19.2 MiB/s) Tegra210 (P2371-2180) # go 0x82000000 ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p1 paddr=[80a57000..80f58117] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 80b825e0. Loaded DTB from 80b825e0. paddr=[8023d000..8024afff] ELF-loading image 'kernel' to 80000000 paddr=[80000000..8023cfff] vaddr=[ffffff8080000000..ffffff808023cfff] virt_entry=ffffff8080000000 ELF-loading image 'sel4test-driver' to 8024b000 paddr=[8024b000..80661fff] vaddr=[400000..816fff] virt_entry=40f0b8 Enabling MMU and paging Jumping to kernel-image entry point... Warning: gpt_cntfrq 19200000, expected 12000000 Bootstrapping kernel available phys memory regions: 2 [80000000..ff000000] [100000000..180000000] reserved virt address space regions: 3 [ffffff8080000000..ffffff808023d000] [ffffff808023d000..ffffff808024b000] [ffffff808024b000..ffffff8080662000] seL4 failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap' at /home/yjy/Desktop/sel4-rpi/sel4test_newv2/kernel/src/object/cnode.c:426 in function cteInsert halting... Kernel entry via Interrupt, irq 0 ------------------------------------------------------------------------------------------------------------------------------------------ Help me! I am running sel4test on my TX1 according to the official tutorial, but I get a problem again and again. For the newly purchased TX1, I directly connected my Ubuntu host with UART serial port. At the same time, I follow this instruction ( https://docs.sel4.systems/Hardware/jetsontx1.html ), pulled the latest sel4test project code, successfully ran ninja command and built images "sel4test-driver-image-arm-tx1". Everything seemed to be going very smoothly. I use the newly purchased SanDisk 64GB SD card to boot my image, which has been formatted in ext4 format. Then I use command `sudo screen / dev / ttyusb0 115200` to open the UART serial port. After pressing and holding the power key for 1 second, and TX1 starts. Then I hit the Enter key to make TX1 cancel the auto boot default image and enter the u-boot interactive command line. Then, according to the instruction, under uboot, I typed the following command to load the image and start from the address 0x82000000: ``` ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 go 0x82000000 ``` Finally, I failed to start sel4test as I wanted. After many repetitions, I got the same error. This is my output： ------------------------------------------------------------------------------------------------------------------------------------------ Tegra210 (P2371-2180) # ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 5247256 bytes read in 260 ms (19.2 MiB/s) Tegra210 (P2371-2180) # go 0x82000000 ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p1 paddr=[80a57000..80f58117] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 80b825e0. Loaded DTB from 80b825e0. paddr=[8023d000..8024afff] ELF-loading image 'kernel' to 80000000 paddr=[80000000..8023cfff] vaddr=[ffffff8080000000..ffffff808023cfff] virt_entry=ffffff8080000000 ELF-loading image 'sel4test-driver' to 8024b000 paddr=[8024b000..80661fff] vaddr=[400000..816fff] virt_entry=40f0b8 Enabling MMU and paging Jumping to kernel-image entry point... Warning: gpt_cntfrq 19200000, expected 12000000 Bootstrapping kernel available phys memory regions: 2 [80000000..ff000000] [100000000..180000000] reserved virt address space regions: 3 [ffffff8080000000..ffffff808023d000] [ffffff808023d000..ffffff808024b000] [ffffff808024b000..ffffff8080662000] seL4 failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap' at /home/yjy/Desktop/sel4-rpi/sel4test_newv2/kernel/src/object/cnode.c:426 in function cteInsert halting... Kernel entry via Interrupt, irq 0 ------------------------------------------------------------------------------------------------------------------------------------------ I'm about to collapse. I really need your help. How can I solve this problem? 1. Why did I get this warning？ "Warning: gpt_cntfrq 19200000, expected 12000000" , It exists in this file "/sel4test/kernel/src/drivers/timer/generic_timer.c:21" 2. About reporting errors "failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap'". I found that the variable "(slot_ptr_t) (rootserver.tcb) ) -> cap.words[0] " is equals to 0xffffffffffffffff, so that the cap_get_capType(destSlot->cap) <=> (slot_ptr_t) (rootserver.tcb) ) -> cap.words[0] & 0x1full != 0 . I guess it caused the mistake, but i don't know why. I'm about to collapse. I really need your help. How can I solve this problem?

1 0

Re: seL4 developer hangout/video call
by Isaac Beckett 27 Jan '22

27 Jan '22

Hello all! If you’re reading this at the time it was sent, then the developer hangout is in roughly an hour. See you there! > > On Jan 25, 2022, at 8:02 PM, devel-request(a)sel4.systems wrote: > > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via email, send a message with subject or > body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > Today's Topics: > > 1. Re: seL4 developer hangout/video call (Gerwin Klein) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Tue, 25 Jan 2022 06:52:21 +0000 > From: Gerwin Klein <kleing(a)unsw.edu.au> > Subject: [seL4] Re: seL4 developer hangout/video call > To: devel <devel(a)sel4.systems> > Message-ID: <7F36F76C-E596-4A51-9419-785AB723CC03(a)unsw.edu.au> > Content-Type: text/plain; charset="us-ascii" > > Just a reminder that seL4 dev hangout is not tomorrow, but shifted by one day. > > Cheers, > Gerwin > >> On 23 Jan 2022, at 18:13, Gerwin Klein <kleing(a)unsw.edu.au> wrote: >> >> An earlier-than-usual heads-up that the seL4 developer hangout this week will be shifted by one day, because of the public holiday in Australia. >> >> This means, we're meeting on Wed for Europe/US and on Thu for Australia: >> >> - Sydney: Thu, Jan 27, 8am >> - Central Europe: Wed, Jan 26, 10pm >> - US West Coast: Wed, Jan 26, 1pm >> >> Zoom link: https://unsw.zoom.us/j/82640784431 >> >> Cheers, >> Gerwin >> > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems > > > ------------------------------ > > End of Devel Digest, Vol 135, Issue 2 > *************************************

3 2

📣 2022 SUMMIT - Trusted Computing Center of Excellence
by Griffiss Institute 27 Jan '22

27 Jan '22

NEXT WEEK! Register TODAY! NEXT WEEK! | SUMMIT 2022 View email in browser https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498… https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498… REGISTER NOW! (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) NEXT WEEK! 2022 SUMMIT BEGINS JAN 31! The Trusted Computing Center of Excellence (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) (TCCoE) is excited to announce that our annual Summit (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) will be held virtually on January 31 - February 3, 2022! The TCCoE has been established with support from DARPA (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) , AFRL (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) , and the Griffiss Institute (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) . Many of you may be familiar with the annual seL4® Summit, which we’ve successfully hosted for the past three years in coordination with the seL4 Foundation. Planning for the next annual seL4 Summit has begun under the leadership of seL4 Foundation, tentatively scheduled for October 2022 at a site in Europe. Beginning in January 2022, the TCCoE will host an annual Summit in the US, a complementary multi-day event focused on trusted computing technologies with a current emphasis on the secure embedded L4 (seL4) microkernel. seL4 is the world’s first open source operating system kernel with an end-to-end proof of implementation correctness and security enforcement. The main theme of this year’s TCCoE Summit is to provide a forum to discuss measurable security, resilience and assurance, via organic integration of hardware and software security features, for current and future platforms and systems. Specifically, the Summit scope includes, (but is not limited to), discussions on hardware security features, kernel, hypervisor and Virtual Machine Managers (VMMs), operating systems, containers, software security, etc. The TCCoE Summit will provide attendees the opportunity to attend presentations by government, industry, and academia experts; interact with discussion panels; and obtain tutorial training related to the seL4 microkernel. Come join us for 4 days packed with thought provoking keynotes, insightful presentations, lively panel discussions, and educational tutorials - an event that anyone interested in embedded systems and trust-based computing cannot miss! We look forward to your attendance! REGISTRATION IS LIVE! Registration | 13 January 2022 - 3 Feb 2022 | $250 (US) REGISTER NOW! (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) REMINDER #1: Some levels of TCCoE Membership include discounted and free attendance at the Summit, so check with your organization about membership status! REMINDER #2: Tutorials will take place on Monday, January 31, starting at 8:00 am EST. These tutorials are included with your 2022 TCCoE Summit registration. You can join these one day tutorials for free just by registering below. TUTORIAL REGISTRATION (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) MEMBERSHIP Have you and/or your company considered Trusted Computing Center of Excellence membership? Through membership, you gain an opportunity to influence the CoE’s priorities and technical direction, share ideas and network among peers in our community, and gain leverage from the latest trusted computing (e.g. seL4®) based innovations. The specific member benefits vary by membership class, but in general, membership benefits include: * Complimentary (or discounted) registration fee for CoE workshops and events * Advertising on the CoE’s website, in CoE publications, and at CoE sponsored events * Voting privileges for the election of the CoE Board of Directors, and other matters * Representation on CoE Committees * Tutorials for developers of trusted systems * Connect and collaborate securely and privately with other CoE members (chat, etc.) * Curated Software Distributions * Access to the CoE Private Code Repository (ITAR restrictions may apply) JOIN NOW! (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498… seL4 is a trademark of LF Projects, LLC. ============================================================ Copyright © 2022 Griffiss Institute, All rights reserved. You are receiving this email because of your interest in the Trusted Computing Center of Excellence.. Our mailing address is: Griffiss Institute 592 Hangar Rd Rome, NY 13441-4506 USA Want to change how you receive these emails? You can ** update your preferences (https://griffissinstitute.us6.list-manage.com/profile?u=f0470275265f4981c83…) or ** unsubscribe from this list (https://griffissinstitute.us6.list-manage.com/unsubscribe?u=f0470275265f498…)

1 0

seL4 developer hangout/video call
by Gerwin Klein 25 Jan '22

25 Jan '22

Hi seL4 devs, a few of us thought it might be nice to talk more directly from time to time rather than only via pull requests, so we're trialling a seL4 developer hangout/video chat. The idea for this is to be: - informal, about 1h - for technical discussions about seL4 and related repositories - anyone can join - every two weeks, initially for 3 times, then we can decide how we like it At least one or two technical steering committee (TSC) members will try to be at every one of these, but these are not TSC meetings where formal decisions are made, just technical discussions about whatever people have on their minds. To provide a starting topic, one thing we'd be interested in is: seL4 boot code There have been quite a few pull requests in that area, and it'd be nice to know what people's plans are and how we can keep this part of seL4 high assurance while making it more flexible. Other topics for future meetings could be better support for other language bindings (e.g. Rust), any RFCs that are open or people are thinking about opening, or just discussions about current pull requests or issues. The first hangout is on - Sydney: Wed, Nov 3, 8am - Central Europe: Tue, Nov 2, 10pm - US East Coast: Tue, Nov 2, 2pm Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

2 9

Re: seL4 developer hangout/video call
by Isaac Beckett 25 Jan '22

25 Jan '22

Other US time zones: PST (West Coast): 1pm MST (Mountain Time): 2pm CST (Central Time): 3pm EST (East Coast): 4pm We have a lot of time zones here, it’s a bit of a pain sometimes. > > On Jan 23, 2022, at 8:01 PM, devel-request(a)sel4.systems wrote: > > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via email, send a message with subject or > body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > Today's Topics: > > 1. Re: seL4 developer hangout/video call (Gerwin Klein) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sun, 23 Jan 2022 07:13:27 +0000 > From: Gerwin Klein <kleing(a)unsw.edu.au> > Subject: [seL4] Re: seL4 developer hangout/video call > To: devel <devel(a)sel4.systems> > Message-ID: <678C2D4C-EEE5-4D79-82BD-256BC78B3BFC(a)unsw.edu.au> > Content-Type: text/plain; charset="us-ascii" > > An earlier-than-usual heads-up that the seL4 developer hangout this week will be shifted by one day, because of the public holiday in Australia. > > This means, we're meeting on Wed for Europe/US and on Thu for Australia: > > - Sydney: Thu, Jan 27, 8am > - Central Europe: Wed, Jan 26, 10pm > - US West Coast: Wed, Jan 26, 1pm > > Zoom link: https://unsw.zoom.us/j/82640784431 > > Cheers, > Gerwin > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems > > > ------------------------------ > > End of Devel Digest, Vol 134, Issue 1 > *************************************

2 1

Sel4 Vmm Project Supporting on memory resources configure
by Tao Heng 陶恒-SW 19 Jan '22

19 Jan '22

Hi Sel4: While portinging Android Guest based on Sel4 Vmm project, I met some problems .In my porting steps, I increased the reserved memory for Android Guest to 2G on my platform. Then there were some parts of Sel4 Vmm project that confused me. 1. the principle to determin the static pool size for bootstrap with allocman n In bootstrap.h, I found your explanation for the value that it is based on the work with trial and error.Is that still the case? n If I incease this size, the frame_vm0_group_bin showed in vm_minimal.cdl file will obviously increase together.What’s the relationship of the two value? 2. How is the staic memory pool created? Is this memory pool created from untyped memory, so as treated untyped object? 3. the principle to determin the vm.simple_untyped24_pool size and nums n What’s the usage of the untyped_pool memory? n How can I make sure a reasonable size and nums of this value ? Much apprecitated, if you can give some feedbacks. Tao Heng | Taoer * +8618800230581 * taoheng(a)saicmotor.com<mailto:taoheng@saicmotor.com> Basic Software Platform SAIC Motor Z-ONE Software Company Auto Innovation Park | 201 Anyan Road, Jiading, Shanghai 邮件免责申明 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

Virtual Machine and scheduling query
by Sidhartha 12 Jan '22

12 Jan '22

Hi, I am a 2nd-year grad student at the Systopia Lab in UBC. I am using seL4 for the OS research project at I have a few independent questions: 1. Virtual Machines can be implemented with different levels of support from the hardware. If we talk about x86_64, in the most basic terms, you could have VMs without or without VT-X extensions. Looking at the resources available on the seL4 site, I think the given VMM libraries assume VT-X. Is there an example that does not use VT-X? 2. The scheduler inside seL4 is relatively simple. I have heard(Thanks Nick!) that if a complicated scheduling policy is desired, it can be done in userspace. A user-level component that has the capabilities to all the TCB's can play with the priority, resume/pause, and achieve any arbitrary scheduling. Is there an example available which I could look at? 3. I would like to implement a new functionality of memory quota, where different user-apps can be assigned memory quota and not just the physical pages. Does such a functionality belong in the kernel or the userspace component(say memory quota manager)? In the latter case, it would be just an endPoint capability to the quota manager service, so how does one split it - say split a quota of 100MB into two separate 50MB quotas. This is more a generic micro-kernel query rather than seL4 specific, but any insights would help. Thanks, Sid sid-agrawal.ca

1 0

sel4test AARCH64 on imx8mm-evk
by Zippy Manaic 07 Jan '22

07 Jan '22

Hi, I have tried running sel4test built for AARCH64 (https://docs.sel4.systems/Hardware/imx8mm.html) on my imx8mm-evk dev board. I am on the 12.1.0 branch of sel4test-manifest.git. Firstly I have to add "set(KernelAArch64SErrorIgnore ON)" to my build config in order to get the tests running and unfortunately things go awry during the test run ... Starting test 47: FRAMEEXPORTS0001 Running test FRAMEEXPORTS0001 (Test that we can access all exported frames) Pagefault from [FRAMEEXPORTS0001]: read fault at PC: 0x41c4ec vaddr: 0x11000000, FSR 0x92000210 Register of root thread in test (may not be the thread that faulted) Register dump: pc: 0x41c4ec sp: 0x100118a0 spsr: 0x80000040 x0: 0x11000000 x1: 0x11000000 x2: 0x55 x3: 0x15 x4: 0xe6 x5: 0x0 x6: 0x0 x7: 0xffffffffffffffff x8: 0x10011a48 x16: 0x0 x17: 0x0 x18: 0x0 x29: 0x100118a0 x30: 0x41c9f0 x9: 0x2b x10: 0x2b x11: 0xffffffff x12: 0x0 x13: 0x0 x14: 0x0 x15: 0x0 x19: 0xe7 x20: 0x8 x21: 0x11000000 x22: 0x0 x23: 0x0 x24: 0x0 x25: 0x0 x26: 0x0 x27: 0x0 x28: 0x0 tpidr_el0: 0x616f60 tpidrro_el0: 0x0 Failure: result == SUCCESS at line 291 of file /host/projects/sel4test/apps/sel4test-driver/src/testtypes.c Error: result == SUCCESS at line 217 of file /host/projects/sel4test/apps/sel4test-driver/src/main.c ... Starting test 55: IPC1001 Running test IPC1001 (Test SMP inter-AS seL4_Send + seL4_Recv) KERNEL DATA ABORT! Faulting instruction: 0xffffff804001e2ac FAR: 0xffffff80bf800020 ESR (DFSR): 0x96000210 halting... Kernel entry via Syscall, number: 1, Call Cap type: 10, Invocation tag: 20 Is this something that should just work? Or am I missing something. Cheers, Zippy

3 9

答复: Devel Digest, Vol 130, Issue 2
by yadong.li 03 Jan '22

03 Jan '22

Hi Matthew: Firstly, thank you for your information. form your answer, we understand the design intention of group, we Iook at compilation proces and may be find the probelm of compiler, we the assume the following scenario: The client A and client B are in the same group, they all have the same global variable like "global_buf", when use objcopy with "--keep-global-symbol" param, it will change the "global_buf" symbol form "gloabl" to "local", this change make the same name global variable of different client in same space can work well, they can access their own global variable as local variable. But In out test, we find if the "global_buf" not be initialized, in the group, there is only one "global_buf", if client A change the value of "global_buf", client B also can see the change, this is may be wrong, we find the gcc objcopy with "--keep-global-symbol" can only affect ".data" and ".bss" section, but "global_buf" which not be initialized, will place in ".common" section, "--keep-global-symbol" will not change the symbol of ".common" form global to local, this may be solved by add "-fno-common" when linker in camkes project related to "group" scenario ________________________________ 发件人: devel-request(a)sel4.systems <devel-request(a)sel4.systems> 发送时间: 2021年12月28日 9:00:05 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 130, Issue 2 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: Some questions about group of camkes (adjust the format) (Matthew Fernandez) ---------------------------------------------------------------------- Message: 1 Date: Mon, 27 Dec 2021 16:26:26 -0800 From: Matthew Fernandez <matthew.fernandez(a)gmail.com> Subject: [seL4] Re: Some questions about group of camkes (adjust the format) To: "yadong.li" <yadong.li(a)horizon.ai> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems>, "xiaonan.wang" <xiaonan.wang(a)horizon.ai>, "lei.mao" <lei.mao(a)horizon.ai> Message-ID: <DA97FC78-B670-4CF7-88AC-9810B31D1015(a)gmail.com> Content-Type: text/plain; charset=utf-8 > On Dec 23, 2021, at 08:50, yadong.li <yadong.li(a)horizon.ai> wrote: > > Hi > > * We learn the group of camkes from the https://github.com/seL4/camkes-tool/blob/master/docs/index.md > * group can colocate two component instances in a single address space, we want to use the share var by this way, like directcall transfer string virtual address, But we feel confused about the global symbols who have the same symbol name include function and variable in a single address space, Their behavior seems undefined 。 My information on how this works is out of date and I can’t answer all your questions, but I can tell you how this feature was originally implemented. Single address space components were originally implemented using post-compilation symbol mangling. As you’ve noticed, naive linking of two component instances together presents two problems: 1. Unrelated homonyms between the instances now conflict. A symbol called `foo` in component instance A and a symbol called `foo` in component instance B now refer to the same thing when linked together. 2. References to glue code have the opposite problem: their names may differ in component instance A and component instance B, but need to refer to the same functions when the two are linked together. Both problems were solved with the same mechanism: GNU objcopy. The invocations to objcopy were template-generated so they could take advantage of knowledge about the system begin compiled. A generated objcopy invocation would do the following: 1. Adjust all non-generated symbols to have internal visibility. Component instance A and component instance B have already been (partially) linked, so at this point the only unresolved symbols that need to remain externally visible are those related to the connection(s) between them. This solves problem 1 above. 2. Name-mangle all remaining symbols to something prefixed with the relevant connection instance’s name. IIRC the name mangling scheme was something like ‘<connection instance name><space><original symbol name>’. This guaranteed uniqueness because <space> is not a character that existed in C or assembly symbols. Whether using a space in a symbol name is legal or not, I don’t know, but all the binutils seemed fine with this. 3. Rename the second component in the name mangling above to a common name. I don’t recall exactly how this name was chosen, but this solves problem 2 above. This sounds pretty unorthodox and brittle, but it actually worked surprisingly well. All combinations of single address space component systems seemed to Just Work, with a few notable sharp edges: * Anything involving MMIO was tricky. These symbols frequently needed to remain externally visible and the two component instances would often have differing names but the same addresses for them. * GNU ld was more or less required. The multiple steps involving partial linking was only supported by GNU ld and Gold at the time. LLVM’s lld may have caught up in the interim years. * The objcopy name mangling broke cross-section references used by GCC’s implementation of Link-Time Optimization. As a result, any LTO compilation degraded to LTO being disabled. This wouldn’t have been a big deal except that one of the primary reasons to put two components in a single address space is to enable cross-component inlining, usually facilitated by LTO. AFAICT this (playing objcopy tricks and expecting LTO to still work) was simply not a supported use case. We explored how to work around this and got some one-off efforts working for benchmarking, but proper support would have involved altering the way binutils work. ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems ------------------------------ End of Devel Digest, Vol 130, Issue 2 *************************************

2 1

Question about the Real-time of the SEL4.
by 刘跃 Jeff Liu 01 Jan '22

01 Jan '22

Hi; As we know, seL4 is a non preemptive kernel. Is it because the kernel of seL4 is an event based model? Then why not use the thread based kernel? As far as I know, VxWorks and QNX are thread based. SeL4's view is that for non preemptive kernel, real-time performance focuses on WCET, and the faster kernel does not guarantee the real-time performance of the system. I partially agree with this view. I want to know if there are real-time comparison data?, The comparison test with VxWorks or QNX is about the real-time performance of the system. the worst case interrupt latency is the sum of both the longest region with interrupts disabled, and the time to dispatch an interrupt to a user thread. How are these two parts of time calculated? Is it the method of WCET static analysis? And Then how to improve the interrupt response time, What is the specific method to reduce interrupt latency? I think most users of seL4 are more concerned about this. I look forward to communicating and discussing with you, experts. Thanks;

2 1

Some questions about group of camkes (adjust the format)
by yadong.li 28 Dec '21

28 Dec '21

Hi * We learn the group of camkes from the https://github.com/seL4/camkes-tool/blob/master/docs/index.md * group can colocate two component instances in a single address space, we want to use the share var by this way, like directcall transfer string virtual address, But we feel confused about the global symbols who have the same symbol name include function and variable in a single address space, Their behavior seems undefined 。 * Our camkes project test below, clien1 and client2 in the same group: " import <std_connector.camkes>; procedure MyInterface { void print(in string message); } component Client { control; uses MyInterface iface; } component Server { provides MyInterface iface; } assembly { composition { group g { component Client client_1; component Client client_2; } component Server server; connection seL4RPCCall conn(from g.client_1.iface, from g.client_2.iface, to server.iface); } configuration { client_1.iface_attributes = 11; client_2.iface_attributes = 22; } } * 1. We test function in group (a single address space): * the client code below: " #include <camkes.h> int run(void) { char *name = get_instance_name(); iface_print(name); return 0; } " * the server code below: " #include <camkes.h> #include <stdio.h> void iface_print(const char *name) { printf("[%s] ping, the badge is [%d]\n", name, iface_get_sender_id()); } " * From the cameks project, we have two client, they are client_1 and client_2, they have the same they can all “iface_print” to access server function，In this scene，we have two quesiton: * Question 1. After compiled the test project, we found in the symbol table of g_group_bin, we have two "iface_print" symbol, they have different address even though they have the same name, it look like the componet can call their own "iface_print", I think in a single address space, component like thread, Why two symbols with the same name(iface_print) will not conflict in one address space * Question 2: when client access server, we offer the _attributes(badge) for the interface of client, by test, the two client can call their own "iface_print", but the server can only recevice one badge 22, below is our test: " [client_2] ping, the badge is [22] [client_1] ping, the badge is [22] " * The attribute(badge) of client1 is covered by the attribute(badge) of client2, The iface_print of two client have only one capability to access IPC endpoint object * We can not understand in single address space,the "iface_print" of two component is behavior as one or two different ? * 2. We test function in global variable (a single address space): * We found whether global variables are initialized will have completely different behavior， out test code below: * scene1 :Client code below: " int temp_value; int run(void) { char *name = get_instance_name(); iface_print(name); printf("at start, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); if (strcmp(name, "client_1") == 0) { int count = 1000000000; while(count--) { asm volatile(""); } /* client1 read the temp_value*/ printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } else { /* client2 change the val of temp_value */ temp_value = 0x12345; printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } return 0; } " * Phenomenon: client1 and client2 are different instances of the same code in same group，form the above code，the symbol of "temp_value" is bss section, the temp_value of client1 and the temp_value of client2 have the same virtual address, and if the client2 change the value, client1 can perceive the change， test as below： " at start, in client_1, the temp_value address is [0x659e70], value is [0x0] at start, in client_2, the temp_value address is [0x659e70], value is [0x0] at last, in client_2, the temp_value address is [0x659e70], value is [0x12345] at last, in client_1, the temp_value address is [0x659e70], value is [0x12345] " * scene2 :Client code below: " int temp_value = 1; int run(void) { char *name = get_instance_name(); iface_print(name); printf("at start, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); if (strcmp(name, "client_1") == 0) { int count = 1000000000; while(count--) { asm volatile(""); } /* client1 read the temp_value*/ printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } else { /* client2 change the val of temp_value */ temp_value = 0x12345; printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } return 0; } " * Phenomenon: client1 and client2 are different instances of the same code in same group，form the above code，the symbol of "temp_value" is data section, the temp_value of client1 and the temp_value of client2 have the different virtual address, and if the client2 change the value, client1 can not get the change， test as below： " at last, in client_2, the temp_value address is [0x445ba8], value is [0x12345] at last, in client_1, the temp_value address is [0x444008], value is [0x1] " * The code of scene1 and scene2 are almost the same, except whether temp_value is initialized， the bss section or data section，but the symbol table completely different, scene1 the symbol table of g_group_bin has only one "temp_value" symbol, But scene1 the symbol table of g_group_bin has two symbols named temp_value, we also do not understand why the same name symbols of global variable should be one or two in a single address of group. It looks like random. Thank you very much

2 1

Some questions about group of camkes
by yadong.li 24 Dec '21

24 Dec '21

Hi * We learn the group of camkes from the https://github.com/seL4/camkes-tool/blob/master/docs/index.md * group can colocate two component instances in a single address space, we want to use the share var by this way, like directcall transfer string virtual address, But we feel confused about the global symbols who have the same symbol name include function and variable in a single address space, Their behavior seems undefined 。 * Our camkes project test below, clien1 and client2 in the same group: import <std_connector.camkes>; procedure MyInterface { void print(in string message); } component Client { control; uses MyInterface iface; } component Server { provides MyInterface iface; } assembly { composition { group g { component Client client_1; component Client client_2; } component Server server; connection seL4RPCCall conn(from g.client_1.iface, from g.client_2.iface, to server.iface); } configuration { client_1.iface_attributes = 11; client_2.iface_attributes = 22; } } * 1. We test function in group (a single address space): * the client code below: #include <camkes.h> int run(void) { char *name = get_instance_name(); iface_print(name); return 0; } * the server code below: #include <camkes.h> #include <stdio.h> void iface_print(const char *name) { printf("[%s] ping, the badge is [%d]\n", name, iface_get_sender_id()); } * From the cameks project, we have two client, they are client_1 and client_2, they have the same they can all “iface_print” to access server function，In this scene，we have two quesiton: * Question 1. After compiled the test project, we found in the symbol table of g_group_bin, we have two "iface_print" symbol, they have different address even though they have the same name, it look like the componet can call their own "iface_print", I think in a single address space, component like thread, Why two symbols with the same name(iface_print) will not conflict in one address space * Question 2: when client access server, we offer the _attributes(badge) for the interface of client, by test, the two client can call their own "iface_print", but the server can only recevice one badge 22, below is our test: [client_2] ping, the badge is [22] [client_1] ping, the badge is [22] * The attribute(badge) of client1 is covered by the attribute(badge) of client2, The iface_print of two client have only one capability to access IPC endpoint object * We can not understand in single address space,the "iface_print" of two component is behavior as one or two different ? * 2. We test function in global variable (a single address space): * We found whether global variables are initialized will have completely different behavior， out test code below: * scene1 :Client code below: int temp_value; int run(void) { char *name = get_instance_name(); iface_print(name); printf("at start, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); if (strcmp(name, "client_1") == 0) { int count = 1000000000; while(count--) { asm volatile(""); } /* client1 read the temp_value*/ printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } else { /* client2 change the val of temp_value */ temp_value = 0x12345; printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } return 0; } * Phenomenon: client1 and client2 are different instances of the same code in same group，form the above code，the symbol of "temp_value" is bss section, the temp_value of client1 and the temp_value of client2 have the same virtual address, and if the client2 change the value, client1 can perceive the change， test as below： at start, in client_1, the temp_value address is [0x659e70], value is [0x0] at start, in client_2, the temp_value address is [0x659e70], value is [0x0] at last, in client_2, the temp_value address is [0x659e70], value is [0x12345] at last, in client_1, the temp_value address is [0x659e70], value is [0x12345] * scene2 :Client code below: int temp_value = 1; int run(void) { char *name = get_instance_name(); iface_print(name); printf("at start, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); if (strcmp(name, "client_1") == 0) { int count = 1000000000; while(count--) { asm volatile(""); } /* client1 read the temp_value*/ printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } else { /* client2 change the val of temp_value */ temp_value = 0x12345; printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } return 0; } * Phenomenon: client1 and client2 are different instances of the same code in same group，form the above code，the symbol of "temp_value" is data section, the temp_value of client1 and the temp_value of client2 have the different virtual address, and if the client2 change the value, client1 can not get the change， test as below： at last, in client_2, the temp_value address is [0x445ba8], value is [0x12345] at last, in client_1, the temp_value address is [0x444008], value is [0x1] * The code of scene1 and scene2 are almost the same, except whether temp_value is initialized， the bss section or data section，but the symbol table completely different, scene1 the symbol table of g_group_bin has only one "temp_value" symbol, But scene1 the symbol table of g_group_bin has two symbols named temp_value, we also do not understand why the same name symbols of global variable should be one or two in a single address of group. It looks like random.

1 0

Can't locate VM at virtual 0?
by Richard Clark 22 Dec '21

22 Dec '21

My VM's can't seem to be untied from actual physical memory.... I've got a nice old moldy version of sel4, around version 8 I think, but it's got some life left if we can figure out how to remap our VMs to 0 instead of mapping virtual directly equal physical... In other words, for some reason, we map virtual == physical, and have to tell the VM that it is up at some high-level address. We would like to be able to pick a physical patch of memory, and map it to zero in the VM, so the VM can believe it is at 0. Honestly I don't understand why that isn't the default anyway... But I've found examples where I can specify a physical address and get back an arbitrary virtual address, and other examples where I can specify a virtual address and get back an arbitrary physical page. What I need, is a way to specify both the physical and the virtual addresses into my VM vspace. Would you happen to have an example or two on hand? For a little more context, I've got the following code, which appears to map the first page ok, but then fails trying to map the next page when called a second time: map_ram_to(vspace_t *vspace, vspace_t *vmm_vspace, vka_t* vka, uintptr_t paddr, uintptr_t vaddr) { vka_object_t frame_obj; cspacepath_t frame[2]; reservation_t res; int err; /* reserve vspace */ printf("map_ram_to, reserve phys mem at %p to vaddr %p\n", (void *)paddr, (void *)vaddr); res = vspace_reserve_range_at(vspace, (void *)paddr, 0x1000, seL4_AllRights, 1); if (!res.res) { ZF_LOGF("Failed to reserve range"); return NULL; } /* map phys addr ro frame obj */ printf("map_ram_to, alloc phys mem at %p\n", (void *)paddr); err = vka_alloc_frame_at(vka, 12, paddr, &frame_obj); if (err) { printf("ERROR VKA alloc ptr: %p\n", vka->data); ZF_LOGF("Failed vka_alloc_frame_maybe_device in devices.c"); vspace_free_reservation(vspace, res); return NULL; } vka_cspace_make_path(vka, frame_obj.cptr, &frame[0]); printf("map_ram vka_cspace_alloc_path\n"); err = vka_cspace_alloc_path(vka, &frame[1]); if (err) { ZF_LOGF("Failed vka_cspace_alloc_path"); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; } printf("map_ram vka_cnode_copy\n"); err = vka_cnode_copy(&frame[1], &frame[0], seL4_AllRights); if (err) { ZF_LOGF("Failed vka_cnode_copy"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; } err = map_page(vspace, frame_obj.cptr, (void *)vaddr, seL4_AllRights, 1, 12); vspace_free_reservation(vspace, res); if (err) { printf("FAILED Failed vspace_map_pages_at_vaddr\n"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); return NULL; } printf("map_ram_to, worked and zeroed at %p\n", (void *)paddr); return (void *)paddr; } Help is greatly appreciated! Richard H. Clark

2 1

vm physaddr != virtual?
by Richard Clark 22 Dec '21

22 Dec '21

My VM's can't seem to be untied from actual physical memory.... I've got a nice old moldy version of sel4, around version 8 I think, but it's got some life left if we can figure out how to remap our VMs to 0 instead of mapping virtual directly equal physical... In other words, for some reason, we map virtual == physical, and have to tell the VM that it is up at some high-level address. We would like to be able to pick a physical patch of memory, and map it to zero in the VM, so the VM can believe it is at 0. Honestly I don't understand why that isn't the default anyway... But I've found examples where I can specify a physical address and get back an arbitrary virtual address, and other examples where I can specify a virtual address and get back an arbitrary physical page. What I need, is a way to specify both the physical and the virtual addresses into my VM vspace. Would you happen to have an example or two on hand? For a little more context, I've got the following code, which appears to map the first page ok, but then fails trying to map the next page when called a second time: map_ram_to(vspace_t *vspace, vspace_t *vmm_vspace, vka_t* vka, uintptr_t paddr, uintptr_t vaddr) { vka_object_t frame_obj; cspacepath_t frame[2]; reservation_t res; int err; /* reserve vspace */ printf("map_ram_to, reserve phys mem at %p to vaddr %p\n", (void *)paddr, (void *)vaddr); res = vspace_reserve_range_at(vspace, (void *)paddr, 0x1000, seL4_AllRights, 1); if (!res.res) { ZF_LOGF("Failed to reserve range"); return NULL; } /* map phys addr ro frame obj */ printf("map_ram_to, alloc phys mem at %p\n", (void *)paddr); err = vka_alloc_frame_at(vka, 12, paddr, &frame_obj); if (err) { printf("ERROR VKA alloc ptr: %p\n", vka->data); ZF_LOGF("Failed vka_alloc_frame_maybe_device in devices.c"); vspace_free_reservation(vspace, res); return NULL; } vka_cspace_make_path(vka, frame_obj.cptr, &frame[0]); printf("map_ram vka_cspace_alloc_path\n"); err = vka_cspace_alloc_path(vka, &frame[1]); if (err) { ZF_LOGF("Failed vka_cspace_alloc_path"); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; } printf("map_ram vka_cnode_copy\n"); err = vka_cnode_copy(&frame[1], &frame[0], seL4_AllRights); if (err) { ZF_LOGF("Failed vka_cnode_copy"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; } err = map_page(vspace, frame_obj.cptr, (void *)vaddr, seL4_AllRights, 1, 12); vspace_free_reservation(vspace, res); if (err) { printf("FAILED Failed vspace_map_pages_at_vaddr\n"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); return NULL; } printf("map_ram_to, worked and zeroed at %p\n", (void *)paddr); return (void *)paddr; } Help is greatly appreciated! Richard H. Clark

1 0

mapping tutorial answers?
by Richard Clark 22 Dec '21

22 Dec '21

I'm interested in the ANSWERS to the MAPPING tutorial. I have my own virtual/physical memory management system and need only the ability to map a specific physical address to a specific virtual address. I can find no such thing in all the sel4 code that I have, but it appears that the mapping tutorial is what I need. Does anyone have this? (preferably arm64 and/or x64) Richard Clark

1 0

sel4-sys support
by kgugala＠antmicro.com 16 Dec '21

16 Dec '21

Hi All, We’ve been working on reviving the sel4-sys Rust crate and getting it usable again. Currently, we have it working correctly with RISC-V, we’re working on ARM (including aarch64) and X86. We’d like to contribute this work, but to have it landed we need to extend the test suite to include crate tests - especially the syscalls API. During the build, the crate generates the syscalls functions accessible from Rust code based on seL4 config. We use standard sel4test-tests suite to handle the tests: * We build the crate as static library * Sel4test is built with `-DLibSel4FunctionAttributes=public` and while linking we overwrite the original symbols with the ones from a static library from the crate This allows us to run the standard test suite against Rust syscall stubs. For now the crate generates the syscall stubs with Rust flavor, so functions signatures between Rust and C do not match. To handle this we additionally generate a thin glue code adopting Rust signatures to the C ones. We generate the Rust syscalls with a slightly modified version of the `syscall_stub_gen.py` script - we copied it into the crate’s codebase. Copying the code doesn’t seem to be the best idea - we’d need to maintain the code in both places - seL4 kernel and the crate. We’d like to merge the Rust generator with the current set of tools - is this something you’d be willing to land in the kernel code? If not, how would you see the way forward here? Thanks and best regards Karol

4 5

Re: seL4 developer hangout/video call
by Isaac Beckett 15 Dec '21

15 Dec '21

This is 4pm east coast US/EST. > The next instalment of the seL4 developer hangout is happening as planned tomorrow. It's the last one for this year: > > - Sydney: Wed, Dec 15, 8am > - Central Europe: Tue, Dec 14, 10pm > - US West Coast: Tue, Dec 14, 1pm > > Zoom link: https://unsw.zoom.us/j/82640784431 > > (There is also a separate meeting of the technical steering committee end of this week) > > Cheers > Gerwin

1 0

two questions about cteDelete of sel4 kernel 12.0.0 ?
by yadong.li 12 Dec '21

12 Dec '21

Hi： I have two questions about cteDelete of sel4 kernel 12.0.0？ IF I want to delete slot that slot->cap is cnode object(I called it level 1 cnode). The finaliseSlot function will create zombie capability and call reduceZombie(), param "immediate" is ture. the reduceZombie() call cteDelete() delete the endSlot, if the endSlot->cap is cnode capability again(I call it level 2 cnode), this time param "immediate" is false. and cteDelete() will call reduceZombie again, but because param "immediate " is false ,this time reduceZombie will not call cteDelete recursively. the reduceZombie will call capSwapForDelete, if Swap cap is not cnode or tcb, when it return to finaliseSlot, finaliseSlot will check finaliseCap, because swap cap is not cnode or tcb, almost it capRemovable, and it return directly. 1. I think when call capSwapForDelete in reduceZombie, the level 2 cnode become Cyclic zombie, but when return finaliseSlot, I do not think it will deal with below branch: if (!immediate && capCyclicZombie(fc_ret.remainder, slot)) { } because this time ,slot ->cap is not cnode or tcb, it will not create zombie cap. Who will delete level 2 cnode ? Is it lost as "Cyclic zombie", memory leak? 2. when delete cnode, it will check "preemptionPoint", if our delete is beak, even though fs_ret.success is false, but this false is not deliver to caller, who will delete cnode object again? Thank you very much

2 3

seL4 kernel does not receive PCI interrupts
by hamed_ganji＠aut.ac.ir 12 Dec '21

12 Dec '21

Hi all, I have created a simple CAMKES-VM-x86 app for a PC but its PCI devices are not working due to not receiving corresponding interrupts. By adding a printf to the function "handleInterrupt" inside the seL4 kernel I found that only some limited interrupts such as timer and serial are received. However, capdl_spec.c file contains all necessary declaration of capabilities and objects for the required interrupts such as follows, ... [19625] = { #ifdef CONFIG_DEBUG_BUILD .name = "vm0_irq_10", #endif .type = CDL_IOAPICInterrupt, .slots.num = 1, .slots.slot = (CDL_CapSlot[]) { {0, {.type = CDL_NotificationCap, .obj_id = 19567 /* vm0_irq_notification_obj_10 */, .is_orig = true, .rights = (CDL_CanRead), .data = { .tag = CDL_CapData_Badge, .badge = 0}}}, }, .ioapicirq_extra = { .ioapic = 0, .ioapic_pin = 10, .level = 1, .polarity = 1, }, }, ... and the host endpoint of the VMM thread is properly set to receive IRQ notifications and route them to VM, and the IOAPIC pin number (source) is also true, I checked. How can I solve the problem? Any pointers would be appreciated. Kind regards, Hamed

1 0

Nvidia Tegra SoCs: Has anyone tried running seL4 on them?
by Isaac Beckett 12 Dec '21

12 Dec '21

Has anyone experimented with running seL4 on Tegra SoCs? I’m interested mainly because I own a Nintendo Switch console that is vulnerable to an exploit in the boot rom that allows for booting arbitrary payloads. Most people use it to run modified versions of the official firmware, or to run Linux or Android, so the hardware is at least decently well reverse engineered at this point, and there are even proper Linux drivers for the joy-con detachable controllers. I’m interested in attempting to run seL4 on this device, mostly to see if I can, but I figured I’d ask here first to see if anyone’s attempted similar hardware.

2 2

next seL4 TSC meeting on Fri 17 Dec (16 Dec in US and Europe)
by Gerwin Klein 11 Dec '21

11 Dec '21

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Fri, 17 Dec, 8am - Central Europe: Tue, 16 Dec, 10pm - US West Coast: Tue, 16 Dec, 1pm The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/82827057586 Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: - update on GitHub status, test stability, etc - release schedule - change main verification platform to imx8? - RFCs: - Core Platform https://sel4.atlassian.net/browse/RFC-5 - Removing CNode Mutate https://sel4.atlassian.net/browse/RFC-7 - SMC calls https://sel4.atlassian.net/browse/RFC-9 If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html

1 0

two questions about cteDelete of sel4 kernel？
by yadong.li 11 Dec '21

11 Dec '21

Hi： I have two questions about cteDelete of sel4 kernel？ IF I want to delete slot that slot->cap is cnode object(I called it level 1 cnode). The finaliseSlot function will create zombie capability and call reduceZombie(), param "immediate" is ture. the reduceZombie() call cteDelete() delete the endSlot, if the endSlot->cap is cnode capability again(I call it level 2 cnode), this time param "immediate" is false. and cteDelete() will call reduceZombie again, but because param "immediate " is false ,this time reduceZombie will not call cteDelete recursively. the reduceZombie will call capSwapForDelete，it will swap zombie cap with slot 0 of level 2 cnode, if Swap cap(slot0 of level 2 cnode) is not cnode or tcb(the cnode object slot 0 must point to cnode self ? I did not find this limitation), when it return to finaliseSlot, finaliseSlot will check finaliseCap, because swap cap is not cnode or tcb, almost it call be capRemovable, and it return directly. 1. I think when call capSwapForDelete in reduceZombie, the level 2 cnode become Cyclic zombie, but when return finaliseSlot, I do not think it will deal with below branch: if (!immediate && capCyclicZombie(fc_ret.remainder, slot)) { } because this time ,slot ->cap is not cnode or tcb, it will not create zombie cap. then Who will delete level 2 cnode ? Is it lost as "Cyclic zombie", memory leak? 2. when delete cnode, it will check "preemptionPoint", if our delete is beak, even though fs_ret.success is false, but this false is not deliver to caller who will delete it again? thank you for your help

1 0

How can I port the seL4 microkernel to my unofficially verified hardware？
by yjy 10 Dec '21

10 Dec '21

Does the document provide relevant information or project? I read related articles and I can be sure that my instruction set is common. Thank you.

2 1

Troubles booting VM with large memory(e.g VM_RAM_SIZE >= 2048MB)
by Han JingLong 韩景龙 09 Dec '21

09 Dec '21

Hello all, Reference to seL4 Docs/Projects/CAmkES ARM VMM, I have successfully run a VM (a Linux guest OS and config VM_RAM_SIZE = 1024MB) on a new ARM(ArmV8a CortexA55) platform. But when I tried to increase the ram size assigned to VM, I encountered the following error: ============================================================================== ram_ut_alloc_iterator@guest_ram.c:295 Failed to allocate page map_vm_memory_reservation@guest_memory.c:470 Failed to get frame for reservation address 0xae7c0000 reservation_size:60000000 …… vm_ram_touch@guest_ram.c:160 Failed to touch ram region: Not registered RAM region 32 bit ARM insts not decoded Pagefault from [Linux]: write fault @ PC: 0xffff000008d9132c IPA: 0xaffff000, FSR: 0x92000046 Context: x0: 0xffff7dfffe639000 x1: 0x0 x2: 0xfc0 x3: 0x4 x4: 0x0 x5: 0x40 x6: 0x3f x7: 0x0 x8: 0xffff7dfffe639000 x9: 0x0 x10: 0x1000 x11: 0x6f01c3b8 x12: 0xc0000000 pc: 0xffff000008d9132c x14: 0x0 sp: 0xffff000009668d80 spsr: 0x40000085 x13: 0x60000000 x15: 0x4 x16: 0x1800 x17: 0xffff7dfffe81c3b4 x18: 0x8 x19: 0xaffff000 x20: 0xffff0000096a1fd0 x21: 0xffff7dfffe80009c x22: 0x58389df x23: 0xffff0000091ce000 x24: 0x4b78e0 x25: 0x47b87c x26: 0x0 x27: 0xa0000000047b818 x28: 0x614f0018 x29: 0xffff000009643eb0 x30: 0xffff0000094f7ad0 m-------- Assertion failed: rt >= 0 (/home/hjl/workdir/vmm_sel4_sdx_android/projects/seL4_projects_libs/libsel4vm/src/arch/arm/fault.c: fault_get_width: 623) Attach config file for reference： 1. overlay dts reserved-memory { #address-cells = < 0x02 >; #size-cells = < 0x02 >; ranges; vm-memory@60000000 { reg = < 0x00 0x60000000 0x00 0x60000000 >; no-map; }; }; 1. devices.camkes #define VM_INITRD_MAX_SIZE 0x5000000 //80 MB #define VM_RAM_BASE 0x60000000 #define VM_RAM_OFFSET 0 #define VM_RAM_SIZE 0x60000000 #define VM_DTB_ADDR 0x6F000000 #define VM_INITRD_ADDR 0x6A000000 vm0.untyped_mmios = [ “0x35436000:12”, // Interrupt Controller Virtual CPU interface (Virtual Machine view) /* The purpose of these untyped regions is to force the untyped * allocator to treat this memory region as reserved so that when we * try to ensure that the VMM is placed into this region in RAM, it * will definitely be available for placement. * * This address pertains to vm-memory@60000000 in the overlay DTS */ “0x60000000:28”, // RAM “0x70000000:28”, // RAM “0x80000000:28”, // RAM “0x90000000:28”, // RAM “0xa0000000:28”, // RAM “0xb0000000:28”, // RAM ]; 1. guest linux dts memory@60000000 { device_type = “memory”; reg = <0x00 0x60000000 0x00 0x60000000>; }; ============================================================================== In contrast, I tried to expand the VM memory based on QEMU and encountered the same problem. Attach config file for reference： 1. settings.cmake if(${PLATFORM} STREQUAL “qemu-arm-virt”) set(QEMU_MEMORY “4096”) set(KernelArmCPU cortex-a53 CACHE STRING “” FORCE) set(VmInitRdFile ON CACHE BOOL “” FORCE) endif() 1. overlay-reserve-vm-memory.dts reserved-memory { #address-cells = < 0x02 >; #size-cells = < 0x02 >; ranges; vm-memory@40000000 { reg = <0x0 0x40000000 0x0 0x50000000>; no-map; }; }; 1. devices.camkes #define VM_INITRD_MAX_SIZE 0x1900000 //25 MB #define VM_RAM_BASE 0x40000000 #define VM_RAM_SIZE 0x50000000 #define VM_RAM_OFFSET 0x00000000 #define VM_DTB_ADDR 0x4F000000 #define VM_INITRD_ADDR 0x4D700000 vm0.untyped_mmios = [ “0x8040000:12”, // Interrupt Controller Virtual CPU interface (Virtual Machine view) “0x40000000:29”, // Linux kernel memory regions “0x60000000:29”, // Linux kernel memory regions “0x80000000:28”, // Linux kernel memory regions ]; 1. guest linux dts memory@40000000 { reg = <0x0 0x40000000 0x0 0x50000000>; device_type = “memory”; }; Is there any memory limit for VM? or Configuration problem? Anyways anyone any help can provide would be awesome and thanks in advance for any help! 邮件免责申明 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

getKernelWcetUs: where does the 10us return value come from?
by Jack Chen 09 Dec '21

09 Dec '21

Hi all, Quick questions regarding the return value of getKernelWcetUs(): 1. For ARM the value is assigned during build process taking config.cmake files, where KERNEL_WCET's are all 10us (except for tk1 it's 100us, typo?) For x86 the function returns 10 directly, and for risc-v, comment suggests it's copied from x86 hoping it's an overestimate. Where does this "10us" come from? Based on static estimate done previously on Armv6 (imx31)? AOS lecture mentioned a "378us" kernel WCET estimate and 99.5us observed WCET for Armv6. 2. Is this 10us WCET value the one used as padding in the Temporal Partitioning routine? ("worst-case flushing time"?) Regards, Jack

3 5

Incorporating seL4 into your project, risc-v architecture
by so_s＠gmx.de 08 Dec '21

08 Dec '21

Dear seL4 devs and community. I try to create a simple project using the seL4 micro kernel. For setting up my environment I followed this (https://github.com/manu88/SeL4_101) and this (https://docs.sel4.systems/projects/buildsystem/incorporating.html) article. As kernel I'm using the last release of SeL4 (https://github.com/seL4/seL4/releases/tag/12.1.0) I created some kind of user application, like Manu88 did with a simple Hello World C-Program. While building with the delivered init-build.sh script I got a lot of repeating errors like this: CMake Error at tools/cmake-tool/helpers/simulation.cmake:179 (add_custom_command): Error evaluating generator expression: $<TARGET_PROPERTY:rootserver_image,KERNEL_IMAGE_NAME> Target "rootserver_image" not found. Call Stack (most recent call first): CMakeLists.txt:22 (GenerateSimulateScript) While going through Manu88s guide I saw that he also got this errors. But after adding a CMakeList.txt file inside his user code, and declaring it as rootserver inside the CMakeList.txt file (I just copied the contents from here: https://github.com/manu88/SeL4_101/blob/master/projects/Hello/CMakeLists.txt) he got rid of the errors. I still get them and searching through the internet could not find a solution for me. Bellow I added the folder structure of my project. Project/ ├── kernel/ ├── projects/ │ ├── Hello/ │ ├── musllibc/ │ ├── utils_libs/ │ ├── seL4_libs/ ├── build/ ├── tools/ │ └── cmake-tool/ │ └── elfloader-tool/ ├── init-build.sh -> tools/cmake-tool/init-build.sh ├── CMakeLists.txt ├── application_settings.cmake -> tools/cmake-tool/helpers/application_settings.cmake ├── settings.cmake So I cannot tell where the issue lies. Any pointers would be appreciated. Kind regards, Sophia

2 3

capdl-loader questions
by Sam Leffler 08 Dec '21

08 Dec '21

I've been investigating how capd-loader works and have some questions. My apologies if these were previously discussed. 1. CDL_Model is mutable. The capDL specification looks like a perfect candidate for being in .rodata but it's stored+treated as mutable. Why? I see capdl-loader uses the mutability to store mapped page frame caps and, for risc-v, VSpace roots, but both can be easily handled w/o modifying the spec. Having this immutable has many benefits. 2. All page frames are treated as shared. CAPDL_SHARED_FRAMES is #define'd in the code so every frame is treated as shared. This inflates the size of the orig_caps array and the kernel capabilities table but seems unnecessary. Why? I've verified that instead of doing the Copy op on each page you can just check the return of the seL4_Page_Map call and if necessary clone the cap. Better would be for camkes to identify shared page frames so this doesn't require 2x syscalls (which spam's the console w/ CONFIG_PRINTING enabled). 3. Why does copy_addr_with_pt exist? There are two memory regions created for mapping page frames into the rootserver address space for doing fill ops. One is 64KB and the other is 1 page (nominally 4KB). init_frame tries the 4KB region first then falls back to the 64K region if mapping into the 4KB region fails. Why (i.e. why would the 1st mapping call fail)? On my risc-v system I never use the 64K region and I'm not sure when it might be used? Even if it were used, why is 64K always allocated; seems like the region should be sized according to the target platform. Having this extra region has a cost that can be significant on small systems. 4. console output. Why is sel4_DebugPutChar (or similar) not a standard part of the kernel? This forces capdl-loader to depend on libsel4platsupport for console output which in turn affects cap space. I can't imagine an seL4 system that cannot write to the console and I think it's entirely reasonable to have a critical system service like the rootserver use that. 5. duplicate_caps. The scheme for constructing a running system from a spec is straightforward except for duplicating caps. Why are all TCB's and CNode caps dup'd? Why does init_tcbs call init_tcb on the original object but immediately configure_tcb on the dup? There are other places where the dup cap is used instead of the original cap (e.g. init_cnode_slot). None of this seems to matter on risc-v; maybe this matters on some other architectures? 6. On risc-v all pages appear to be marked executable--including ipc buffers! This seems just wrong and a potential security hole. 7. Why does seL4_TCB_WriteRegisters take a _mutable_ seL4_UserContext? I'm guessing this is a mistake in the xml spec (but haven't looked). 8. init_cspaces mystifies me. There are two loops over all CNodes; one that does "COPY" operations and one that does "MOVE" operations. I see nothing explaining what's happening. I've read this code many times and still don't get it; please explain. 9. According to comments, the use of a global static to setup the UserContext for a new TCB is done because one cannot take the address of a local variable. On what architecture is this true? On risc-v the context is copied into "registers" before calling the kernel so this doesn't appear to be an issue with crossing the user-kernel protection boundary. 10. Memory reclamation. I'm unclear what happens to the memory used by capdl-loader. The process does a TCB_Suspend call when it's done. Does this cause the CSpace & VSpace to be reclaimed? For CAmkES this doesn't matter as there's no support for allocating memory but I'm building a system where this isn't true. How do I release memory (in particular) back to the untyped pool? I have a bunch of niggly code complaints/questions but let's start with the above. -Sam

2 4

Re: some performance problem when test 4 cores SMP答复: Devel Digest, Vol 127, Issue 5
by yadong.li 07 Dec '21

07 Dec '21

Hi: > So you would expect that the reported metric would scale following Amdahl's law based on the proportion of an operation that is serialized inside the kernel lock which would potentially vary across platforms. > It cannot simply be throughput, else the doubled delay should be reflected in a significantly reduced throughput, but it has almost no effect. 1. This is what I also feel confused, I think whether it is depend on the implementation of ipc_normal_delay ipc_normal_delay will call below code: delay = OVERHEAD_FIXUP(REXP(id) * current_delay_cycle, overhead); insert a command such as 'zigset(...)'for every core, The ziggurat method for generating random variables, when double delay, the random variables coefficient will reduce the delay influence? 2. " the proportion of an operation that is serialized inside the kernel lock ", CLH lock is serialized between cores, if 4 cores will have big different performance on different ARM platform? > For 3 or 4 cores the combined latency of two IPCs is larger than the 500cy delay and you expect lock contention, resulting in reduced scaling, while it should still scale almost perfectly with the 1000cy delay. > > > Addition： > > Our seL4_Call performance is same with other platform > > XXXX IMX8MM_EVK_64 TX2_64 > > seL4_Call 367(0) 378(2) 492(16) client->server, same vspace, ipc_len is 0 > > seL4_ReplyRecv 396(0) 402(2) 513(16) server->client, same vspace, ipc_len is 0 1. the seL4_Call and seL4_ReplyRecv are measured on SMP kernel 2. or 3 or 4 cores the combined latency of two IPCs is larger than the 500cy delay and you expect lock contention ---- that's what I thought at first, But It can't be explained very well on IMX8MM_EVK_64, base on the test seL4_Call data, when run on 3 cores and 4cores, IMX8MM_EVK_64 still have a good scalability, so I think not all seL4_Call and ReplyRecv flow which cost maybe 300 or 400 is locked(like el trap), TX2 should have a good scalability as expected when run on 3 or 4 cores, but it did not show good, from data below：1497740（3core， 500cycles），1545872（4core） > > My test results below: > > ARM platform > > Test item XXX IMX8MM_EVK_64 TX2 > > mean(Stddev) > > 500 cycles, 1 core 636545(46) 625605(29) 598142(365) > > 500 cycles, 2 cores 897900(2327) 1154209(44) 994298(94) > > 500 cycles, 3 cores 1301679(2036) 1726043(65) 1497740(127) > > 500 cycles, 4 cores 1387678(549) 2172109(12674) 1545872(109) > > 1000 cycles, 1 core 636529(42) 625599(22) 597627(161) > > 1000 cycles, 2 cores 899212(3384) 1134110(34) 994437(541) > > 1000 cycles, 3 cores 1297322(5028) 1695385(45) 1497547(714) > > 1000 cycles, 4 cores 1387149(456) 2174605(81) 1545716(614) > I notice your standard deviations for 2 and 3 cores are surprisingly high (although still small in relative terms). > > Did you try running the same again? Are the numbers essentially the same or are multiple runs all over the shop? 1. Yes，I test several times，I always get the same results, have little different 2. I think the stddev is small relative to our test results, IMX8MM_EVK_64 also have a big stddev(500 cycles, 3core) from the data. -----邮件原件----- 发件人: devel-request(a)sel4.systems [mailto:devel-request@sel4.systems] 发送时间: 2021年12月7日 11:45 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 127, Issue 5 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: Use TimeServer by Group Components Questions (Kent Mcleod) 2. Re: Incorporating seL4 into your project, risc-v architecture (Kent Mcleod) 3. Re: some performance problem when test 4 cores SMP benchmark of seL4bench project 答复: Devel Digest, Vol 127, Issue 1 (Kent Mcleod) 4. Re: Use TimeServer by Group Components Questions (15852538526(a)139.com) 5. Re: Use TimeServer by Group Components Questions (Kent Mcleod) 6. Re: some performance problem when test 4 cores SMP benchmark of seL4bench project 答复: Devel Digest, Vol 127, Issue 1 (Gernot Heiser) ---------------------------------------------------------------------- Message: 1 Date: Tue, 7 Dec 2021 13:03:00 +1100 From: Kent Mcleod <kent.mcleod72(a)gmail.com> Subject: [seL4] Re: Use TimeServer by Group Components Questions To: 15852538526(a)139.com Cc: devel <devel(a)sel4.systems> Message-ID: <CA+-ozWeJgZm3B902EKBU6dUGxy6wU3Cp92jEUYwRKNFcVS=7DA(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" On Fri, Dec 3, 2021 at 2:51 PM <15852538526(a)139.com> wrote: > > I got an problem when I use TimeServer with Group Components. I wish more than one component in the same Group Components, that can use TimeServer. While the cdl only have one ep for all components in the Group to communicate to TimeServer with an badge value that not equal to zero. And TimeServer must to distinguish requester by the badge, so only one component can receive TimeServer's response. How can I resolve this problem? The TimeServer component cannot be used as part of a Group component. The Group component mechanism isn't designed to transparently work for any component and the Connection types that the TimeServer uses are not compatible with the Group mechanism. > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email > to devel-leave(a)sel4.systems ------------------------------ Message: 2 Date: Tue, 7 Dec 2021 13:14:30 +1100 From: Kent Mcleod <kent.mcleod72(a)gmail.com> Subject: [seL4] Re: Incorporating seL4 into your project, risc-v architecture To: so_s(a)gmx.de Cc: devel <devel(a)sel4.systems> Message-ID: <CA+-ozWeU7Bi-byXhsvo9jnQ_tcn90U7QRa8_hh39p2rVgUcKzA(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" On Fri, Dec 3, 2021 at 8:14 AM <so_s(a)gmx.de> wrote: > > Dear seL4 devs and community. > > I try to create a simple project using the seL4 micro kernel. For setting up my environment I followed this (https://github.com/manu88/SeL4_101) and this (https://docs.sel4.systems/projects/buildsystem/incorporating.html) article. As kernel I'm using the last release of SeL4 (https://github.com/seL4/seL4/releases/tag/12.1.0) I created some kind of user application, like Manu88 did with a simple Hello World C-Program. While building with the delivered init-build.sh script I got a lot of repeating errors like this: > CMake Error at tools/cmake-tool/helpers/simulation.cmake:179 (add_custom_command): > Error evaluating generator expression: > > $<TARGET_PROPERTY:rootserver_image,KERNEL_IMAGE_NAME> > > Target "rootserver_image" not found. > Call Stack (most recent call first): > CMakeLists.txt:22 (GenerateSimulateScript) While going through > Manu88s guide I saw that he also got this errors. But after adding a CMakeList.txt file inside his user code, and declaring it as rootserver inside the CMakeList.txt file (I just copied the contents from here: https://github.com/manu88/SeL4_101/blob/master/projects/Hello/CMakeLists.txt) he got rid of the errors. I still get them and searching through the internet could not find a solution for me. Bellow I added the folder structure of my project. > Project/ > ├── kernel/ > ├── projects/ > │ ├── Hello/ > │ ├── musllibc/ > │ ├── utils_libs/ > │ ├── seL4_libs/ > ├── build/ > ├── tools/ > │ └── cmake-tool/ > │ └── elfloader-tool/ > ├── init-build.sh -> tools/cmake-tool/init-build.sh > ├── CMakeLists.txt > ├── application_settings.cmake -> > tools/cmake-tool/helpers/application_settings.cmake > ├── settings.cmake > > So I cannot tell where the issue lies. Any pointers would be appreciated. If you are using https://github.com/manu88/SeL4_101/blob/master/projects/Hello/CMakeLists.txt inside projects/Hello/ then you need to make sure that the top level CMakeLists inside Project/ is either a symlink to tools/cmake-tool/default-CMakeLists.txt or is similar to https://github.com/manu88/SeL4_101/blob/master/CMakeLists.txt. With this file layout, ../init-build.sh will end up calling the following CMake invocation: `cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DSEL4_CACHE_DIR=../.sel4_cache -C "../settings.cmake" "../"`. What is the contents of your settings.cmake file? > > Kind regards, > Sophia > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email > to devel-leave(a)sel4.systems ------------------------------ Message: 3 Date: Tue, 7 Dec 2021 13:43:48 +1100 From: Kent Mcleod <kent.mcleod72(a)gmail.com> Subject: [seL4] Re: some performance problem when test 4 cores SMP benchmark of seL4bench project 答复: Devel Digest, Vol 127, Issue 1 To: Gernot Heiser <gernot(a)unsw.edu.au> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <CA+-ozWcihN6my4WOyPbpCcfp3=rksYSnnEgZE2kc6c-BV4Kymw(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" On Thu, Dec 2, 2021 at 9:28 PM Gernot Heiser <gernot(a)unsw.edu.au> wrote: > > > > > On 2 Dec 2021, at 16:17, yadong.li <yadong.li(a)horizon.ai> wrote: > > > > First, I got the data of IMX8MM_EVK_64 and TX2 from > > https://github.com/seL4/sel4bench/actions/runs/1469475721#artifacts, > > the sel4bench-results-imx8mm_evk file and sel4bench-results-tx2 file, unpack the file out, I find xxxx_SMP_64.json Secondly, the test is the smp benchmark form sel4bench-manifest project, the source file is sel4bench/apps/smp/src/main.c The test scenario look like below: > > A pair thread of ping-pong on the same core, the ping thread will > > wait for "ipc_normal_delay" time then send 0 len ipc message to pong > > thread, then return. I think the 500 cycles mean how long > > ipc_normal_delay will really delay > > > The above scenario will test on one core, or mutil core. If we run 4 cores, every core will have a ping thread and a pong thread run like above description, then record the sum of all cores ping-pong counts. > > ok, but what is the metric reported? [Apologies for not being on top > of the details of our benchmarking setups.] Looking at the sel4bench smp benchmark implementation, the metric is the total number of "operations" in a single second. An operation is a round trip intra address space seL4_Call + seL4_ReplyRecv between 2 threads on the same core with each thread delaying for the cycle count before performing the next operation. After 1 second of all cores performing these operations continuously and maintaining a core-local (on a separate cache line) count, the total number of operations is added together and reported as the final number. So you would expect that the reported metric would scale following Amdahl's law based on the proportion of an operation that is serialized inside the kernel lock which would potentially vary across platforms. > > It cannot simply be throughput, else the doubled delay should be reflected in a significantly reduced throughput, but it has almost no effect. > > > I think this experiment is used to illustrate in multi core, our seL4 kernel big lock will not affect mutli-core performance, am I right ? > > Not quite. As there’s only one big lock, only one core can execute the kernel at any time. If one core is in the IPC while another core is trying to IPC, even though both IPCs are core-local, the second will have to wait until the first gets out of the lock. > > As the delay is higher than the syscall latency, you’d expect perfect scalability from one core to two (with the lock essentially synchronising the threads). For 3 or 4 cores the combined latency of two IPCs is larger than the 500cy delay and you expect lock contention, resulting in reduced scaling, while it should still scale almost perfectly with the 1000cy delay. This is exactly what you see for the i.MX8 and the TX2. > > > Addition： > > Our seL4_Call performance is same with other platform > > XXXX IMX8MM_EVK_64 TX2_64 > > seL4_Call 367(0) 378(2) 492(16) client->server, same vspace, ipc_len is 0 > > seL4_ReplyRecv 396(0) 402(2) 513(16) server->client, same vspace, ipc_len is 0 > > OK, so baseline performance is good. But are these measured on a single-core or SMP kernel (i.e. is locking included)? > > > My test results below: > > ARM platform > > Test item XXX IMX8MM_EVK_64 TX2 > > mean(Stddev) > > 500 cycles, 1 core 636545(46) 625605(29) 598142(365) > > 500 cycles, 2 cores 897900(2327) 1154209(44) 994298(94) > > 500 cycles, 3 cores 1301679(2036) 1726043(65) 1497740(127) > > 500 cycles, 4 cores 1387678(549) 2172109(12674) 1545872(109) > > 1000 cycles, 1 core 636529(42) 625599(22) 597627(161) > > 1000 cycles, 2 cores 899212(3384) 1134110(34) 994437(541) > > 1000 cycles, 3 cores 1297322(5028) 1695385(45) 1497547(714) > > 1000 cycles, 4 cores 1387149(456) 2174605(81) 1545716(614) > > I notice your standard deviations for 2 and 3 cores are surprisingly high (although still small in relative terms). > > Did you try running the same again? Are the numbers essentially the same or are multiple runs all over the shop? > > There are some issues with our benchmarking methodology. Fixing up sel4bench is one of the projects I’d like to do if I got a student for it, or maybe someone from the community would want to help? > > But just from looking at the data I’m not sure that’s the issue here. > > Gernot > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email > to devel-leave(a)sel4.systems ------------------------------ Message: 4 Date: Tue, 07 Dec 2021 03:06:38 -0000 From: 15852538526(a)139.com Subject: [seL4] Re: Use TimeServer by Group Components Questions To: devel(a)sel4.systems Message-ID: <163884639883.1070957.2394639262660252936(a)mattermost.seL4.systems> Content-Type: text/plain; charset="utf-8" Thank you very much for answering my question. I still have a doubt about the TimeServer. I can manually modify the cdl file and then I get the the expected source file(capdl_spec.c) from using capdl-parse. I also need to change the return value of timeserver <IF>_notification API. I have try and I can run the program as I expected. Is there any way to create adapted cdl file automatic by modifying the ADL parse project? I am looking forward to getting your answer again. Thank you very much. my ADL file: import <std_connector.camkes>; import <global-connectors.camkes>; import <TimeServer/TimeServer.camkes>; component Client { control; uses Timer timeout; } assembly { composition { group grp { component Client c1; component Client c2; } component TimeServer time_server; connection seL4TimeServer ts1( from grp.c1.timeout, to time_server.the_timer); connection seL4TimeServer ts2( from grp.c2.timeout, to time_server.the_timer); } configuration { time_server.timers_per_client = 1; } } ------------------------------ Message: 5 Date: Tue, 7 Dec 2021 14:23:54 +1100 From: Kent Mcleod <kent.mcleod72(a)gmail.com> Subject: [seL4] Re: Use TimeServer by Group Components Questions To: 15852538526(a)139.com Cc: devel <devel(a)sel4.systems> Message-ID: <CA+-ozWestyqAM4wy+x359CLZLf13PzdCRBNFSfPY-3nyo9Y6wA(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" On Tue, Dec 7, 2021 at 2:09 PM <15852538526(a)139.com> wrote: > > Thank you very much for answering my question. I still have a doubt about the TimeServer. I can manually modify the cdl file and then I get the the expected source file(capdl_spec.c) from using capdl-parse. I also need to change the return value of timeserver <IF>_notification API. I have try and I can run the program as I expected. Is there any way to create adapted cdl file automatic by modifying the ADL parse project? There isn't a supported way to modify the generated cdl file as CAmkES expects to generate a full system specification. What is your motivation for trying to make the timeserver a group component instead of a separate component? As part of a group component it will still have its own kernel objects for its threads, code, data and heap memories so you still have the costs of isolation but without the benefits because it still shares the virtual address space and capability space with other components in the same group. > I am looking forward to getting your answer again. Thank you very much. > > my ADL file: > import <std_connector.camkes>; > import <global-connectors.camkes>; > import <TimeServer/TimeServer.camkes>; > > component Client { > control; > uses Timer timeout; > } > > assembly { > composition { > group grp { > component Client c1; > component Client c2; > } > component TimeServer time_server; > > connection seL4TimeServer ts1( > from grp.c1.timeout, to time_server.the_timer); > connection seL4TimeServer ts2( > from grp.c2.timeout, to time_server.the_timer); > } > > configuration { > time_server.timers_per_client = 1; > } > } > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email > to devel-leave(a)sel4.systems ------------------------------ Message: 6 Date: Tue, 7 Dec 2021 03:45:09 +0000 From: Gernot Heiser <gernot(a)unsw.edu.au> Subject: [seL4] Re: some performance problem when test 4 cores SMP benchmark of seL4bench project 答复: Devel Digest, Vol 127, Issue 1 To: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <17FC6BC4-3407-44AE-B7AA-4623EFF76988(a)unsw.edu.au> Content-Type: text/plain; charset="utf-8" On 7 Dec 2021, at 13:43, Kent Mcleod <kent.mcleod72(a)gmail.com> wrote: > > Looking at the sel4bench smp benchmark implementation, the metric is > the total number of "operations" in a single second. An operation is > a round trip intra address space seL4_Call + seL4_ReplyRecv between 2 > threads on the same core with each thread delaying for the cycle count > before performing the next operation. After 1 second of all cores > performing these operations continuously and maintaining a core-local > (on a separate cache line) count, the total number of operations is > added together and reported as the final number. So you would expect > that the reported metric would scale following Amdahl's law based on > the proportion of an operation that is serialized inside the kernel > lock which would potentially vary across platforms. Thanks for the explanation, Kent. Observations: 1) The metric is essentially independent of the delay. Looking at the single-core figures for the i/MX8, I get 1598.5 ns in both cases, the difference being 15ps. Doesn’t make sense to me. 2) Assuming this processor runs at the 1.8GHz it seems speced for, this corresponds to 2877 cycles, which is huge, even if the 1000cy delay is subtracted! 3) As I said before, intra-AS IPC is a meaningless metric we should never use (but that’s incidental to the particular thing we want to measure here). 4) Having to do these calculations to understand the numbers is a sure indication that the results are presented in an unsuitable form. I can’t see how these figures make sense. Gernot ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems ------------------------------ End of Devel Digest, Vol 127, Issue 5 *************************************

1 0

CfP: Microkernel and Component-based OS Devroom at FOSDEM 2022
by Alexander Boettcher 07 Dec '21

07 Dec '21

Hello seL4 community, FOSDEM 2022 will be an online event (again) with the traditional Microkernel devroom as part of it. Thanks to Martin Decky & my colleague Sebastian Sumpf for engagement! The original Call for Papers follows. Best regards, Alexander. -- Alexander Boettcher Genode Labs https://www.genodians.org - https://www.genode.org ------------------------------------------------------------------------------------------------------ Microkernel and Component-based OS Devroom at FOSDEM 2022 CALL FOR PARTICIPATION On-line version of this CfP: http://fosdem.microkernel.info/ The developers and users of several free and open source microkernel-based and component-based operating systems will meet on-line as part of FOSDEM 2022 [1] and will share a developer room. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-based, unikernel-based, component-based operating systems and similar topics. The devroom has been preliminarily scheduled to Saturday February 5th 2022. The devroom will take place during European day hours. Possible topics of the devroom include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * languages, tools and toolchains used * enabling support for hardware (architectures, device drivers) and programming languages * development processes, debugging * maintenance, testing and release engineering * safety, security and robustness * trends and challenges * research and open questions * community and governance * use cases, experiences and status updates * best practices and lessons learned * demos This is a call for your participation. We kindly ask you to submit your proposals no later than on December 28th 2021. Please use the Pentabarf web site [2] to submit your proposals. If you already have a user account in Pentabarf, please do not create a new one. Addtionally, make sure to select the Microkernel and Component-based OS Devroom as the track when submitting your talk and include at least the following information in your proposal: * title of your talk * your full name * short abstract of your talk (one or two paragraphs) * duration of your talk (at least 20 minutes and no longer than 50 minutes) * your short bio * your photo The talks will be pre-recorded in advance in January and streamed automatically during the event. This means that you will need to complete and submit your talk recording by January 15th 2022. However, each speaker should be also present on-line just after the streaming of their talk for a live Q&A. You can specify your prefered time slot of your talk. The communication language of the devroom is English. The official devroom schedule (along with the accepted talks) will be announced on December 31st 2021 on the devroom's mailing list [3] and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM web site. For any comments, questions and suggestions (e.g. suggestions for a different type of event during the devroom), please do not hesitate to use the devroom's mailing list [3]. About the Devroom Since the first Microkernel OS Devroom at FOSDEM 2012 [4], this devroom has been a part of each following FOSDEM (with slight variations of the name). The focus gradually widened to include component-based, unikernel-based and other operating systems. By now, it has become a somewhat institutionalized tradition for the open source operating systems community and it is one of the few places where microkernel enthusiasts and people with different views on how operating systems should work meet regularly. To this date, over a dozen projects have participated in one way or another. Many of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. Extraordinary Circumstances in 2022 (Again) Due to the extraordinary mode of organization of FOSDEM 2022 (being an on-line event again), the devroom talks will be required to be pre-recorded in January and streamed during the event (with a live Q&A). The talk videos will be published under Creative Commons license by FOSDEM. By submitting a recorded talk, the speaker agrees to have it made available publicly indefinitively. For organizational purposes, we also need contact information of the speakers of accepted talks. Please check the official CfP page [5] of the devroom regularly. We will keep updating it as technical guidelines will be set by the FOSDEM organizers. Microkernel Dinner Sadly, it will not be possible to arrange our traditional microkernel dinner and other in-person social gatherings in Brussels this time again. However, we plan a closing event of the devroom as a loose approximation of the microkernel dinner. The details will be announced later. We encourage the on-line participats to bring their own food and beverages. About FOSDEM FOSDEM [6] is a two-day event organized by volunteers to promote the widespread use of free and open source software. FOSDEM is widely recognized as one of the best such conferences worldwide. FOSDEM covers a wide spectrum of free and open source software and hardware projects and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and proposals. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. In recent years, FOSDEM has been hosting more than 5000 developers annually at the ULB Solbosch campus. Due to the circumstances, FOSDEM 2022 will be organized as an on-line event. The participation in FOSDEM is totally free, although the organizers gratefully accept donations and sponsorship. No registration is necessary, but attendees are expected to follow the FOSDEM's code of conduct [7]. Important Dates Recap * 2021-12-28: Deadline for talk proposal submission * 2021-12-31: Schedule published and speakers notified of acceptance * 2022-01-15: Deadline for talk pre-recoding submission * 2022-02-05: Devroom taking place on-line Contact In case of any comments, questions and suggestions, please do not hesitate to contact the devroom organizers via the devroom's mailing list [3]. The primary organizers of the devroom in 2022 are: * Sebastian Sumpf * Martin Decky Links [1] https://fosdem.org/2022/ [2] https://penta.fosdem.org/submission/FOSDEM22/ [3] https://lists.fosdem.org/listinfo/microkernel-devroom [4] https://archive.fosdem.org/2012/schedule/track/microkernel_os_devroom.html [5] http://fosdem.microkernel.info/ [6] https://fosdem.org/ [7] https://fosdem.org/2022/practical/conduct/

1 0

Use TimeServer by Group Components Questions
by 15852538526＠139.com 07 Dec '21

07 Dec '21

I got an problem when I use TimeServer with Group Components. I wish more than one component in the same Group Components, that can use TimeServer. While the cdl only have one ep for all components in the Group to communicate to TimeServer with an badge value that not equal to zero. And TimeServer must to distinguish requester by the badge, so only one component can receive TimeServer's response. How can I resolve this problem?

2 4

Re: some performance problem when test 4 cores SMP benchmark of seL4bench project 答复: Devel Digest, Vol 127, Issue 1
by yadong.li 07 Dec '21

07 Dec '21

Hi professor Heiser： To understand what’s going on I’d need to know what these numbers are: - what is being measured, and what’s the 500/100cy parameter? - which web site are the “official” numbers from, they aren’t at https://sel4.systems/About/Performance/ First, I got the data of IMX8MM_EVK_64 and TX2 from https://github.com/seL4/sel4bench/actions/runs/1469475721#artifacts, the sel4bench-results-imx8mm_evk file and sel4bench-results-tx2 file, unpack the file out, I find xxxx_SMP_64.json Secondly, the test is the smp benchmark form sel4bench-manifest project, the source file is sel4bench/apps/smp/src/main.c The test scenario look like below: A pair thread of ping-pong on the same core, the ping thread will wait for "ipc_normal_delay" time then send 0 len ipc message to pong thread, then return. I think the 500 cycles mean how long ipc_normal_delay will really delay The above scenario will test on one core, or mutil core. If we run 4 cores, every core will have a ping thread and a pong thread run like above description, then record the sum of all cores ping-pong counts. I think this experiment is used to illustrate in multi core, our seL4 kernel big lock will not affect mutli-core performance, am I right ? Addition： Our seL4_Call performance is same with other platform XXXX IMX8MM_EVK_64 TX2_64 seL4_Call 367(0) 378(2) 492(16) client->server, same vspace, ipc_len is 0 seL4_ReplyRecv 396(0) 402(2) 513(16) server->client, same vspace, ipc_len is 0 Thank you for your help -----邮件原件----- 发件人: devel-request(a)sel4.systems [mailto:devel-request@sel4.systems] 发送时间: 2021年12月2日 9:00 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 127, Issue 1 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Subscription (Xin Wang) 2. some performance problem when test 4 cores SMP benchmark of seL4bench project (yadong.li) 3. Re: some performance problem when test 4 cores SMP benchmark of seL4bench project (Gernot Heiser) ---------------------------------------------------------------------- Message: 1 Date: Wed, 1 Dec 2021 06:52:45 +0000 From: Xin Wang <xin.wang(a)bst.ai> Subject: [seL4] Subscription To: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <BL0PR18MB2146092BCA3DBADBC26984ADF7689(a)BL0PR18MB2146.nam prd18.prod.outlook.com> Content-Type: text/plain; charset="gb2312" Hi sirs, Subscription Thanks, 从 Windows 版邮件<https://go.microsoft.com/fwlink/?LinkId=550986>发送 ------------------------------ Message: 2 Date: Wed, 1 Dec 2021 14:58:17 +0000 From: yadong.li <yadong.li(a)horizon.ai> Subject: [seL4] some performance problem when test 4 cores SMP benchmark of seL4bench project To: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <2ae9929de02e481796d3d697182842c3(a)horizon.ai> Content-Type: text/plain; charset="gb2312" Hi, Now, I meet some performance problem when test 4 cores SMP benchmark of seL4bench on our platform. Out platform is XXX, But I get the test data of IMX8MM_EVK_64 and TX2 platform from seL4 website, I think they are official statistics. My test results below: ARM platform Test item XXX IMX8MM_EVK_64 TX2 mean(Stddev) 500 cycles, 1 core 636545(46) 625605(29) 598142(365) 500 cycles, 2 cores 897900(2327) 1154209(44) 994298(94) 500 cycles, 3 cores 1301679(2036) 1726043(65) 1497740(127) 500 cycles, 4 cores 1387678(549) 2172109(12674) 1545872(109) 1000 cycles, 1 core 636529(42) 625599(22) 597627(161) 1000 cycles, 2 cores 899212(3384) 1134110(34) 994437(541) 1000 cycles, 3 cores 1297322(5028) 1695385(45) 1497547(714) 1000 cycles, 4 cores 1387149(456) 2174605(81) 1545716(614) From these compare data: 1. When test smp bench on one core, the performance of several platform is similar 2. When test smp bench on muti core, the result of IMX8MM_EVK_64 is beauty, the result of 4 cores is 3.47 times as good as 1 core, I think it’s good 3. But the platform of TX2 has some different performance, the result of 2 cores is 1.66 times as good as 1 core, I still think is good, But the result of 3 cores almost have the same ping-pong count with 4 cores, why add one core, the count result not add as our expected ? 4. The performance of our platform is badly, on our platform, the result of 3 cores almost also have the same ping-pong count with 4 cores, and our count result of 4 cores just 2 times as good as one core, I think it is very bad 5. I want to know what are the possible causes of the badly performance about our platform XXX and TX2 ? ------------------------------ Message: 3 Date: Wed, 1 Dec 2021 21:09:41 +0000 From: Gernot Heiser <gernot(a)unsw.edu.au> Subject: [seL4] Re: some performance problem when test 4 cores SMP benchmark of seL4bench project To: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <720E9728-1079-4455-BB0E-34A7C5CE88F4(a)unsw.edu.au> Content-Type: text/plain; charset="utf-8" Hi Yandong, To understand what’s going on I’d need to know what these numbers are: - what is being measured, and what’s the 500/100cy parameter? - which web site are the “official” numbers from, they aren’t at https://sel4.systems/About/Performance/ Gernot On 2 Dec 2021, at 01:58, yadong.li<http://yadong.li/> <yadong.li(a)horizon.ai<mailto:yadong.li@horizon.ai>> wrote: Hi, Now, I meet some performance problem when test 4 cores SMP benchmark of seL4bench on our platform. Out platform is XXX, But I get the test data of IMX8MM_EVK_64 and TX2 platform from seL4 website, I think they are official statistics. My test results below: ARM platform Test item XXX IMX8MM_EVK_64 TX2 mean(Stddev) 500 cycles, 1 core 636545(46) 625605(29) 598142(365) 500 cycles, 2 cores 897900(2327) 1154209(44) 994298(94) 500 cycles, 3 cores 1301679(2036) 1726043(65) 1497740(127) 500 cycles, 4 cores 1387678(549) 2172109(12674) 1545872(109) 1000 cycles, 1 core 636529(42) 625599(22) 597627(161) 1000 cycles, 2 cores 899212(3384) 1134110(34) 994437(541) 1000 cycles, 3 cores 1297322(5028) 1695385(45) 1497547(714) 1000 cycles, 4 cores 1387149(456) 2174605(81) 1545716(614) From these compare data: 1. When test smp bench on one core, the performance of several platform is similar 2. When test smp bench on muti core, the result of IMX8MM_EVK_64 is beauty, the result of 4 cores is 3.47 times as good as 1 core, I think it’s good 3. But the platform of TX2 has some different performance, the result of 2 cores is 1.66 times as good as 1 core, I still think is good, But the result of 3 cores almost have the same ping-pong count with 4 cores, why add one core, the count result not add as our expected ? 4. The performance of our platform is badly, on our platform, the result of 3 cores almost also have the same ping-pong count with 4 cores, and our count result of 4 cores just 2 times as good as one core, I think it is very bad 5. I want to know what are the possible causes of the badly performance about our platform XXX and TX2 ? _______________________________________________ Devel mailing list -- devel(a)sel4.systems<mailto:devel@sel4.systems> To unsubscribe send an email to devel-leave(a)sel4.systems<mailto:devel-leave@sel4.systems> ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems ------------------------------ End of Devel Digest, Vol 127, Issue 1 *************************************

3 3

some performance problem when test 4 cores SMP benchmark of seL4bench project
by yadong.li 02 Dec '21

02 Dec '21

Hi, Now, I meet some performance problem when test 4 cores SMP benchmark of seL4bench on our platform. Out platform is XXX, But I get the test data of IMX8MM_EVK_64 and TX2 platform from seL4 website, I think they are official statistics. My test results below: ARM platform Test item XXX IMX8MM_EVK_64 TX2 mean(Stddev) 500 cycles, 1 core 636545(46) 625605(29) 598142(365) 500 cycles, 2 cores 897900(2327) 1154209(44) 994298(94) 500 cycles, 3 cores 1301679(2036) 1726043(65) 1497740(127) 500 cycles, 4 cores 1387678(549) 2172109(12674) 1545872(109) 1000 cycles, 1 core 636529(42) 625599(22) 597627(161) 1000 cycles, 2 cores 899212(3384) 1134110(34) 994437(541) 1000 cycles, 3 cores 1297322(5028) 1695385(45) 1497547(714) 1000 cycles, 4 cores 1387149(456) 2174605(81) 1545716(614) From these compare data: 1. When test smp bench on one core, the performance of several platform is similar 2. When test smp bench on muti core, the result of IMX8MM_EVK_64 is beauty, the result of 4 cores is 3.47 times as good as 1 core, I think it’s good 3. But the platform of TX2 has some different performance, the result of 2 cores is 1.66 times as good as 1 core, I still think is good, But the result of 3 cores almost have the same ping-pong count with 4 cores, why add one core, the count result not add as our expected ? 4. The performance of our platform is badly, on our platform, the result of 3 cores almost also have the same ping-pong count with 4 cores, and our count result of 4 cores just 2 times as good as one core, I think it is very bad 5. I want to know what are the possible causes of the badly performance about our platform XXX and TX2 ?

2 1

Subscription
by Xin Wang 01 Dec '21

01 Dec '21

Hi sirs, Subscription Thanks, 从 Windows 版邮件<https://go.microsoft.com/fwlink/?LinkId=550986>发送

1 0

VM Kernel Modules
by Michael Neises 20 Nov '21

20 Nov '21

Hello all, I recently spent a lot of time getting the camkes-vm-linux tutorial to work, because it is the only example I could find of compiling a kernel module for the linux vm as a part of the camkes build process. Unfortunately, the kernel module doesn't seem to work. For more information, see the previous email chain as well as https://github.com/NeisesResearch/vm_measure/wiki/Building-the-camkes_vm_li… . In lieu of doing things the right way, I believe I could compile a kernel module for the linux kernel that is provided as part of the camkes build system. I believe this is how the introspect-app accomplishes its work. However, I need to have the exact kernel and exact configuration in order to compile the kernel module correctly. Can anyone point me to the correct kernel version and configuration, so that I can target the provided linux kernel for module compilation? Or if there's a better way to get a kernel module in there, please let me know. Cheers, Michael Neises

4 5

the security whiltelist of smc call 答复: Devel Digest, Vol 124, Issue 1
by yadong.li 19 Nov '21

19 Nov '21

Hi: In our ARMv8 platform，we access secure world not only from the VM guest OS， but also form native compont like config clk register In ARMv8 platform, SMC instructions are not allowed from EL0. So in camkes-vm project, I create a new smc capability and a new syscall as a temporary solution, like below: "LIBSEL4_INLINE seL4_ARM_SMC_CallFunc_t seL4_ARM_SMC_CallFunc(seL4_ARM_SMC _service, seL4_Word function_id, seL4_Word arg0, seL4_Word arg1, seL4_Word arg2)" But I did not pay much attention to security, it is just meet our current work. I didnot really understand the essence of kernel whitelist mentioned by "https://sel4.atlassian.net/browse/RFC-9"? I have some question below, I feel the smc cap should like schedcontrol cap belong every core. 1. what is the whiltelist describe ? sip command smc function id? 2. how are the members of whilelist represented in the kernel , check the invLabel of syscall in kernel if we provide one smc cap not every function id? or just check the range of function id ? 3. Does each TCB have its own whitelist or does the entire system have a whitelist? thank you very much. -----邮件原件----- 发件人: devel-request(a)sel4.systems [mailto:devel-request@sel4.systems] 发送时间: 2021年11月10日 9:00 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 124, Issue 1 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. RFC-9: new capability for seL4 SMC Forwarding on Arm (Gerwin Klein) ---------------------------------------------------------------------- Message: 1 Date: Tue, 9 Nov 2021 21:52:58 +0000 From: Gerwin Klein <kleing(a)unsw.edu.au> Subject: [seL4] RFC-9: new capability for seL4 SMC Forwarding on Arm To: devel <devel(a)sel4.systems> Message-ID: <613858AC-3DB1-4D7C-A892-9ABDB5B31D58(a)unsw.edu.au> Content-Type: text/plain; charset="utf-8" I’d like to solicit discussion on the new RFC on forwarding Secure Monitor Calls on Arm: https://sel4.atlassian.net/browse/RFC-9 Relevant Arm documentation (SMC calling conventions): https://developer.arm.com/documentation/den0028/latest?_ga=2.116565828.3903… Any opinions, concerns, alternative designs? Cheers, Gerwin ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems ------------------------------ End of Devel Digest, Vol 124, Issue 1 *************************************

1 0

Got it, Thank you for your help. 答复: Devel Digest, Vol 125, Issue 2
by yadong.li 18 Nov '21

18 Nov '21

-----邮件原件----- 发件人: devel-request(a)sel4.systems [mailto:devel-request@sel4.systems] 发送时间: 2021年11月18日 5:56 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 125, Issue 2 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: some question about seL4 performance (Gerwin Klein) 2. Re: some question about seL4 performance (Gernot Heiser) 3. Re: some question about seL4 performance (Gerwin Klein) ---------------------------------------------------------------------- Message: 1 Date: Wed, 17 Nov 2021 21:24:57 +0000 From: Gerwin Klein <kleing(a)unsw.edu.au> Subject: [seL4] Re: some question about seL4 performance To: yadong.li <yadong.li(a)horizon.ai> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <CA210292-C334-42C1-9FB4-48CAFDE8CCC6(a)unsw.edu.au> Content-Type: text/plain; charset="utf-8" > On 18 Nov 2021, at 02:06, yadong.li <yadong.li(a)horizon.ai> wrote: > > Hi： > I learn the sel4 performance form > https://sel4.systems/About/Performance/ > I focus on the ARMv8 platform, from the website, the parameters are as follows: > ISA Mode Core/SoC/Board Clock IRQ Invoke IPC call IPC reply > "Armv8a 64 A57/Tx1/Jetson 1.9 GHz 863 (18) 396(15) 397(4)" > > I want to know what is the length of IPC for the record provided on the web page , when test IPC call and reply? 0 or 10? The page reports the 0-length numbers. The idea is that IPC should fit into registers, the 10 case is the one that make it spill into memory deliberately. That number is good to know for development, but should not be the main performance characteristic. Cheers, Gerwin ------------------------------ Message: 2 Date: Wed, 17 Nov 2021 21:36:39 +0000 From: Gernot Heiser <gernot(a)unsw.edu.au> Subject: [seL4] Re: some question about seL4 performance To: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <9885F4AB-61C0-46CD-B239-595E38482673(a)unsw.edu.au> Content-Type: text/plain; charset="utf-8" On 18 Nov 2021, at 08:24, Gerwin Klein <kleing(a)unsw.edu.au> wrote: > > The page reports the 0-length numbers. The idea is that IPC should fit into registers, the 10 case is the one that make it spill into memory deliberately. That number is good to know for development, but should not be the main performance characteristic. Note that whether data is transferred solely in registers or using a memory buffer does not make a big difference on contemporary hardware. However, our present implementation reverts to the slow path as soon as the message size overflows the physical message registers, which will make the PIC much slower. This is something that could be fixed by widening the fastpath conditions without much complications. However, we haven’t yet come across an important use case where this matters, so there isn’t much motivation for investing time in it. Gernot ------------------------------ Message: 3 Date: Wed, 17 Nov 2021 21:56:06 +0000 From: Gerwin Klein <kleing(a)unsw.edu.au> Subject: [seL4] Re: some question about seL4 performance To: Gernot Heiser <gernot(a)unsw.edu.au> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <FFD95815-9F62-4A90-A3D0-59671152494D(a)unsw.edu.au> Content-Type: text/plain; charset="us-ascii" On 18 Nov 2021, at 08:36, Gernot Heiser <gernot(a)unsw.edu.au<mailto:gernot@unsw.edu.au>> wrote: On 18 Nov 2021, at 08:24, Gerwin Klein <kleing(a)unsw.edu.au<mailto:kleing@unsw.edu.au>> wrote: The page reports the 0-length numbers. The idea is that IPC should fit into registers, the 10 case is the one that make it spill into memory deliberately. That number is good to know for development, but should not be the main performance characteristic. Note that whether data is transferred solely in registers or using a memory buffer does not make a big difference on contemporary hardware. However, our present implementation reverts to the slow path as soon as the message size overflows the physical message registers, which will make the PIC much slower. Yes I should have mentioned that. If you look at the raw numbers for x86, eg. at https://github.com/seL4/sel4bench/actions/runs/1469475721#artifacts, fast path/no fast path is almost equal for length 10. You get a tiny bit better performance for length 10 when the fast path is switched off completely, because it doesn't first have to test whether to take the fast path or not. Cheers, Gerwin ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems ------------------------------ End of Devel Digest, Vol 125, Issue 2 *************************************

1 0

some question about seL4 performance
by yadong.li 18 Nov '21

18 Nov '21

Hi： I learn the sel4 performance form https://sel4.systems/About/Performance/ I focus on the ARMv8 platform, from the website, the parameters are as follows: ISA Mode Core/SoC/Board Clock IRQ Invoke IPC call IPC reply "Armv8a 64 A57/Tx1/Jetson 1.9 GHz 863 (18) 396(15) 397(4)" I want to know what is the length of IPC for the record provided on the web page , when test IPC call and reply? 0 or 10? thank you very much

3 3

Crash problem, CAmkES-VM app with Ethernet passthrough
by hamed_ganji＠aut.ac.ir 18 Nov '21

18 Nov '21

Hello everyone, I attempt to make a simple CAmkES-VM app to load a Linux VM with Ethernet passthrough. After running, Linux kernel crashes while initializing the device (e1000). Can anyone guide me how to fix the problem, please. Thanks in advance. The used qemu command: ------------------------------------------------------------ $ qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,+xsave,+xsaveopt,+xsavec,+fsgsbase,+pcid,+invpcid,enforce,+vmx -nographic -serial mon:stdio -m size=4G -enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 ------------------------------------------------------------ Here is my CAmkES app definition: ------------------------------------------------------------ import <VM/vm.camkes>; #include <configurations/vm.h> #define VM_GUEST_CMDLINE "earlyprintk=ttyS0,115200 console=ttyS0,115200 i8042.nokbd=y i8042.nomux=y \ i8042.noaux=y io_delay=udelay noisapnp pci=nomsi debug root=/dev/mem" // nosmap acpi=off" component Init0 { VM_INIT_DEF() } assembly { composition { VM_COMPOSITION_DEF() VM_PER_VM_COMP_DEF(0) } configuration { VM_CONFIGURATION_DEF() VM_PER_VM_CONFIG_DEF(0) vm0.simple_untyped25_pool = 75; vm0.cnode_size_bits = 24; vm0.heap_size = 0x2000000; vm0.guest_ram_mb = 2048; vm0.kernel_cmdline = VM_GUEST_CMDLINE; vm0.kernel_image = "bzimage"; vm0.kernel_relocs = "bzimage"; vm0.initrd_image = "rootfs.cpio"; vm0.iospace_domain = 0x0f; vm0.pci_devices_iospace = 1; vm0.vm_ioports = [ {"start":0xc000, "end":0xc040, "pci_device":2, "name":"eth"}, ]; vm0.pci_devices = [ { "name":"eth", "bus":0, "dev":2, "fun":0, "irq":"eth_irq", "memory":[ {"paddr":0xfeb00000, "size":0x80000, "page_bits":12}, {"paddr":0xfeb80000, "size":0x20000, "page_bits":12} ] }, ]; vm0.vm_irqs = [ {"name":"eth_irq", "source":1, "level_trig":1, "active_low":1, "dest":11}, ]; } } ------------------------------------------------------------ The output lines: ------------------------------------------------------------ Booting from ROM..Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0xa1f000 end=0x1edbe18 size=0x14bce18 name='images/capdl-loader-image-x86_64-pc99' Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 7fedf000 type 1 Adding physical memory region 0x100000-0x7ffdf000 Physical Memory Region from 7ffdf000 size 21000 type 2 Physical Memory Region from b0000000 size 10000000 type 2 Physical Memory Region from fed1c000 size 4000 type 2 Physical Memory Region from feffc000 size 4000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 Physical Memory Region from 100000000 size 80000000 type 1 Adding physical memory region 0x100000000-0x180000000 Multiboot gave us no video information ACPI: RSDP paddr=0xf5ac0 ACPI: RSDP vaddr=0xf5ac0 ACPI: RSDT paddr=0x7ffe2140 ACPI: RSDT vaddr=0x7ffe2140 Kernel loaded to: start=0x100000 end=0xa1e000 size=0x91e000 entry=0x1012db ACPI: RSDT paddr=0x7ffe2140 ACPI: RSDT vaddr=0x7ffe2140 ACPI: FADT paddr=0x7ffe1f18 ACPI: FADT vaddr=0x7ffe1f18 ACPI: FADT flags=0x84a5 ACPI: DMAR paddr=0x7ffe20f8 ACPI: DMAR vaddr=0x7ffe20f8 ACPI: IOMMU host address width: 39 ACPI: 1 IOMMUs detected ACPI: MADT paddr=0x7ffe200c ACPI: MADT vaddr=0x7ffe200c ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd ACPI: 1 CPU(s) detected ELF-loading userland images from boot modules: size=0x294b000 v_entry=0x408619 v_start=0x400000 v_end=0x2d4b000 p_start=0x1edc000 p_end=0x4827000 Moving loaded userland images to final location: from=0x1edc000 to=0xa1e000 size=0x294b000 Starting node #0 with APIC ID 0 Mapping kernel window is done IOMMU 0x0: 16-bit domain IDs supported IOMMU: Using 3 page-table levels (max. supported: 3) IOMMU: Create VTD context table for PCI bus 0x0 (pptr=0xffffff817e01d000) IOMMU: Create VTD context table for PCI bus 0x1 (pptr=0xffffff817e01e000) IOMMU: Create VTD context table for PCI bus 0x2 (pptr=0xffffff817e01f000) IOMMU: Create VTD context table for PCI bus 0x3 (pptr=0xffffff817e020000) IOMMU: Create VTD context table for PCI bus 0x4 (pptr=0xffffff817e021000) IOMMU: Create VTD context table for PCI bus 0x5 (pptr=0xffffff817e022000) IOMMU: Create VTD context table for PCI bus 0x6 (pptr=0xffffff817e023000) IOMMU: Create VTD context table for PCI bus 0x7 (pptr=0xffffff817e024000) IOMMU: Create VTD context table for PCI bus 0x8 (pptr=0xffffff817e025000) IOMMU: Create VTD context table for PCI bus 0x9 (pptr=0xffffff817e026000) IOMMU: Create VTD context table for PCI bus 0xa (pptr=0xffffff817e027000) IOMMU: Create VTD context table for PCI bus 0xb (pptr=0xffffff817e028000) IOMMU: Create VTD context table for PCI bus 0xc (pptr=0xffffff817e029000) IOMMU: Create VTD context table for PCI bus 0xd (pptr=0xffffff817e02a000) IOMMU: Create VTD context table for PCI bus 0xe (pptr=0xffffff817e02b000) IOMMU: Create VTD context table for PCI bus 0xf (pptr=0xffffff817e02c000) IOMMU: Create VTD context table for PCI bus 0x10 (pptr=0xffffff817e02d000) IOMMU: Create VTD context table for PCI bus 0x11 (pptr=0xffffff817e02e000) IOMMU: Create VTD context table for PCI bus 0x12 (pptr=0xffffff817e02f000) IOMMU: Create VTD context table for PCI bus 0x13 (pptr=0xffffff817e030000) IOMMU: Create VTD context table for PCI bus 0x14 (pptr=0xffffff817e031000) IOMMU: Create VTD context table for PCI bus 0x15 (pptr=0xffffff817e032000) IOMMU: Create VTD context table for PCI bus 0x16 (pptr=0xffffff817e033000) IOMMU: Create VTD context table for PCI bus 0x17 (pptr=0xffffff817e034000) IOMMU: Create VTD context table for PCI bus 0x18 (pptr=0xffffff817e035000) IOMMU: Create VTD context table for PCI bus 0x19 (pptr=0xffffff817e036000) IOMMU: Create VTD context table for PCI bus 0x1a (pptr=0xffffff817e037000) IOMMU: Create VTD context table for PCI bus 0x1b (pptr=0xffffff817e038000) IOMMU: Create VTD context table for PCI bus 0x1c (pptr=0xffffff817e039000) IOMMU: Create VTD context table for PCI bus 0x1d (pptr=0xffffff817e03a000) IOMMU: Create VTD context table for PCI bus 0x1e (pptr=0xffffff817e03b000) IOMMU: Create VTD context table for PCI bus 0x1f (pptr=0xffffff817e03c000) IOMMU: Create VTD context table for PCI bus 0x20 (pptr=0xffffff817e03d000) IOMMU: Create VTD context table for PCI bus 0x21 (pptr=0xffffff817e03e000) IOMMU: Create VTD context table for PCI bus 0x22 (pptr=0xffffff817e03f000) IOMMU: Create VTD context table for PCI bus 0x23 (pptr=0xffffff817e040000) IOMMU: Create VTD context table for PCI bus 0x24 (pptr=0xffffff817e041000) IOMMU: Create VTD context table for PCI bus 0x25 (pptr=0xffffff817e042000) IOMMU: Create VTD context table for PCI bus 0x26 (pptr=0xffffff817e043000) IOMMU: Create VTD context table for PCI bus 0x27 (pptr=0xffffff817e044000) IOMMU: Create VTD context table for PCI bus 0x28 (pptr=0xffffff817e045000) IOMMU: Create VTD context table for PCI bus 0x29 (pptr=0xffffff817e046000) IOMMU: Create VTD context table for PCI bus 0x2a (pptr=0xffffff817e047000) IOMMU: Create VTD context table for PCI bus 0x2b (pptr=0xffffff817e048000) IOMMU: Create VTD context table for PCI bus 0x2c (pptr=0xffffff817e049000) IOMMU: Create VTD context table for PCI bus 0x2d (pptr=0xffffff817e04a000) IOMMU: Create VTD context table for PCI bus 0x2e (pptr=0xffffff817e04b000) IOMMU: Create VTD context table for PCI bus 0x2f (pptr=0xffffff817e04c000) IOMMU: Create VTD context table for PCI bus 0x30 (pptr=0xffffff817e04d000) IOMMU: Create VTD context table for PCI bus 0x31 (pptr=0xffffff817e04e000) IOMMU: Create VTD context table for PCI bus 0x32 (pptr=0xffffff817e04f000) IOMMU: Create VTD context table for PCI bus 0x33 (pptr=0xffffff817e050000) IOMMU: Create VTD context table for PCI bus 0x34 (pptr=0xffffff817e051000) IOMMU: Create VTD context table for PCI bus 0x35 (pptr=0xffffff817e052000) IOMMU: Create VTD context table for PCI bus 0x36 (pptr=0xffffff817e053000) IOMMU: Create VTD context table for PCI bus 0x37 (pptr=0xffffff817e054000) IOMMU: Create VTD context table for PCI bus 0x38 (pptr=0xffffff817e055000) IOMMU: Create VTD context table for PCI bus 0x39 (pptr=0xffffff817e056000) IOMMU: Create VTD context table for PCI bus 0x3a (pptr=0xffffff817e057000) IOMMU: Create VTD context table for PCI bus 0x3b (pptr=0xffffff817e058000) IOMMU: Create VTD context table for PCI bus 0x3c (pptr=0xffffff817e059000) IOMMU: Create VTD context table for PCI bus 0x3d (pptr=0xffffff817e05a000) IOMMU: Create VTD context table for PCI bus 0x3e (pptr=0xffffff817e05b000) IOMMU: Create VTD context table for PCI bus 0x3f (pptr=0xffffff817e05c000) IOMMU: Create VTD context table for PCI bus 0x40 (pptr=0xffffff817e05d000) IOMMU: Create VTD context table for PCI bus 0x41 (pptr=0xffffff817e05e000) IOMMU: Create VTD context table for PCI bus 0x42 (pptr=0xffffff817e05f000) IOMMU: Create VTD context table for PCI bus 0x43 (pptr=0xffffff817e060000) IOMMU: Create VTD context table for PCI bus 0x44 (pptr=0xffffff817e061000) IOMMU: Create VTD context table for PCI bus 0x45 (pptr=0xffffff817e062000) IOMMU: Create VTD context table for PCI bus 0x46 (pptr=0xffffff817e063000) IOMMU: Create VTD context table for PCI bus 0x47 (pptr=0xffffff817e064000) IOMMU: Create VTD context table for PCI bus 0x48 (pptr=0xffffff817e065000) IOMMU: Create VTD context table for PCI bus 0x49 (pptr=0xffffff817e066000) IOMMU: Create VTD context table for PCI bus 0x4a (pptr=0xffffff817e067000) IOMMU: Create VTD context table for PCI bus 0x4b (pptr=0xffffff817e068000) IOMMU: Create VTD context table for PCI bus 0x4c (pptr=0xffffff817e069000) IOMMU: Create VTD context table for PCI bus 0x4d (pptr=0xffffff817e06a000) IOMMU: Create VTD context table for PCI bus 0x4e (pptr=0xffffff817e06b000) IOMMU: Create VTD context table for PCI bus 0x4f (pptr=0xffffff817e06c000) IOMMU: Create VTD context table for PCI bus 0x50 (pptr=0xffffff817e06d000) IOMMU: Create VTD context table for PCI bus 0x51 (pptr=0xffffff817e06e000) IOMMU: Create VTD context table for PCI bus 0x52 (pptr=0xffffff817e06f000) IOMMU: Create VTD context table for PCI bus 0x53 (pptr=0xffffff817e070000) IOMMU: Create VTD context table for PCI bus 0x54 (pptr=0xffffff817e071000) IOMMU: Create VTD context table for PCI bus 0x55 (pptr=0xffffff817e072000) IOMMU: Create VTD context table for PCI bus 0x56 (pptr=0xffffff817e073000) IOMMU: Create VTD context table for PCI bus 0x57 (pptr=0xffffff817e074000) IOMMU: Create VTD context table for PCI bus 0x58 (pptr=0xffffff817e075000) IOMMU: Create VTD context table for PCI bus 0x59 (pptr=0xffffff817e076000) IOMMU: Create VTD context table for PCI bus 0x5a (pptr=0xffffff817e077000) IOMMU: Create VTD context table for PCI bus 0x5b (pptr=0xffffff817e078000) IOMMU: Create VTD context table for PCI bus 0x5c (pptr=0xffffff817e079000) IOMMU: Create VTD context table for PCI bus 0x5d (pptr=0xffffff817e07a000) IOMMU: Create VTD context table for PCI bus 0x5e (pptr=0xffffff817e07b000) IOMMU: Create VTD context table for PCI bus 0x5f (pptr=0xffffff817e07c000) IOMMU: Create VTD context table for PCI bus 0x60 (pptr=0xffffff817e07d000) IOMMU: Create VTD context table for PCI bus 0x61 (pptr=0xffffff817e07e000) IOMMU: Create VTD context table for PCI bus 0x62 (pptr=0xffffff817e07f000) IOMMU: Create VTD context table for PCI bus 0x63 (pptr=0xffffff817e080000) IOMMU: Create VTD context table for PCI bus 0x64 (pptr=0xffffff817e081000) IOMMU: Create VTD context table for PCI bus 0x65 (pptr=0xffffff817e082000) IOMMU: Create VTD context table for PCI bus 0x66 (pptr=0xffffff817e083000) IOMMU: Create VTD context table for PCI bus 0x67 (pptr=0xffffff817e084000) IOMMU: Create VTD context table for PCI bus 0x68 (pptr=0xffffff817e085000) IOMMU: Create VTD context table for PCI bus 0x69 (pptr=0xffffff817e086000) IOMMU: Create VTD context table for PCI bus 0x6a (pptr=0xffffff817e087000) IOMMU: Create VTD context table for PCI bus 0x6b (pptr=0xffffff817e088000) IOMMU: Create VTD context table for PCI bus 0x6c (pptr=0xffffff817e089000) IOMMU: Create VTD context table for PCI bus 0x6d (pptr=0xffffff817e08a000) IOMMU: Create VTD context table for PCI bus 0x6e (pptr=0xffffff817e08b000) IOMMU: Create VTD context table for PCI bus 0x6f (pptr=0xffffff817e08c000) IOMMU: Create VTD context table for PCI bus 0x70 (pptr=0xffffff817e08d000) IOMMU: Create VTD context table for PCI bus 0x71 (pptr=0xffffff817e08e000) IOMMU: Create VTD context table for PCI bus 0x72 (pptr=0xffffff817e08f000) IOMMU: Create VTD context table for PCI bus 0x73 (pptr=0xffffff817e090000) IOMMU: Create VTD context table for PCI bus 0x74 (pptr=0xffffff817e091000) IOMMU: Create VTD context table for PCI bus 0x75 (pptr=0xffffff817e092000) IOMMU: Create VTD context table for PCI bus 0x76 (pptr=0xffffff817e093000) IOMMU: Create VTD context table for PCI bus 0x77 (pptr=0xffffff817e094000) IOMMU: Create VTD context table for PCI bus 0x78 (pptr=0xffffff817e095000) IOMMU: Create VTD context table for PCI bus 0x79 (pptr=0xffffff817e096000) IOMMU: Create VTD context table for PCI bus 0x7a (pptr=0xffffff817e097000) IOMMU: Create VTD context table for PCI bus 0x7b (pptr=0xffffff817e098000) IOMMU: Create VTD context table for PCI bus 0x7c (pptr=0xffffff817e099000) IOMMU: Create VTD context table for PCI bus 0x7d (pptr=0xffffff817e09a000) IOMMU: Create VTD context table for PCI bus 0x7e (pptr=0xffffff817e09b000) IOMMU: Create VTD context table for PCI bus 0x7f (pptr=0xffffff817e09c000) IOMMU: Create VTD context table for PCI bus 0x80 (pptr=0xffffff817e09d000) IOMMU: Create VTD context table for PCI bus 0x81 (pptr=0xffffff817e09e000) IOMMU: Create VTD context table for PCI bus 0x82 (pptr=0xffffff817e09f000) IOMMU: Create VTD context table for PCI bus 0x83 (pptr=0xffffff817e0a0000) IOMMU: Create VTD context table for PCI bus 0x84 (pptr=0xffffff817e0a1000) IOMMU: Create VTD context table for PCI bus 0x85 (pptr=0xffffff817e0a2000) IOMMU: Create VTD context table for PCI bus 0x86 (pptr=0xffffff817e0a3000) IOMMU: Create VTD context table for PCI bus 0x87 (pptr=0xffffff817e0a4000) IOMMU: Create VTD context table for PCI bus 0x88 (pptr=0xffffff817e0a5000) IOMMU: Create VTD context table for PCI bus 0x89 (pptr=0xffffff817e0a6000) IOMMU: Create VTD context table for PCI bus 0x8a (pptr=0xffffff817e0a7000) IOMMU: Create VTD context table for PCI bus 0x8b (pptr=0xffffff817e0a8000) IOMMU: Create VTD context table for PCI bus 0x8c (pptr=0xffffff817e0a9000) IOMMU: Create VTD context table for PCI bus 0x8d (pptr=0xffffff817e0aa000) IOMMU: Create VTD context table for PCI bus 0x8e (pptr=0xffffff817e0ab000) IOMMU: Create VTD context table for PCI bus 0x8f (pptr=0xffffff817e0ac000) IOMMU: Create VTD context table for PCI bus 0x90 (pptr=0xffffff817e0ad000) IOMMU: Create VTD context table for PCI bus 0x91 (pptr=0xffffff817e0ae000) IOMMU: Create VTD context table for PCI bus 0x92 (pptr=0xffffff817e0af000) IOMMU: Create VTD context table for PCI bus 0x93 (pptr=0xffffff817e0b0000) IOMMU: Create VTD context table for PCI bus 0x94 (pptr=0xffffff817e0b1000) IOMMU: Create VTD context table for PCI bus 0x95 (pptr=0xffffff817e0b2000) IOMMU: Create VTD context table for PCI bus 0x96 (pptr=0xffffff817e0b3000) IOMMU: Create VTD context table for PCI bus 0x97 (pptr=0xffffff817e0b4000) IOMMU: Create VTD context table for PCI bus 0x98 (pptr=0xffffff817e0b5000) IOMMU: Create VTD context table for PCI bus 0x99 (pptr=0xffffff817e0b6000) IOMMU: Create VTD context table for PCI bus 0x9a (pptr=0xffffff817e0b7000) IOMMU: Create VTD context table for PCI bus 0x9b (pptr=0xffffff817e0b8000) IOMMU: Create VTD context table for PCI bus 0x9c (pptr=0xffffff817e0b9000) IOMMU: Create VTD context table for PCI bus 0x9d (pptr=0xffffff817e0ba000) IOMMU: Create VTD context table for PCI bus 0x9e (pptr=0xffffff817e0bb000) IOMMU: Create VTD context table for PCI bus 0x9f (pptr=0xffffff817e0bc000) IOMMU: Create VTD context table for PCI bus 0xa0 (pptr=0xffffff817e0bd000) IOMMU: Create VTD context table for PCI bus 0xa1 (pptr=0xffffff817e0be000) IOMMU: Create VTD context table for PCI bus 0xa2 (pptr=0xffffff817e0bf000) IOMMU: Create VTD context table for PCI bus 0xa3 (pptr=0xffffff817e0c0000) IOMMU: Create VTD context table for PCI bus 0xa4 (pptr=0xffffff817e0c1000) IOMMU: Create VTD context table for PCI bus 0xa5 (pptr=0xffffff817e0c2000) IOMMU: Create VTD context table for PCI bus 0xa6 (pptr=0xffffff817e0c3000) IOMMU: Create VTD context table for PCI bus 0xa7 (pptr=0xffffff817e0c4000) IOMMU: Create VTD context table for PCI bus 0xa8 (pptr=0xffffff817e0c5000) IOMMU: Create VTD context table for PCI bus 0xa9 (pptr=0xffffff817e0c6000) IOMMU: Create VTD context table for PCI bus 0xaa (pptr=0xffffff817e0c7000) IOMMU: Create VTD context table for PCI bus 0xab (pptr=0xffffff817e0c8000) IOMMU: Create VTD context table for PCI bus 0xac (pptr=0xffffff817e0c9000) IOMMU: Create VTD context table for PCI bus 0xad (pptr=0xffffff817e0ca000) IOMMU: Create VTD context table for PCI bus 0xae (pptr=0xffffff817e0cb000) IOMMU: Create VTD context table for PCI bus 0xaf (pptr=0xffffff817e0cc000) IOMMU: Create VTD context table for PCI bus 0xb0 (pptr=0xffffff817e0cd000) IOMMU: Create VTD context table for PCI bus 0xb1 (pptr=0xffffff817e0ce000) IOMMU: Create VTD context table for PCI bus 0xb2 (pptr=0xffffff817e0cf000) IOMMU: Create VTD context table for PCI bus 0xb3 (pptr=0xffffff817e0d0000) IOMMU: Create VTD context table for PCI bus 0xb4 (pptr=0xffffff817e0d1000) IOMMU: Create VTD context table for PCI bus 0xb5 (pptr=0xffffff817e0d2000) IOMMU: Create VTD context table for PCI bus 0xb6 (pptr=0xffffff817e0d3000) IOMMU: Create VTD context table for PCI bus 0xb7 (pptr=0xffffff817e0d4000) IOMMU: Create VTD context table for PCI bus 0xb8 (pptr=0xffffff817e0d5000) IOMMU: Create VTD context table for PCI bus 0xb9 (pptr=0xffffff817e0d6000) IOMMU: Create VTD context table for PCI bus 0xba (pptr=0xffffff817e0d7000) IOMMU: Create VTD context table for PCI bus 0xbb (pptr=0xffffff817e0d8000) IOMMU: Create VTD context table for PCI bus 0xbc (pptr=0xffffff817e0d9000) IOMMU: Create VTD context table for PCI bus 0xbd (pptr=0xffffff817e0da000) IOMMU: Create VTD context table for PCI bus 0xbe (pptr=0xffffff817e0db000) IOMMU: Create VTD context table for PCI bus 0xbf (pptr=0xffffff817e0dc000) IOMMU: Create VTD context table for PCI bus 0xc0 (pptr=0xffffff817e0dd000) IOMMU: Create VTD context table for PCI bus 0xc1 (pptr=0xffffff817e0de000) IOMMU: Create VTD context table for PCI bus 0xc2 (pptr=0xffffff817e0df000) IOMMU: Create VTD context table for PCI bus 0xc3 (pptr=0xffffff817e0e0000) IOMMU: Create VTD context table for PCI bus 0xc4 (pptr=0xffffff817e0e1000) IOMMU: Create VTD context table for PCI bus 0xc5 (pptr=0xffffff817e0e2000) IOMMU: Create VTD context table for PCI bus 0xc6 (pptr=0xffffff817e0e3000) IOMMU: Create VTD context table for PCI bus 0xc7 (pptr=0xffffff817e0e4000) IOMMU: Create VTD context table for PCI bus 0xc8 (pptr=0xffffff817e0e5000) IOMMU: Create VTD context table for PCI bus 0xc9 (pptr=0xffffff817e0e6000) IOMMU: Create VTD context table for PCI bus 0xca (pptr=0xffffff817e0e7000) IOMMU: Create VTD context table for PCI bus 0xcb (pptr=0xffffff817e0e8000) IOMMU: Create VTD context table for PCI bus 0xcc (pptr=0xffffff817e0e9000) IOMMU: Create VTD context table for PCI bus 0xcd (pptr=0xffffff817e0ea000) IOMMU: Create VTD context table for PCI bus 0xce (pptr=0xffffff817e0eb000) IOMMU: Create VTD context table for PCI bus 0xcf (pptr=0xffffff817e0ec000) IOMMU: Create VTD context table for PCI bus 0xd0 (pptr=0xffffff817e0ed000) IOMMU: Create VTD context table for PCI bus 0xd1 (pptr=0xffffff817e0ee000) IOMMU: Create VTD context table for PCI bus 0xd2 (pptr=0xffffff817e0ef000) IOMMU: Create VTD context table for PCI bus 0xd3 (pptr=0xffffff817e0f0000) IOMMU: Create VTD context table for PCI bus 0xd4 (pptr=0xffffff817e0f1000) IOMMU: Create VTD context table for PCI bus 0xd5 (pptr=0xffffff817e0f2000) IOMMU: Create VTD context table for PCI bus 0xd6 (pptr=0xffffff817e0f3000) IOMMU: Create VTD context table for PCI bus 0xd7 (pptr=0xffffff817e0f4000) IOMMU: Create VTD context table for PCI bus 0xd8 (pptr=0xffffff817e0f5000) IOMMU: Create VTD context table for PCI bus 0xd9 (pptr=0xffffff817e0f6000) IOMMU: Create VTD context table for PCI bus 0xda (pptr=0xffffff817e0f7000) IOMMU: Create VTD context table for PCI bus 0xdb (pptr=0xffffff817e0f8000) IOMMU: Create VTD context table for PCI bus 0xdc (pptr=0xffffff817e0f9000) IOMMU: Create VTD context table for PCI bus 0xdd (pptr=0xffffff817e0fa000) IOMMU: Create VTD context table for PCI bus 0xde (pptr=0xffffff817e0fb000) IOMMU: Create VTD context table for PCI bus 0xdf (pptr=0xffffff817e0fc000) IOMMU: Create VTD context table for PCI bus 0xe0 (pptr=0xffffff817e0fd000) IOMMU: Create VTD context table for PCI bus 0xe1 (pptr=0xffffff817e0fe000) IOMMU: Create VTD context table for PCI bus 0xe2 (pptr=0xffffff817e0ff000) IOMMU: Create VTD context table for PCI bus 0xe3 (pptr=0xffffff817e100000) IOMMU: Create VTD context table for PCI bus 0xe4 (pptr=0xffffff817e101000) IOMMU: Create VTD context table for PCI bus 0xe5 (pptr=0xffffff817e102000) IOMMU: Create VTD context table for PCI bus 0xe6 (pptr=0xffffff817e103000) IOMMU: Create VTD context table for PCI bus 0xe7 (pptr=0xffffff817e104000) IOMMU: Create VTD context table for PCI bus 0xe8 (pptr=0xffffff817e105000) IOMMU: Create VTD context table for PCI bus 0xe9 (pptr=0xffffff817e106000) IOMMU: Create VTD context table for PCI bus 0xea (pptr=0xffffff817e107000) IOMMU: Create VTD context table for PCI bus 0xeb (pptr=0xffffff817e108000) IOMMU: Create VTD context table for PCI bus 0xec (pptr=0xffffff817e109000) IOMMU: Create VTD context table for PCI bus 0xed (pptr=0xffffff817e10a000) IOMMU: Create VTD context table for PCI bus 0xee (pptr=0xffffff817e10b000) IOMMU: Create VTD context table for PCI bus 0xef (pptr=0xffffff817e10c000) IOMMU: Create VTD context table for PCI bus 0xf0 (pptr=0xffffff817e10d000) IOMMU: Create VTD context table for PCI bus 0xf1 (pptr=0xffffff817e10e000) IOMMU: Create VTD context table for PCI bus 0xf2 (pptr=0xffffff817e10f000) IOMMU: Create VTD context table for PCI bus 0xf3 (pptr=0xffffff817e110000) IOMMU: Create VTD context table for PCI bus 0xf4 (pptr=0xffffff817e111000) IOMMU: Create VTD context table for PCI bus 0xf5 (pptr=0xffffff817e112000) IOMMU: Create VTD context table for PCI bus 0xf6 (pptr=0xffffff817e113000) IOMMU: Create VTD context table for PCI bus 0xf7 (pptr=0xffffff817e114000) IOMMU: Create VTD context table for PCI bus 0xf8 (pptr=0xffffff817e115000) IOMMU: Create VTD context table for PCI bus 0xf9 (pptr=0xffffff817e116000) IOMMU: Create VTD context table for PCI bus 0xfa (pptr=0xffffff817e117000) IOMMU: Create VTD context table for PCI bus 0xfb (pptr=0xffffff817e118000) IOMMU: Create VTD context table for PCI bus 0xfc (pptr=0xffffff817e119000) IOMMU: Create VTD context table for PCI bus 0xfd (pptr=0xffffff817e11a000) IOMMU: Create VTD context table for PCI bus 0xfe (pptr=0xffffff817e11b000) IOMMU: Create VTD context table for PCI bus 0xff (pptr=0xffffff817e11c000) IOMMU 0x0: enabling... enabled Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/212 T0xffffff817e11d400 "rootserver" @4014bf]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/212 T0xffffff817e11d400 "rootserver" @4014bf]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/212 T0xffffff817e11d400 "rootserver" @4014bf]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/212 T0xffffff817e11d400 "rootserver" @4014bf]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/212 T0xffffff817e11d400 "rootserver" @4014bf]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>> Single bus detected lib_pci_scan_dev found pci device 0 0 PCI :: 00.00.00 : intel Unknown device ID. (vid 0x8086 did 0x29c0) line0 pin0 lib_pci_scan_dev found pci device 0 1 PCI :: 00.01.00 : Unknown vendor ID. Unknown device ID. (vid 0x1234 did 0x1111) line0 pin0 BAR0 : [ mem 0xfd000000 sz 0x1000000 szmask 0xff000000 prefetch ] BAR2 : [ mem 0xfebb0000 sz 0x1000 szmask 0xfffff000 ] lib_pci_scan_dev found pci device 0 2 PCI :: 00.02.00 : intel Unknown device ID. (vid 0x8086 did 0x100e) line11 pin1 BAR0 : [ mem 0xfeb80000 sz 0x20000 szmask 0xfffe0000 ] BAR1 : [ io 0xc000 sz 0x40 szmask 0xffffffc0 ] lib_pci_scan_dev found pci device 0 31 PCI :: 00.1f.00 : intel intel_ich9_8 (vid 0x8086 did 0x2918) line0 pin0 lib_pci_scan_dev found multi function device 0 31 PCI :: 00.1f.02 : intel Unknown device ID. (vid 0x8086 did 0x2922) line10 pin1 BAR4 : [ io 0xc080 sz 0x20 szmask 0xffffffe0 ] BAR5 : [ mem 0xfebb1000 sz 0x1000 szmask 0xfffff000 ] PCI :: 00.1f.03 : intel intel_ich9_6 (vid 0x8086 did 0x2930) line10 pin1 BAR4 : [ io 0x700 sz 0x40 szmask 0xffffffc0 ] Guest page dir allocated at 0x10000000. Creating 1-1 entries sel4utils_reserve_range_at_no_alloc@vspace.c:601 Range not available at 0x7e00, size 0x78200 vm_reserve_memory_at@guest_memory.c:328 Failed to allocate vm reservation: Unable to create vspace reservation at address 0x7e00 of size 492032 vm_ram_register_at@guest_ram.c:355 Unable to reserve ram region at addr 0x7e00 of size 0x78200 guest_elf_relocate@guest_image.c:129 50000 relocs done. guest_elf_relocate@guest_image.c:129 100000 relocs done. Constructing guest cmdline at 0x500 of size 142 Guest boot info allocated at 0x58f. Populating... Final e820 map is: 0x0 - 0x500 type 2 0x500 - 0x7c00 type 1 0x7c00 - 0x80000 type 2 0x80000 - 0x9fc00 type 1 0x9fc00 - 0x10001000 type 2 0x10001000 - 0x90001000 type 1 Initializing guest to start running at 0x10400000 [ 0.000000] Linux version 4.8.16 (alisonf@carbon) (gcc version 7.4.0 (Ubuntu 7.4.0-1ubuntu1~18.04.1) ) #1 Wed Oct 23 17:26:59 AEDT 2019 [ 0.000000] Disabled fast string operations [ 0.000000] x86/fpu: Legacy x87 FPU detected. [ 0.000000] x86/fpu: Using 'eager' FPU context switches. [ 0.000000] e820: BIOS-provided physical RAM map: [ 0.000000] BIOS-e820: [mem 0x0000000000000000-0x00000000000004ff] reserved [ 0.000000] BIOS-e820: [mem 0x0000000000000500-0x0000000000007bff] usable [ 0.000000] BIOS-e820: [mem 0x0000000000007c00-0x000000000007ffff] reserved [ 0.000000] BIOS-e820: [mem 0x0000000000080000-0x000000000009fbff] usable [ 0.000000] BIOS-e820: [mem 0x000000000009fc00-0x0000000010000fff] reserved [ 0.000000] BIOS-e820: [mem 0x0000000010001000-0x0000000090000fff] usable [ 0.000000] bootconsole [earlyser0] enabled [ 0.000000] Notice: NX (Execute Disable) protection missing in CPU! [ 0.000000] DMI not present or invalid. [ 0.000000] e820: update [mem 0x00000000-0x00000fff] usable ==> reserved [ 0.000000] e820: remove [mem 0x000a0000-0x000fffff] usable [ 0.000000] e820: last_pfn = 0x90001 max_arch_pfn = 0x100000 [ 0.000000] MTRR: Disabled [ 0.000000] x86/PAT: MTRRs disabled, skipping PAT initialization too. [ 0.000000] x86/PAT: Configuration [0-7]: WB WT UC- UC WB WT UC- UC [ 0.000000] Warning only 895MB will be used. [ 0.000000] Use a HIGHMEM enabled kernel. [ 0.000000] Scanning 1 areas for low memory corruption [ 0.000000] initial memory mapped: [mem 0x00000000-0x10ffffff] [ 0.000000] Base memory trampoline at [c009b000] 9b000 size 16384 [ 0.000000] BRK [0x10b8f000, 0x10b8ffff] PGTABLE [ 0.000000] BRK [0x10b90000, 0x10b90fff] PGTABLE [ 0.000000] RAMDISK: [mem 0x10c71000-0x11279fff] [ 0.000000] 895MB LOWMEM available. [ 0.000000] mapped low ram: 0 - 37fe2000 [ 0.000000] low ram: 0 - 37fe2000 [ 0.000000] Zone ranges: [ 0.000000] DMA [mem 0x0000000000001000-0x0000000000ffffff] [ 0.000000] Normal [mem 0x0000000001000000-0x0000000037fe1fff] [ 0.000000] Movable zone start for each node [ 0.000000] Early memory node ranges [ 0.000000] node 0: [mem 0x0000000000001000-0x0000000000006fff] [ 0.000000] node 0: [mem 0x0000000000080000-0x000000000009efff] [ 0.000000] node 0: [mem 0x0000000010001000-0x0000000090000fff] [ 0.000000] Initmem setup node 0 [mem 0x0000000000001000-0x0000000090000fff] [ 0.000000] On node 0 totalpages: 163846 [ 0.000000] free_area_init_node: node 0, pgdat d0a7ce40, node_mem_map f7466020 [ 0.000000] DMA zone: 32 pages used for memmap [ 0.000000] DMA zone: 0 pages reserved [ 0.000000] DMA zone: 37 pages, LIFO batch:0 [ 0.000000] Normal zone: 1760 pages used for memmap [ 0.000000] Normal zone: 163809 pages, LIFO batch:31 [ 0.000000] e820: [mem 0x90001000-0xffffffff] available for PCI devices [ 0.000000] clocksource: refined-jiffies: mask: 0xffffffff max_cycles: 0xffffffff, max_idle_ns: 19112604462750000 ns [ 0.000000] pcpu-alloc: s0 r0 d32768 u32768 alloc=1*32768 [ 0.000000] pcpu-alloc: [0] 0 [ 0.000000] Built 1 zonelists in Zone order, mobility grouping on. Total pages: 162054 [ 0.000000] Kernel command line: earlyprintk=ttyS0,115200 console=ttyS0,115200 i8042.nokbd=y i8042.nomux=y i8042.noaux=y io_delay=udelay noisapnp pci=nomsi debug root=/dev/mem [ 0.000000] PID hash table entries: 4096 (order: 2, 16384 bytes) [ 0.000000] Dentry cache hash table entries: 131072 (order: 7, 524288 bytes) [ 0.000000] Inode-cache hash table entries: 65536 (order: 6, 262144 bytes) [ 0.000000] Initializing CPU#0 [ 0.000000] Memory: 632784K/655384K available (4590K kernel code, 339K rwdata, 1744K rodata, 284K init, 496K bss, 22600K reserved, 0K cma-reserved) [ 0.000000] virtual kernel memory layout: [ 0.000000] fixmap : 0xfffe4000 - 0xfffff000 ( 108 kB) [ 0.000000] vmalloc : 0xf87e2000 - 0xfffe2000 ( 120 MB) [ 0.000000] lowmem : 0xc0000000 - 0xf7fe2000 ( 895 MB) [ 0.000000] .init : 0xd0a88000 - 0xd0acf000 ( 284 kB) [ 0.000000] .data : 0xd087bcae - 0xd0a86d40 (2092 kB) [ 0.000000] .text : 0xd0400000 - 0xd087bcae (4591 kB) [ 0.000000] Checking if this processor honours the WP bit even in supervisor mode...Ok. [ 0.000000] SLUB: HWalign=32, Order=0-3, MinObjects=0, CPUs=1, Nodes=1 [ 0.000000] NR_IRQS:16 nr_irqs:16 16 [ 0.000000] CPU 0 irqstacks, hard=f7008000 soft=f700a000 [ 0.000000] Console: colour dummy device 80x25 [ 0.000000] console [ttyS0] enabled [ 0.000000] console [ttyS0] enabled [ 0.000000] bootconsole [earlyser0] disabled [ 0.000000] bootconsole [earlyser0] disabled [ 0.000000] tsc: Fast TSC calibration failed [ 0.000000] tsc: Unable to calibrate against PIT [ 0.000000] tsc: No reference (HPET/PMTIMER) available [ 0.000000] tsc: Marking TSC unstable due to could not calculate TSC khz [ 0.040000] Calibrating delay loop... 7023.82 BogoMIPS (lpj=35119104) [ 0.070000] pid_max: default: 32768 minimum: 301 [ 0.080000] Security Framework initialized [ 0.080000] Mount-cache hash table entries: 2048 (order: 1, 8192 bytes) [ 0.090000] Mountpoint-cache hash table entries: 2048 (order: 1, 8192 bytes) [ 0.100000] Disabled fast string operations [ 0.100000] Last level iTLB entries: 4KB 0, 2MB 0, 4MB 0 [ 0.110000] Last level dTLB entries: 4KB 0, 2MB 0, 4MB 0, 1GB 0 [ 0.110000] CPU: Intel Core i7 9xx (Nehalem Class Core i7) (family: 0x6, model: 0x1a, stepping: 0x3) [ 0.150000] Performance Events: unsupported p6 CPU model 26 no PMU driver, software events only. [ 0.160000] devtmpfs: initialized [ 0.160000] clocksource: jiffies: mask: 0xffffffff max_cycles: 0xffffffff, max_idle_ns: 19112604462750000 ns [ 0.170000] kworker/u2:0 (11) used greatest stack depth: 7308 bytes left [ 0.180000] NET: Registered protocol family 16 [ 0.190000] cpuidle: using governor ladder [ 0.190000] cpuidle: using governor menu [ 0.200000] clocksource: pit: mask: 0xffffffff max_cycles: 0xffffffff, max_idle_ns: 1601818034827 ns [ 0.210000] PCI: Using configuration type 1 for base access [ 0.220000] vgaarb: loaded [ 0.220000] SCSI subsystem initialized [ 0.230000] libata version 3.00 loaded. [ 0.230000] usbcore: registered new interface driver usbfs [ 0.240000] usbcore: registered new interface driver hub [ 0.240000] usbcore: registered new device driver usb [ 0.250000] pps_core: LinuxPPS API ver. 1 registered [ 0.250000] pps_core: Software ver. 5.3.6 - Copyright 2005-2007 Rodolfo Giometti <giometti(a)linux.it> [ 0.260000] PTP clock support registered [ 0.270000] dmi: Firmware registration failed. [ 0.270000] PCI: Probing PCI hardware [ 0.280000] PCI: root bus 00: using default resources [ 0.280000] PCI: Probing PCI hardware (bus 00) [ 0.290000] PCI host bridge to bus 0000:00 [ 0.290000] pci_bus 0000:00: root bus resource [io 0x0000-0xffff] [ 0.300000] pci_bus 0000:00: root bus resource [mem 0x00000000-0xffffffff] [ 0.310000] pci_bus 0000:00: No busn resource found for root bus, will use [bus 00-ff] [ 0.320000] pci 0000:00:00.0: [5e14:0042] type 00 class 0x060000 [ 0.330000] pci 0000:00:01.0: [1234:1111] type 00 class 0x030000 [ 0.340000] pci 0000:00:01.0: reg 0x10: [mem 0x90001000-0x90001fff pref] [ 0.350000] pci 0000:00:01.0: reg 0x14: [mem 0x91001000-0x91001fff] [ 0.370000] pci 0000:00:01.0: reg 0x30: [mem 0xfeba0000-0xfebaffff pref] [ 0.380000] vgaarb: setting as boot device: PCI:0000:00:01.0 [ 0.380000] vgaarb: device added: PCI:0000:00:01.0,decodes=io+mem,owns=io+mem,locks=none [ 0.400000] pci 0000:00:02.0: [8086:100e] type 00 class 0x020000 [ 0.400000] pci 0000:00:02.0: reg 0x10: [mem 0x91002000-0x91003fff] [ 0.410000] pci 0000:00:02.0: reg 0x14: [io 0xc000-0xc03f] [ 0.420000] pci 0000:00:02.0: reg 0x30: [mem 0xfeb00000-0xfeb7ffff pref] [ 0.430000] pci 0000:00:03.0: [8086:2918] type 00 class 0x060100 [ 0.440000] pci 0000:00:03.0: quirk: [io 0x0600-0x067f] claimed by ICH6 ACPI/GPIO/TCO [ 0.450000] pci 0000:00:04.0: [8086:2922] type 00 class 0x010601 [ 0.460000] pci 0000:00:04.0: reg 0x10: [io 0xc080-0xc09f] [ 0.470000] pci 0000:00:04.0: reg 0x14: [mem 0x91022000-0x91022fff] [ 0.490000] pci 0000:00:05.0: [8086:2930] type 00 class 0x0c0500 [ 0.490000] pci 0000:00:05.0: reg 0x10: [io 0x0700-0x073f] [ 0.510000] pci_bus 0000:00: busn_res: [bus 00-ff] end is updated to 00 [ 0.520000] PCI: pci_cache_line_size set to 32 bytes [ 0.520000] e820: reserve RAM buffer [mem 0x00007c00-0x0000ffff] [ 0.530000] e820: reserve RAM buffer [mem 0x0009fc00-0x0009ffff] [ 0.540000] e820: reserve RAM buffer [mem 0x90001000-0x93ffffff] [ 0.540000] NetLabel: Initializing [ 0.550000] NetLabel: domain hash size = 128 [ 0.550000] NetLabel: protocols = UNLABELED CIPSOv4 [ 0.560000] NetLabel: unlabeled traffic allowed by default [ 0.570000] clocksource: Switched to clocksource pit [ 0.570000] VFS: Disk quotas dquot_6.6.0 [ 0.580583] VFS: Dquot-cache hash table entries: 1024 (order 0, 4096 bytes) [ 0.580583] hugetlbfs: disabling because there are no supported hugepage sizes [ 0.608902] pci_bus 0000:00: resource 4 [io 0x0000-0xffff] [ 0.622439] pci_bus 0000:00: resource 5 [mem 0x00000000-0xffffffff] [ 0.629178] NET: Registered protocol family 2 [ 0.629178] TCP established hash table entries: 8192 (order: 3, 32768 bytes) [ 0.643721] TCP bind hash table entries: 8192 (order: 3, 32768 bytes) [ 0.651068] TCP: Hash tables configured (established 8192 bind 8192) [ 0.651068] UDP hash table entries: 512 (order: 1, 8192 bytes) [ 0.664304] UDP-Lite hash table entries: 512 (order: 1, 8192 bytes) [ 0.673571] NET: Registered protocol family 1 [ 0.679034] RPC: Registered named UNIX socket transport module. [ 0.679034] RPC: Registered udp transport module. [ 0.691033] RPC: Registered tcp transport module. [ 0.691033] RPC: Registered tcp NFSv4.1 backchannel transport module. [ 0.702947] pci 0000:00:01.0: Video device with shadowed ROM at [mem 0x000c0000-0x000dffff] [ 0.713872] PCI: CLS 0 bytes, default 32 [ 0.719115] Unpacking initramfs... [ 0.728865] Freeing initrd memory: 6180K (d0c71000 - d127a000) [ 0.740017] platform rtc_cmos: registered platform RTC device (no PNP device found) [ 0.749380] Scanning for low memory corruption every 60 seconds [ 0.749380] futex hash table entries: 256 (order: -1, 3072 bytes) [ 0.765067] workingset: timestamp_bits=30 max_order=18 bucket_order=0 [ 0.788927] squashfs: version 4.0 (2009/01/31) Phillip Lougher [ 0.798908] NFS: Registering the id_resolver key type [ 0.798908] Key type id_resolver registered [ 0.812867] Key type id_legacy registered [ 0.818762] Block layer SCSI generic (bsg) driver version 0.4 loaded (major 250) [ 0.831896] io scheduler noop registered [ 0.831896] io scheduler deadline registered [ 0.841111] io scheduler cfq registered (default) [ 0.841111] intel_idle: does not run on family 6 model 26 [ 0.854361] Serial: 8250/16550 driver, 4 ports, IRQ sharing enabled [ 0.877337] serial8250: ttyS0 at I/O 0x3f8 (irq = 4, base_baud = 115200) is a 16550A [ 0.888811] Non-volatile memory driver v1.3 [ 0.888811] [drm] Initialized drm 1.1.0 20060810 [ 0.900611] loop: module loaded [ 0.910483] lpc_ich 0000:00:03.0: I/O space for GPIO uninitialized [ 0.919536] ahci 0000:00:04.0: version 3.0 [ 0.919536] ahci: probe of 0000:00:04.0 failed with error -22 [ 0.931932] pcnet32: pcnet32.c:v1.35 21.Apr.2008 tsbogend(a)alpha.franken.de [ 0.940722] e100: Intel(R) PRO/100 Network Driver, 3.5.24-k2-NAPI [ 0.940722] e100: Copyright(c) 1999-2006 Intel Corporation [ 0.953860] e1000: Intel(R) PRO/1000 Network Driver - version 7.3.21-k8-NAPI [ 0.962047] e1000: Copyright (c) 1999-2006 Intel Corporation. [ 1.029745] BUG: unable to handle kernel paging request at f87f9820 [ 1.029745] IP: [<d06ecf45>] e1000_reset_hw+0x10f/0x180 [ 1.029745] *pde = 37021067 *pte = 00000000 [ 1.029745] Oops: 0000 [#1] [ 1.029745] Modules linked in: [ 1.029745] CPU: 0 PID: 1 Comm: swapper Not tainted 4.8.16 #1 [ 1.029745] task: f704c000 task.stack: f7050000 [ 1.029745] EIP: 0060:[<d06ecf45>] EFLAGS: 00210202 CPU: 0 [ 1.029745] EIP is at e1000_reset_hw+0x10f/0x180 [ 1.029745] EAX: f87f4000 EBX: f73f274c ECX: 00000000 EDX: 00000060 [ 1.029745] ESI: 04140240 EDI: 0000c000 EBP: f7051e38 ESP: f7051e2c [ 1.029745] DS: 007b ES: 007b FS: 0000 GS: 0000 SS: 0068 [ 1.029745] CR0: 80050033 CR2: f87f9820 CR3: 10ad2000 CR4: 00000680 [ 1.029745] Stack: [ 1.029745] f73f2000 00000000 00000000 f7051e78 d06e97c0 f7051e54 f73f2400 00000043 [ 1.029745] f73f274c 00000000 f7083800 00000000 f7051e78 d05bb85a f7051e6c d0a696d4 [ 1.029745] f7083800 f7083868 d0a69694 f7051e90 d05bbb48 d0a69660 f7083868 d0a69694 [ 1.029745] Call Trace: [ 1.029745] [<d06e97c0>] e1000_probe+0x556/0xb18 [ 1.029745] [<d05bb85a>] ? pci_match_device+0x5f/0x7c [ 1.029745] [<d05bbb48>] pci_device_probe+0x51/0x98 [ 1.029745] [<d06a48ed>] driver_probe_device+0xc9/0x1aa [ 1.029745] [<d06a4a26>] __driver_attach+0x58/0x74 [ 1.029745] [<d06a352c>] bus_for_each_dev+0x4f/0x63 [ 1.029745] [<d06a44c1>] driver_attach+0x14/0x16 [ 1.029745] [<d06a49ce>] ? driver_probe_device+0x1aa/0x1aa [ 1.029745] [<d06a4216>] bus_add_driver+0xab/0x18a [ 1.029745] [<d06a4e77>] driver_register+0x6e/0xa0 [ 1.029745] [<d05bb5a0>] __pci_register_driver+0x27/0x2a [ 1.029745] [<d0aa34b0>] ? e100_init_module+0x4d/0x4d [ 1.029745] [<d0aa34e8>] e1000_init_module+0x38/0x6e [ 1.029745] [<d0aa34b0>] ? e100_init_module+0x4d/0x4d [ 1.029745] [<d0400465>] do_one_initcall+0x7c/0xed [ 1.029745] [<d043744a>] ? parse_args+0x1b3/0x27d [ 1.029745] [<d0a88b40>] ? kernel_init_freeable+0xdf/0x17d [ 1.029745] [<d0a88b5d>] kernel_init_freeable+0xfc/0x17d [ 1.029745] [<d0878103>] kernel_init+0x8/0xcb [ 1.029745] [<d087a4e2>] ret_from_kernel_thread+0xe/0x24 [ 1.029745] [<d08780fb>] ? rest_init+0x59/0x59 [ 1.029745] Code: 8b 03 8b 40 18 80 cc 20 8b 13 89 42 18 8b 03 8b 40 08 b8 02 00 00 00 eb 05 b8 05 00 00 00 e8 22 d8 d5 ff 83 7b 0c 04 76 13 8b 03 <8b> 80 20 58 00 00 80 e4 df 8b 13 89 82 20 58 00 003 [ 1.029745] EIP: [<d06ecf45>] e1000_reset_hw+0x10f/0x180 SS:ESP 0068:f7051e2c [ 1.029745] CR2: 00000000f87f9820 [ 1.029745] ---[ end trace f9705abe48180ae4 ]--- [ 1.042868] Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000009 [ 1.042868] [ 1.042868] Kernel Offset: disabled [ 1.042868] ---[ end Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000009 [ 1.042868] [ 2.558940] random: fast init done [ 133.760986] random: crng init done ------------------------------------------------------------

1 0

PicoServer attributes
by christinefragoso＠protonmail.com 16 Nov '21

16 Nov '21

I am running on an i.MX6 the picoserver app https://github.com/seL4/camkes/tree/master/apps/picoserver Both the echo and listener components print out to serial: listener instance starting up, going to be listening on 10.0.0.2:4321 echo instance starting up, going to be listening on 10.0.0.2:1234 but only the echo component receives PicoTCP events: Assigned ipv4 10.0.0.2 to device eth0 IPv6: DAD verified valid address. echo: Connection established with 10.0.0.1 on socket 1 echo: Received a message on socket 3, going to echo to Listener echo: Received a message on socket 3, going to echo to Listener echo: Received a message on socket 3, going to echo to Listener Note that the listener component does not even print out "Connection established". I tried to figure out why, and found out that by editing this part of picoserver.camkes: /* * The attributes of the *_(control/send/recv) interfaces should be the same and unique between * different components, this determines the client ID of this component with respect to * the PicoServer component */ echo.echo_control_attributes = "1"; echo.echo_recv_attributes = "1"; echo.echo_recv_shmem_size = 0x1000; echo.echo_send_attributes = "1"; echo.echo_send_shmem_size = 0x1000; echo.ip_addr = PICOSERVER_IP_ADDR; /* * Listener config */ listener.listener_control_attributes = "2"; listener.listener_recv_attributes = "2"; listener.listener_recv_shmem_size = 0x1000; listener.listener_send_attributes = "2"; listener.listener_send_shmem_size = 0x1000; listener.ip_addr = PICOSERVER_IP_ADDR; and changing the attributes to this: /* * The attributes of the *_(control/send/recv) interfaces should be the same and unique between * different components, this determines the client ID of this component with respect to * the PicoServer component */ echo.echo_control_attributes = "0"; echo.echo_recv_attributes = "0"; echo.echo_recv_shmem_size = 0x1000; echo.echo_send_attributes = "0"; echo.echo_send_shmem_size = 0x1000; echo.ip_addr = PICOSERVER_IP_ADDR; /* * Listener config */ listener.listener_control_attributes = "1"; listener.listener_recv_attributes = "1"; listener.listener_recv_shmem_size = 0x1000; listener.listener_send_attributes = "1"; listener.listener_send_shmem_size = 0x1000; listener.ip_addr = PICOSERVER_IP_ADDR; then listener will print that it has connected to echo, but now echo will not print out anything. How do I make both echo and listener print out on the serial port? Which part of the code looks at echo.echo_recv_attributes = "1"; and listener.listener_recv_attributes = "2"; in order to determine the client ID of the echo and listener components with respect the PicoServer component? From what I can tell, attributes was not declared as an actual attribute.

1 0

RFC-9: new capability for seL4 SMC Forwarding on Arm
by Gerwin Klein 13 Nov '21

13 Nov '21

I’d like to solicit discussion on the new RFC on forwarding Secure Monitor Calls on Arm: https://sel4.atlassian.net/browse/RFC-9 Relevant Arm documentation (SMC calling conventions): https://developer.arm.com/documentation/den0028/latest?_ga=2.116565828.3903… Any opinions, concerns, alternative designs? Cheers, Gerwin

2 4

Camkes VMM configuration
by Jose Martins 10 Nov '21

10 Nov '21

Hello. I've been playing around with the camkes Arm VMM. However, the meaning of some of the configuration fields is not completely clear to me. For example: - what is the difference between "linux_ram_base" and "linux_ram_paddr_base" in the linux_address_config attribute? Are these supposed to define the virtual and physical addresses of the guest's ram region base, respectively? If so, can we have non-identity mappings by setting them to different values? From my experiments having different addresses on those does not always work (even if both are aligned to a 2M superpage boundary) . - what is the difference between the untyped_mmios and mmios attributes? They seem to serve pretty similar purposes. For example, in different vm-examples they are both used for assigning the virtual gic cpu interface to the guest. I probably have a few other questions. I couldn't find it, but I was hoping there was more thorough documentation for the vm configuration detailing the meaning of these fields (and others)? Best regards, José

2 1

Re: Runtime Measurement Hiccup
by Hugo V.C. 08 Nov '21

08 Nov '21

BTW, regarding to the nice trick suggested by Kent (using expect language to interact with console) just wanted to show you this expect script I wrote on 2007 (page 210 of https://www.pentest.es/checkpoint_hack.pdf) to exploit a vulnerability via interactive SSH shell in a very hardened device at that time (Check Point Secure Platform) which was an EAL4+ certified appliance with a locked down custom Linux, and patched kernel (Exec-Shield) with a painful set of memory protections, ASCII Armor, etc + a creative protection in their custom interactive shell (called CPSHELL) that only allowed a restricted set of ASCII chars... It took me 6 months to figure out how to bypass every single protection of that target, and chain all the different bypass techniques into a fully functional exploit. It was hard but I did it and I'm pretty sure anyone with somewhat creative offensive mind (there are thousands out there) would have achieved the same, after or before. Two things I want to highlight here is: 1) Anyone that is tempted to build "insecure" software solutions (Linux/non_verified_code) on top of secure solutions (seL4) must assume for the global design of the architecture that the "insecure" solution (Linux/non_verified_code) should be considered already broken. If you don't do this and expect other low level layers of security to solve root security issues, things may go horribly wrong. This is what happened in the case of Check Point Secure Platform, at that time, all the security was relying in the low level, multiple layers of the OS protections, but the source code of the vendor specific command line tools were full of security bugs... So, let's not expect seL4 host to solve the security problems of the guests (Linux, etc). seL4 can guarantee isolation of guests and it's own security, but as long there's an interaction with the guest (i.e. via console) there's lot of room for exploitation of the guest. 2) Going a step ahead, console interaction is just the most simple, but there are other ways to interact with guests as they are not physically isolated entities of the Universe.... I mean, if we consider chain supply attacks as a real possibility (i.e. an open source tool integrated into a Linux guest on top of seL4) we should be aware that it is not difficult to create a covert channel attack to extract information from the "isolated" guest... So even without any I/O available, the guest can play with multiple physical low level hardware details and physical environment variables to create a funny reliable stealth communication channel. I was just thinking loud but hope it helps someone else to have a wide vision of low level security. Expect scripting interaction with console suggestion by Kent reminded me about this old exploit I wrote and then I extrapolated it to any interaction in our beloved seL4 environments. Have a nice day. El mié, 3 nov 2021 a las 13:00, Hugo V.C. (<skydivebcn(a)gmail.com>) escribió: Very nice trick Kent! Thank you for sharing. That kind of information, from you guys the seL4 experts, is invaluable. El mié, 3 nov 2021 a las 12:15, Kent Mcleod (<kent.mcleod72(a)gmail.com>) escribió: Hi Michael, Just trying to answer your question about how to get data from a simulated system to a host system, the way we do it for sel4test and sel4bench is to use the serial console and grep for magic escape strings. It isn't foolproof but having something like: printf("<digest>%s</digest>\n", digest); from the simulated machine can be captured automatically by the host via matching the input character stream from the console looking to match <digest>.*</digest>. We use expect (https://en.wikipedia.org/wiki/Expect) or the python wrapper pexpect for scripting this and it's how we extract seL4test results and the sel4bench benchmark results that are automatically posted to https://sel4.systems/About/Performance/ via capturing the serial stream. ( https://github.com/seL4/sel4bench/runs/4064401581?check_suite_focus=true shows the output where the benchmark results are just dumped to the console). Kent.

1 0

Graph-refine Toolset Usability Issues (for WCET analysis)
by Jack Chen 06 Nov '21

06 Nov '21

Greetings I'm recently conducting research on WCET analysis of seL4-based systems. Graph-to-graph seems to be a good starting point. However the toolset doesn't seem to be fully working in my setup. My setup: x86, 16GB RAM, Windows10 WSL Ubuntu 20.04 Goal: To replicate the static WCET analysis decribed in the paper [Sewell et al. 2016], using graph-to-graph and graph-refine/seL4-example build. Steps taken: - repo setup with "verification-manifest" - fetched 2 versions: defalut (10/21/2021), and 12.1.0 - followed READMEs: preparing isabelle, HOL4, standalone c-parser, and their dependencies (according to graph-refine/seL4-example/readme) - L4V_ARCH=ARM - [./run_tests] in l4v - [make tar] in graph-refine/seL4-example - [python graph-refine.py <targetdir> all] Results (default version) : --------------------------- - seL4-example [make tar]: all things seem normal except - Graph spec failed in _start for pos 0xe0000008. - Graph spec failed in _start for pos 0xe0000008. - l4v run_tests: 43/51 passed - HaskellKernel STUCK (probably due to internet access issue for my region), CParserTest Failed - graph-refine: KeyError: 'kernel_devices' - This one is interesting. The seL4 code fetched with this "default" manifest contains a "kernel_device_frames", which I think is called "kernel_devices" in previous versions of seL4 kernel code. In kernel.elf.rodata they seem to be associated with the same block of assembly code. Results (12.1.0): --------------------------- - seL4-example [make tar]: same as default, graph spec fails - l4v run_tests: 29/51 passed - HaskellKernel STUCK as usual, CParserTest Failed, CBaseRefine TIMEOUT, AInvs TIMEOUT, a lot others SKIPPED due to dependency - graph-refine: There's no KeyError now because "kernel_devices" is present in this version of seL4 code, but I got this instead: ###======================================= ### Doing stack analysis for 'cap_get_capPtr'. (48 of 575) ### Traceback (most recent call last): ### File "graph-refine.py", line 31, in <module> ### args = target_objects.load_target_args () ### ... ### ... ### File "stack_logic.py", line 223, in get_ptr_offsets ### assert not fail_early, (v, ptr) ### AssertionError: ((3758178040, Expr ('Var', Type ('Word', 32), name = 'r13')), 'r13_after_3758178040_3758178040=i+0') ###===================================== Here are my questions: - Are these issues common, or is my setup & installations just wrong? Any way to resolve these issues? (big questions, and hence the long email, and hence I'm here asking the experts) - Is solver.py currently broken? (dug up some clues in seL4-example/Makefile) - for graph-to-graph, phantom_preempt.py seems required in the convert_loop_bounds step: Any guide on how to write this file, e.g. format, content? - To replicate the WCET experiment in the 2016 paper, should I download the specific version of the verification repo of that time? - static vs. measurement-based WCET analysis: Going forward, on more advanced ARM archs (e.g., Armv8), is static WCET analysis still worth it (or even feasible)? Is hybrid approach the way to go? Is the TS team still working on WCET tools for seL4 on ARM systems? (saw papers from the team many years ago discussing the combination of static cache analysis and probabilistic measurement) Regards, Jack

3 3

Too large messages
by Peter Chubb 05 Nov '21

05 Nov '21

There've been a few messages stuck in the queue recently because they're too large for the list. Please remember when sending to the Devel(a)sel4.systems list -- trim what you're replying to, to just the relevant bits -- reply in-line (no top-posting) -- send only plain text (not screen shots or HTML). Serial port output can be pasted in-line. This will maximise your chance of getting email through on first attempt. -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW

1 0

Re: Runtime Measurement Hiccup
by Hugo V.C. 05 Nov '21

05 Nov '21

Hi Michael! Adding the full list to the thread again (we missed them at some point...). "I appreciate the complete lack of partial credit, and I consider you find my work to be a waste." I don't think anyone thinks your work is a waste. Personally, I just gave my opinion about the architecture, but of course the final decision is yours, as it is your baby :) Maybe someone on the list can answer you with a more specific example you require (even if they already gave some hints...). Cheers, El lun, 25 oct 2021 a las 19:11, Michael Neises (<neisesmichael(a)gmail.com>) escribió: > Hugo (and Everyone), > > Thank you for the reminders. > > I believe it's trivial to provide or restrict caps to any IO device. So, > yes, I believe with the board's reference manual it should theoretically be > quite easy to restrict them all. > > I appreciate the complete lack of partial credit, and I consider you find > my work to be a waste. So with that in mind I'll ask once more: > > Has anyone on the planet ever performed such an independent measurement of > a virtual machine, or is seL4 really as unusable as indicated? > > I don't want to spend any amount of time barking up a tree that doesn't > exist. > > Cheers, > Michael Neises > > > > > > On Mon, Oct 25, 2021, 01:02 Hugo V.C. <skydivebcn(a)gmail.com> wrote: > >> Hi Michael, >> >> as I commented, it depends on the runtime environment. The scenario I >> described, even if challenging, it is just one of many you could face. Let >> me explain myself. >> >> Really, it is irrelevant if the full Linux (or whatever OS) VM is >> "inmutable". At some point you need to load code into memory and run it. >> Then, only formal verified code (like seL4) is reasonably secure. Being >> pedant, anything else simply it is not. >> Why? >> >> The reason is you will never be sure what interactions the VM OS (in your >> example Linux) will have with the outside World. Do you have NTP client...? >> HTTP clients...(wget)? DNS clients...? Are you absolutely sure you know >> every line of this VM OS (Linux) and can guarantee there will be no out of >> control interaction with the outside Word? >> >> Let's go a step ahead in the offensive mindset. Even in the case you are >> building a siloed "air gap" machine (no networking), do you have full >> awareness of all the I/O mechanisms of the device so you can guarantee >> there will be no interaction with the outside World...? >> >> For that reasons code is formally verified. That is the only way to be >> sure things are reasonably secure. >> >> If we accept the last statement as true, any integrity check done from >> inside of unverified code, is, by definition, not trustable. But of course >> you can do it. >> >> On the other side, what I don't get is, if you consider (for whatever >> reason) your guest OS is inmutable... then why you want to check integrity >> from inside...? >> >> In embedded World, integrity checks always need something (theoretically) >> really inmutable (i.e. CPU fuses). You need to check/anchor from the most >> trustable source you have. That's why in embedded devices there are those >> "funny" boot sequences with chain of trust where different parts of the >> system (from most simple to most complex) are used to verify the next step >> in the boot chain. >> >> Having said that, of course you can do integrity checks from inside the >> VM itself, but IMHO will be a waste of trusted computing power of seL4 >> platform. >> >> Please excuse me in advance if I misunderstood your message. >> >> A very interesting topic. >> >> Cheers, >> >> >> El lun., 25 oct. 2021 2:34, Michael Neises <neisesmichael(a)gmail.com> >> escribió: >> >>> Hugo and Everyone, >>> >>> Thanks for the response. This is something I've worried about as well. >>> >>> I've been under the impression that once I compile a seL4 image, that >>> image should be static no matter how many times I boot it. That is, I've >>> looked around for persistent storage to use, and my solution has so far >>> been to recompile the entire seL4 image in order to insert new data. So >>> even when I "touch" files in the Linux virtual machine, they are completely >>> forgotten when I reboot the system. For a time I thought of this as an >>> impediment, but I soon came to realize it as a benefit. So I suppose I >>> should clarify that when I said "Linux kernel" in that quote, I really >>> meant this particular Linux image which is prepared at compile-time and >>> virtualized by seL4 at runtime. >>> >>> For the last several months, I've been operating under the assumption >>> that there is no way for me, even as a developer, to "manipulate the seL4 >>> image I used to boot myself." Namely, I've been trying to jump through all >>> these virtual network hoops because I couldn't figure out a way to make >>> persistent changes to the image. So, as I said, I had taken it for granted >>> that a seL4 image was immutable in this way, but I recognize your point >>> that maybe it is not. My argument has been that the seL4 image is loaded >>> onto an SD card, and I can forbid access to that SD card, which means the >>> image should be guaranteed to be untouchable except maybe by the seL4 >>> kernel itself. >>> >>> I believe seL4's proofs uphold my argument regarding "capabilities" to >>> the SD card, but I admit a slim understanding of seL4's "caps." I will be >>> happy as always to be edified. >>> >>> Cheers and Good Evening to you, >>> Michael Neises >>> >>> On Sun, Oct 24, 2021 at 4:32 PM Hugo V.C. <skydivebcn(a)gmail.com> wrote: >>> >>>> Hi Michael, >>>> >>>> "Please correct me if I am wrong, but I think if the very first thing >>>> the Linux kernel does is measure itself, before it is even connected >>>> to a network, then there is simply no attack surface" >>>> >>>> My 5 cents: it is not so simple... it depends on the specfic run time >>>> environment. >>>> Anyway, just as an example, some years ago I was challenged with a >>>> similar scenario: an appliance running Linux firmware with an embedded >>>> integrity mechanism in the kernel code that checked its own integrity and >>>> also the integrity of all loaded kernel modules (that were doing integrity >>>> checks of the file system). Once initial modules were loaded no more were >>>> allowed to be loaded. >>>> Anyway, the running kernel was very outdated, so I was able to find a >>>> vulnerability that allowed me to inject my own data/code in the kernel >>>> space. The problem was persistence: most of the file system was read >>>> only... with the exception of some config files in the compact flash >>>> storage... a second bug in the parsing of the config files (that allowed >>>> user space command execution to trigger the kernel vuln) gave me the >>>> persistence I wanted for my kernel level vulnerability in that "inmutable" >>>> system. Game over. >>>> >>>> So, it really depends on your environment. As long you have I/O data >>>> operation were an attacker can interact to some persistent storage, then >>>> there's room for persistent intrusion no matter the runtime checks you do >>>> on the kernel or the file system. There have been plenty of even more >>>> elaborated attacks/tricks on heavily siloed and isolated and "inmutable" >>>> systems that have been carried out in the computing history. In fact, those >>>> are the interesting ones... :-) >>>> >>>> Hopes this helps. >>>> >>>> >>>> El dom., 24 oct. 2021 19:46, Michael Neises <neisesmichael(a)gmail.com> >>>> escribió: >>>> >>>>> Hello seL4 developers, >>>>> >>>>> Thank you for the replies. >>>>> >>>>> For the sake of clarity, the system works like this: >>>>> At compile time, some expected digest values are made available only >>>>> to a >>>>> distinct CAmkES component. At the time of first-Linux-boot, a kernel >>>>> module >>>>> takes several measurements of the other kernel modules present >>>>> (including >>>>> itself). It reports these digests outwards to CAmkES, where they are >>>>> compared against the expected values. It is the "pre-compile-time >>>>> provisioning of these expected digests" in which I am interested. At >>>>> this >>>>> time, I can simulate the system and compute these digests, but the >>>>> only way >>>>> I have to extract them is to copy them by hand off the screen. To be >>>>> totally explicit, I want to extract these values in order to re-compile >>>>> them into a system that knows its expected digest values. I want to >>>>> have an >>>>> initial simulation where I extract these digests, so that in the >>>>> subsequent compilation and simulations, the system is aware what values >>>>> these digests are required to take. >>>>> >>>>> Please correct me if I am wrong, but I think if the very first thing >>>>> the >>>>> Linux kernel does is measure itself, before it is even connected to a >>>>> network, then there is simply no attack surface. Of course I'm very >>>>> happy >>>>> to be wrong, but I don't see who the attacker is in this situation. >>>>> Certainly, there remains an open question of how to extend these >>>>> measurements meaningfully into the space where there is a viable attack >>>>> surface (after enabling a network adapter), but I consider that >>>>> question to >>>>> be beside the point for now (some future work). If there is some way >>>>> for me >>>>> to inspect the run-time data of the Linux system without relying >>>>> somewhat >>>>> on a tool inside the Linux instance, I would very much like to know >>>>> about >>>>> it. My strategy follows the same path as the vm-introspect example app >>>>> (which I'm under the impression was created for this explicit purpose), >>>>> which itself trusts implicitly the Linux instance. Again, to be >>>>> entirely >>>>> explicit, there does not appear to be any information anywhere on a >>>>> way to >>>>> meaningfully inspect a virtualized Linux system without trusting it >>>>> even >>>>> the slightest bit. I would be elated to be corrected; if someone can >>>>> show >>>>> me how to scrape (from the seL4 side exclusively) all the bits from a >>>>> virtual Linux system and reassemble those bits into >>>>> semantically-valuable >>>>> information, I'm sure you will not hear from me for several months >>>>> while I >>>>> rebuild everything I have. At this time that does not appear to be >>>>> possible. >>>>> >>>>> Cheers, >>>>> Michael Neises >>>>> >>>>> On Tue, Oct 19, 2021 at 3:46 PM Michael Neises < >>>>> neisesmichael(a)gmail.com> >>>>> wrote: >>>>> >>>>> > Hello seL4 developers, >>>>> > >>>>> > I want to be able to retrieve data from seL4's virtual Linux >>>>> machine, in >>>>> > order to store it in a persistent way. Namely, I want to be able to >>>>> > simulate a seL4 kernel, boot its Linux virtual machine, compute some >>>>> hash >>>>> > digests, and then export those hash digests. These digests are >>>>> valuable >>>>> > because they represent the "clean room" runtime-state of the linux >>>>> machine. >>>>> > Currently I can export these digests by way of hand-eye >>>>> coordination, but I >>>>> > consider this unusable as a piece of software. >>>>> > >>>>> > To date I've taken two main approaches: CAmkES FileServer or virtual >>>>> > networking. I'm under the impression that the FileServer changes are >>>>> not >>>>> > persistent through reboot, and even if they were, to change the boot >>>>> image >>>>> > after compile-time would seem to fly in the face of seL4's >>>>> principles. >>>>> > Virtual networking seems to promise I can host my digests on a >>>>> webpage that >>>>> > is visible to my "root host" machine; that is, the simulated seL4's >>>>> linux >>>>> > instance hosts a site available on my 192.168.x.x network. I know >>>>> there is >>>>> > a seL4webserver app as part of the seL4 repositories which claims to >>>>> do >>>>> > this, but unfortunately its prose is unhelpful and it doesn't seem >>>>> to work >>>>> > even when it compiles and simulates. >>>>> > >>>>> > I've taken two distinct strategies to investigate the virtual network >>>>> > approach. First, I tried to get it to work on my normal stack: >>>>> Windows 10 >>>>> > using WSL2 using a Docker container to simulate the seL4 image. The >>>>> problem >>>>> > with this approach is that it appears I'm required to blindly thread >>>>> 3 or 4 >>>>> > needles all at once, without getting feedback more descriptive than >>>>> "you >>>>> > didn't do it." In other words, there does not appear to be a partial >>>>> > success available, and without ICMP ping, I honestly have no idea >>>>> how to >>>>> > debug these "virtual" networks. >>>>> > >>>>> > Next, I tried simplifying my stack by installing the dependencies >>>>> natively >>>>> > on a Debian 10 machine, which should bypass several layers of the >>>>> virtual >>>>> > network I was suggesting in my first strategy. Unfortunately, I met >>>>> with >>>>> > the same "AttributeError: module 'yaml' has no attribute >>>>> 'FullLoader'" >>>>> > error that inspired me to begin using Docker several years ago. Of >>>>> course I >>>>> > should note that "pip/pip2/pip3 install pyyaml" all report that >>>>> pyyaml is >>>>> > already installed, so I would be in debt to anyone who has an idea >>>>> about >>>>> > that error. >>>>> > >>>>> > To conclude, I find virtual networks opaque, and I would be grateful >>>>> for >>>>> > any guidance. If you have a different idea how I might achieve my >>>>> goal, I >>>>> > would be similarly effusive in my thanks. >>>>> > >>>>> > Cheers, >>>>> > Michael Neises >>>>> > >>>>> _______________________________________________ >>>>> Devel mailing list -- devel(a)sel4.systems >>>>> To unsubscribe send an email to devel-leave(a)sel4.systems >>>>> >>>>

4 7

Pine64 PinePhone with seL4: any prior attempts?
by Isaac Beckett 03 Nov '21

03 Nov '21

Hello! I recently received a PinePhone for my birthday, and it finally arrived a few weeks later. It’s been fun to tinker with so far, although I haven’t yet replaced the Linux distro it came with yet, which I plan to do soon. But thinking about my options for that made me wonder, has anyone attempted to run seL4, even just a test program, on one of these before? It’s an aarch64 device using a quad-core Allwinner A64 SOC, so four Cortex CPU cores and an Arm Mali GPU. I don’t have any experience bringing up an OS in new hardware. It runs Linux fine, and while the included software setup is a bit sluggish, I’m pretty sure that’s just from Plasma mobile being very resource hungry. So, I’m curious, has anyone experimented with this in the past? I think this platform could be very useful, personally I’m hoping that as hobbyist type phones like this become more mature, that people will have more choices for software to run on it.

3 2

CAmkES: dataports larger than 4k
by Fabrizio Bertocci 01 Nov '21

01 Nov '21

Is it possible to use dataports that are larger than 4k? I tried with both typed dataports and "Buf" dataport but I can't find a way to do it. In the hello-camkes-2 tutorial, I tried to add a configuration for my dataports in the main assembly file to increase its size like this: // Typed dataport name: 'd_image' // Buf dataport name: 'd' configuration { echo.d_size=65536; // Buf dataport echo.d_image_size=65536; // Typed dataport } unfortunately that doesn't seem to do anything as d_get_size() keep returning 4k, and for the typed dataport, the build system triggers the static assert "typeof(from_0_d_image_data) size greater than dataport size" Thanks, Fabrizio

2 1

Runtime Measurement Hiccup
by Michael Neises 25 Oct '21

25 Oct '21

Hello seL4 developers, I want to be able to retrieve data from seL4's virtual Linux machine, in order to store it in a persistent way. Namely, I want to be able to simulate a seL4 kernel, boot its Linux virtual machine, compute some hash digests, and then export those hash digests. These digests are valuable because they represent the "clean room" runtime-state of the linux machine. Currently I can export these digests by way of hand-eye coordination, but I consider this unusable as a piece of software. To date I've taken two main approaches: CAmkES FileServer or virtual networking. I'm under the impression that the FileServer changes are not persistent through reboot, and even if they were, to change the boot image after compile-time would seem to fly in the face of seL4's principles. Virtual networking seems to promise I can host my digests on a webpage that is visible to my "root host" machine; that is, the simulated seL4's linux instance hosts a site available on my 192.168.x.x network. I know there is a seL4webserver app as part of the seL4 repositories which claims to do this, but unfortunately its prose is unhelpful and it doesn't seem to work even when it compiles and simulates. I've taken two distinct strategies to investigate the virtual network approach. First, I tried to get it to work on my normal stack: Windows 10 using WSL2 using a Docker container to simulate the seL4 image. The problem with this approach is that it appears I'm required to blindly thread 3 or 4 needles all at once, without getting feedback more descriptive than "you didn't do it." In other words, there does not appear to be a partial success available, and without ICMP ping, I honestly have no idea how to debug these "virtual" networks. Next, I tried simplifying my stack by installing the dependencies natively on a Debian 10 machine, which should bypass several layers of the virtual network I was suggesting in my first strategy. Unfortunately, I met with the same "AttributeError: module 'yaml' has no attribute 'FullLoader'" error that inspired me to begin using Docker several years ago. Of course I should note that "pip/pip2/pip3 install pyyaml" all report that pyyaml is already installed, so I would be in debt to anyone who has an idea about that error. To conclude, I find virtual networks opaque, and I would be grateful for any guidance. If you have a different idea how I might achieve my goal, I would be similarly effusive in my thanks. Cheers, Michael Neises

4 6

Verified platform (Sabre lite)
by ouvl 15 Oct '21

15 Oct '21

Good afternoon. The only verified platform is Sabre lite (Platform Sabre lite, System-on-chip i.MX6). There is a link for the board on the website https://docs.sel4.systems/Hardware/sabreLite.html, but the link https://boundarydevices.com/product/sabre-lite-imx6-sbc/ is not working. On the same site https://boundarydevices.com, board https://boundarydevices.com/product/bd-sl-i-mx6/ is displayed. There are different boards with iMX6 processor, and processors, for example, i.MX 6 ULL, i.MX 6 UltraLite, i.MX 6 SLL, i.MX 6 SoloLite, i.MX 6 SoloX, i.MX 6 Solo, i.MX 6 Solo, i.MX 6 Dual, i.MX 6 Quad, i.MX 6 DualPlus, i.MX 6 QuadPlus. There is only 1 GiB of RAM in the board, so please clarify regarding my question. Are all the boards suitable for the operation of a verified microkernel seL4 with full verification, or is only https://boundarydevices.com/product/bd-sl-i-mx6/ suitable board?

1 0

Inter-VM communication on seL4
by everton＠ssrc.tii.ae 29 Sep '21

29 Sep '21

Hello seL4-devs, I am working with seL4 running as a hypervisor with multiple VMs. I am aware of vchan (inactive) and VirtIO Net as mechanisms for inter-VM communication on top of seL4. However, I am looking to have a shared memory inter-VM communication between my VMs. Is there a well-maintained mechanism with shared memory and notifications for inter VM communication? I have been trying to create a CAmkES example with dataport and I found out this "seL4SharedDataWithCaps" CAmkES connector for connecting dataport interfaces (https://github.com/seL4/global-components/issues/8) connection seL4SharedDataWithCaps sharedMem(from vm0.dummy_port, to vm0.buff, to vm1.buff); The "to" side of the connection is supposed to give capabilities to both vmm0 and vmm1 (workaround proposed in the link above). How to use those capabilities to map "buff" into Linux guest address space? Ideally, I would like to access that "buff" from Linux kernel without VMM intervention. Thank you in advance. Best, Everton

2 1

ethernet pass-through using CAmkES VM on x86
by meshkat os 29 Sep '21

29 Sep '21

hi I am new to camkes VM on x86. I want to connect the guest to the host via the ethernet network. and I used this ( https://docs.sel4.systems/projects/camkes-vm/) tutorial to create pass-through in minimal example x86. run in qemu on ubuntu 17.10. but the guest os doesn't create an ethernet interface. I also tested zmq example this is qemu options: qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,enforce,+vmx -nographic -serial mon:stdio -m size=2G -enable-kvm -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-image-ia32-pc99 and minimal.camkes configs: configuration { VM_CONFIGURATION_DEF() VM_PER_VM_CONFIG_DEF(0) vm0.simple_untyped23_pool = 20; vm0.heap_size = 0x2000000; vm0.guest_ram_mb = 128; vm0.kernel_cmdline = VM_GUEST_CMDLINE; vm0.kernel_image = "bzimage"; vm0.kernel_relocs = "bzimage"; vm0.initrd_image = "rootfs.cpio"; vm0.iospace_domain = 0x0f; vm0_config.pci_devices_iospace = 1; vm0_config.ioports = [ {"start":0x4080, "end":0x4090, "pci_device":0x1f, "name":"SATA"}, {"start":0x4090, "end":0x40a0, "pci_device":0x1f, "name":"SATA"}, {"start":0x40b0, "end":0x40b8, "pci_device":0x1f, "name":"SATA"}, {"start":0x40b8, "end":0x40c0, "pci_device":0x1f, "name":"SATA"}, {"start":0x40c8, "end":0x40cc, "pci_device":0x1f, "name":"SATA"}, {"start":0x40cc, "end":0x40d0, "pci_device":0x1f, "name":"SATA"}, {"start":0x3000, "end":0x3020, "pci_device":0, "name":"Ethernet5"}, ]; vm0_config.pci_devices = [ { "name":"SATA", "bus":0, "dev":0x1f, "fun":2, "irq":"SATA", "memory":[], }, { "name":"Ethernet5", "bus":5, "dev":0, "fun":0, "irq":"Ethernet5", "memory":[ {"paddr":0xc0500000, "size":0x20000, "page_bits":12}, {"paddr":0xc0520000, "size":0x4000, "page_bits":12}, ], }, ]; vm0_config.irqs = [ {"name":"SATA", "source":19, "level_trig":1, "active_low":1, "dest":11}, {"name":"Ethernet5", "source":0x11, "level_trig":1, "active_low":1, "dest":10}, ]; } thanks

4 4

seL4 Raspberry Pi 4B Support
by Drew Humphrey 29 Sep '21

29 Sep '21

Hi, I am doing a feasibility study to ascertain whether Linux can be deployed to a seL4 kernel running on a Pi 4B with 8GB of memory. I have seen that there is explicit support for the Pi 3B, and that Linux can be run in a virtual machine on top of seL4. But I did not see explicit support for a Pi 4B and the ability to have the Pi run the Linux VM. Please let me know if this would be possible. Thanks, Drew Humphrey

4 3

Mismatch in number of pages allocated
by Sid Agrawal 29 Sep '21

29 Sep '21

Hi sel4-dev, I was looking at the sel4utils/vspace <https://github.com/seL4/seL4_libs/tree/master/libsel4utils> library and noticed a mismatch in the number of pages allocated as per the two data structures which keep track of the address space. Below I have laid out my test setup, steps to reproduce and finally the exact questions. In my test setup(which is copied from sel4test system), the root task(driver) starts another process(test app) with its own address space using sel4utils_spawn_process_v.(inside basic_run_test). Then in the root task we do a walk of the child task's address space structures maintained by sel4utils/vspace library. The 2 structures I am walking are: - The linked list of reservations: source-code <https://github.com/seL4/seL4_libs/blob/master/libsel4utils/include/sel4util…>: Here we traverse a linked list and count the number of pages which have been allocated based on the size of each reservation. - The tree which keeps the caps of pages mapped so far(sort of like the shadow page table). source-code <https://github.com/seL4/seL4_libs/blob/master/libsel4utils/include/sel4util…>. Here we traverse the multi-level shadow page table hierarchy to count the pages the library has mapped. I find that the number of pages I get from the 2 walks are not equal. I understand that neither of the above are reflective of the true state of the address space as that is only known to the kernel. So, it is simply possible that in some code path, the library inserts an entry in to one of the structures and not the other. I have used Intel 32-bit platform to keep the page table structure simple for this query. Here is the code to walk the vspace(source code) <https://github.com/sid-agrawal/seL4_libs/blob/0d37c61f89dc335a5905f5625be31…> : int sel4utils_walk_vspace(vspace_t *vspace, vka_t *vka) { sel4utils_alloc_data_t *data = get_alloc_data(vspace); int index = 0; sel4utils_res_t *sel4_res = data->reservation_head; printf("===========Start of interesting output================\n"); printf("VSPACE_NUM_LEVELS %d\n", VSPACE_NUM_LEVELS); /* walk all the reservations */ printf("\nReservations from sel4utils_alloc_data->reservation_head:\n"); while (sel4_res != NULL) { long int sz = (sel4_res->end - sel4_res->start ) / (4 * 1024); printf("\t[%d] %p->%p %lu pages malloced(%u)\n", index, sel4_res->start, sel4_res->end, sz, sel4_res->malloced); index++; sel4_res = sel4_res->next; } int num_empty = 0; int num_reserved =0; int num_used =0; int i = 0; /* Walk all the page tables */ printf("\n\nIntel-32 Page Table Hierarcy from sel4utils_alloc_data->top_level->table \n"); if (data->top_level) { for (i = 0; i < BIT(VSPACE_LEVEL_BITS); i++) { if (data->top_level->table[i] == RESERVED) { num_reserved++; } else if (data->top_level->table[i] == EMPTY) { num_empty++; } else { num_used++; vspace_bottom_level_t *bottom_table = (vspace_bottom_level_t *)data->top_level->table[i]; int L2_num_empty = 0; int L2_num_reserved = 0; int L2_num_used = 0; int ii = 0; for (ii = 0; ii < BIT(VSPACE_LEVEL_BITS); ii++) { uintptr_t cap = bottom_table->cap[ii]; if (cap == RESERVED) { L2_num_reserved++; } else if (cap == EMPTY) { L2_num_empty++; } else { L2_num_used++; } } printf("PDE-Index(%d) \n\t" \ "NUM-PTE: %5d Empty: %5d \tReserved: %5d \tUsed: %5d\n", i, ii, L2_num_empty, L2_num_reserved, L2_num_used, ii); } } printf("===========Start of interesting output================\n"); } return index; } Test Environment: - The docker environment was setup using instruction from Using Docker for seL4 <https://docs.sel4.systems/projects/dockerfiles/>. - Qemu on Ubuntu 20.04 on 64 bit Intel machine Below is the steps to reproduce the issue: # Setup the project using a manifest repo. # The structure of the project is borrowed from sel4test. # The manifest points two repo's which are not original sel4 repos: # - seL4_libs: The new walker helper is here, based on fork of sel4/sel4_libs # - sel4-gpi: The test code is here. This is new repo. mkdir sel4-gpi-system cd sel4-gpi-system repo init -u https://github.com/sid-agrawal/sel4-gpi-manifest -b refs/tags/v3.0 repo sync container # Jump to the docker sel4 dev environment, omit if you do not care mkdir build cd build ../init-build.sh -DPLATFORM=ia32 -DSIMULATION=TRUE ninja && ./simulate # To exit Qemu Ctrl-A X The output from the test code is: ===========Start of interesting output================ VSPACE_NUM_LEVELS 2 Reservations from sel4utils_alloc_data->reservation_head: [0] 0x10001000->0x10012000 17 pages malloced(1) Intel-32 Page Table Hierarcy from sel4utils_alloc_data->top_level->table PDE-Index(32) NUM-PTE: 1024 Empty: 637 Reserved: 0 Used: 387 PDE-Index(64) NUM-PTE: 1024 Empty: 1005 Reserved: 1 Used: 18 ===========Start of interesting output================ The first part of the output shows the size of the reservation in number of 4KB pages which is 17 pages. We see that the vspace has only 1 reservation, which is 17 pages long and is malloced. This itself is a little odd; I was expecting multiple reservations for code, stack, ro-data etc. The second part of the output shows the page directory and table entries. Here we see that the 2 PDE are in use with a total of 405(18 + 387) PTEs used in total. So, my query is, why is there is a discrepancy in the number of pages used? - Does the library allocate a bunch of pages(387) which do not belong to any reservation? - As far as the single page difference of 17 Vs 18, I think that can be explained by the driver sharing a page with the test-app. Besides the above, I have a couple of more general questions about the user space virtual memory libraries in seL4. - Why does the library need to mimic the PT hierarchy in user space? - I am trying to implement fork in the sel4utils, mainly as an exercise. Is there a helper function to duplicate an address space(let's say without any COW)? Thanks for your time. If there is some additional info I should be providing while raising question on this forum do let me know. Best, Sid

1 0

"Incorporating into your project"
by fosslinux 27 Sep '21

27 Sep '21

Dear seL4 devs and community. I am attempting to integrate seL4 into a new project of mine. To begin setting up this project, I used https://docs.sel4.systems/projects/buildsystem/incorporating.html as a reference to set up the structure of the repository (FWIW, I did not use repo, however I do not believe this should impact the build system). However, it appears these instructions may be outdated(?) or otherwise incorrect. I set up a file structure as shown under the heading "Kernel directory" in the above webpage, taking sources from; kernel/ -> https://github.com/sel4/sel4 projects/seL4_libs/ -> https://github.com/seL4/seL4_libs tools/ -> https://github.com/seL4/seL4_tools I symlinked default-CMakeLists.txt to CMakeLists.txt in the root directory as well as init-build.sh to the root directory. I created a build directory, and from within that directory, executed ../init-build.sh -DPLATFORM=X86_64 -DSIMULATION=TRUE, but this produced the CMake error; CMake Error at kernel/configs/seL4Config.cmake:174 (message): Variable 'KernelArch' is not set. Call Stack (most recent call first): kernel/CMakeLists.txt:10 (include) (I got the same result regardless of PLATFORM value). I cannot tell where the issue lies. Any pointers would be appreciated. Kind regards, ST (fossy)

2 2

Call for participation in embedded power system security exercise
by Gernot Heiser 27 Sep '21

27 Sep '21

Abstract: We are conducting a small embedded power systems security exercise at Charles Darwin University Control Systems Test Facility (CSTF) on the Laot System designed for protecting critical infrastructure (see https://trustworthy.systems/projects/TS/laot, https://eds.power.on.net/laot-pub) The exercise will involve penetration testing with the targets being a generator controlled by a Comap controller and a small nuclear reactor simulator (see https://eds.power.on.net/little-moata/index) These devices will for parts of the exercise be protected by the Laot system. There will be no cost to participants. All material including reports will be provided to all participants at the end. Keywords: seL4, Laot, MODBUS, Security, Protection of Critical Infrastructure, Hybrid Power Systems, AUUG What: Laot is a seL4-based system for protecting critical infrastructure. Why: The exercise is intended to test the system and provide a useful exercise for the penetration testing on industrial control systems. When: Over the next 2-4 weeks. How: Send an email or ring Phil he will give you an exercise brief and timings. Any general enquires are also welcome via the same means. Where: Remote for participants but the lab is in Darwin, Northern Australia. Local Darwin participants will be provided appropriate Darwin food and drink. Who: The 3 members of the Laot team are Gernot Heiser, Ben Leslie and Phil Maker. What: the exercise will be conducted over a 72h period in order to document and describe vulnerabilities in a variety of systems. Please read the Laot and little moata references above and contact Phil. In terms of background you will need to know the usual kali penetration tools (nmap, ...) and have an idea about either C or MODBUS. We will provide example code and exercise instructions. Phil Maker web: https://eds.power.on.net/EDS email: <philip.maker(a)gmail.com> phoneemail: <philmakerphone(a)gmail.com> -- email to phone (fastest) phone: +61 (0)447 630 229

1 0

Known working embedded device for CAmkES VMs
by christinefragoso＠protonmail.com 23 Sep '21

23 Sep '21

I want to run cross-communicating CAmkES VMs on an embedded device. I see from https://github.com/seL4/camkes-vm-examples that my options are optiplex9020, cma34cr, and exynos5422. Are there any other options? Which of these options are known to work properly with a recent seL4 image?

1 0

Removing support for KZM, i.MX31 and ARMv6
by Matthew Brecknell 16 Sep '21

16 Sep '21

To reduce maintenance burden, we would like to remove seL4 support for the KZM evaluation board, which is based on the freescale i.MX31 processor with an ARM1136 core. Since this is the only ARMv6 platform supported by seL4, this would also remove support for ARMv6. We've previously sought feedback here, and in the seL4 discourse: https://sel4.discourse.group/t/should-we-continue-to-support-armv6-and-kzm-… https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/EQ27WY… We've now prepared an RFC to begin the formal process to remove KZM support: https://sel4.atlassian.net/browse/RFC-8 If you have concerns about this, please raise them as soon as possible! If you support the change, please also let us know, since that helps us establish consensus.

1 0

sel4webserver build problem
by Michael Neises 15 Sep '21

15 Sep '21

Hello, I'm trying to learn from the "sel4webserver" app here: https://docs.sel4.systems/projects/sel4webserver/. I believe I've been able to configure my network the way described on that page, but I'm failing to build because I'm missing the docsite dependencies here: https://github.com/seL4/docs/blob/master/tools/Dockerfile I build all my camkes apps using docker's `make user` with these files here: https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles.git I'm sure there's a way to have a docker container with these camkes dependencies as well as the docsite dependencies, but I'm not an expert with docker. Does anyone have any tips on how to make all these things play nice together? Cheers, Michael Neises

1 0

Steal This Drone: High Assurance Cyber Military Systems
by William ML Leslie 02 Sep '21

02 Sep '21

Looks like the HACMS talk from Collins Aerospace at DEFCON is up. This covers the system they built to fly aircraft on seL4, and especially the tools they used to do so. It's pretty light on technical content, but still quite impressive. https://youtu.be/X9rsv4YIShY -- William Leslie Q: What is your boss's password? A: "Authentication", clearly Notice: Likely much of this email is, by the nature of copyright, covered under copyright law. You absolutely MAY reproduce any part of it in accordance with the copyright law of the nation you are reading this in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without prior contractual agreement.

1 0

Port to a cartesi-machine (riscv:rv64ima)
by marcelo.politzer＠cartesi.io 31 Aug '21

31 Aug '21

Hi, I'm in the process of porting seL4 to a cartesi-machine, which is basically a riscv:rv64ima without PMP (at least for now). after increasing the available memory 4G and a tweak in the elfloader to accept the flattened device tree from OpenSBI I got the kernel to start[1], but with errors. Tried to boot a hello world and the sel4tests, both give pretty much the same result. I have a suspicion that the unsupported PMP may have something to do with this but since I'm still pretty new to seL4 so I would like advice on how to debug this further. Best, Marcelo [1] ``` OpenSBI v0.9 ____ _____ ____ _____ / __ \ / ____| _ \_ _| | | | |_ __ ___ _ __ | (___ | |_) || | | | | | '_ \ / _ \ '_ \ \___ \| _ < | | | |__| | |_) | __/ | | |____) | |_) || |_ \____/| .__/ \___|_| |_|_____/|____/_____| | | |_| Platform Name : Cartesi Platform Features : mfdeleg Platform HART Count : 1 Platform IPI Device : aclint-mswi Platform Timer Device : aclint-mtimer Platform Console Device : htif Platform HSM Device : --- Platform SysReset Device : htif Firmware Base : 0x80000000 Firmware Size : 260 KB Runtime SBI Version : 0.3 Domain0 Name : root Domain0 Boot HART : 0 Domain0 HARTs : 0* Domain0 Region00 : 0x0000000002080000-0x00000000020bffff (I) Domain0 Region01 : 0x0000000002000000-0x000000000207ffff (I) Domain0 Region02 : 0x0000000080000000-0x000000008007ffff () Domain0 Region03 : 0x0000000000000000-0xffffffffffffffff (R,W,X) Domain0 Next Address : 0x0000000080200000 Domain0 Next Arg1 : 0x000000017fff0000 Domain0 Next Mode : S-mode Domain0 SysReset : yes Boot HART ID : 0 Boot HART Domain : root Boot HART ISA : rv64imasu Boot HART Features : scounteren,mcounteren,time Boot HART PMP Count : 0 Boot HART PMP Granularity : 0 Boot HART PMP Address Bits: 0 Boot HART MHPM Count : 0 Boot HART MIDELEG : 0x0000000000000222 Boot HART MEDELEG : 0x000000000000b109 ELF-loader started on (HART 0) (NODES 1) paddr=[80200000..806e5037] Loaded DTB from 17fff0000. paddr=[84025000..84025fff] ELF-loading image 'kernel' to 84000000 paddr=[84000000..84024fff] vaddr=[ffffffff84000000..ffffffff84024fff] virt_entry=ffffffff84000000 ELF-loading image 'sel4test-driver' to 84026000 paddr=[84026000..8445bfff] vaddr=[10000..445fff] virt_entry=1eef8 Enabling MMU and paging Jumping to kernel-image entry point... Init local IRQ Bootstrapping kernel Initialing PLIC... Booting all finished, dropped to user space /host/cartesi/kernel/src/kernel/faulthandler.c:156 :: Caught cap fault in send phase at address 0 while trying to handle: user exception 0x2 code 0 in thread 0xffffffc17feca200 "rootserver" at address 0x101f0 With stack: 0x333e70: 0x4 0x333e78: 0x3 0x333e80: 0x333ec0 0x333e88: 0x1f884 0x333e90: 0x333f30 0x333e98: 0x333f20 0x333ea0: 0x333f10 0x333ea8: 0x100000000 0x333eb0: 0x333f00 0x333eb8: 0x1f008 0x333ec0: 0x0 0x333ec8: 0x333f30 0x333ed0: 0x333f20 0x333ed8: 0x333f10 0x333ee0: 0x1 0x333ee8: 0x14540 ```

4 7

Compiling rumprun's libc as a shared object
by Ellis 27 Aug '21

27 Aug '21

Hello, Recently I have been trying to use sel4 rumprun on another build system after compiling but I've noticed that rumprun or musl libc only produce static libraries. How would I compile libc as a shared object? Sincerely, Ellis

1 0

Re: Is the project port Minix 3 to run on seL4 already in work?
by Christian Sagstetter 24 Aug '21

24 Aug '21

@Gernot yes that's exactly what I meant when I saw the suggested project here: https://docs.sel4.systems/SuggestedProjects.html. is there anything left from the student project that I could continue working on? best, christian

2 1

DeclareCAmkESComponent questions
by Grant Jurgensen 24 Aug '21

24 Aug '21

Hi, I have a couple questions about the `DeclareCAmkESComponent` CMake function. First, is there a way to add a dependency to a CAmkES component? Normally I would use the CMake function `add_dependencies`, but this requires a target name, and I don't believe that the `DeclareCAmkESComponent` function exposes any such target name. If the function deliberately obscures the target name, perhaps a `DEPENDENCIES` argument could be added to the function? Second, does the `INCLUDES` argument to `DeclareCAmkESComponent` ignore / filter out certain include paths? My compilation was failing because it could not find the proper headers packaged with my compiler. Even if I added the path explicitly by passing it to the `INCLUDES` argument, it was seemingly ignored. It wasn't until I copied the headers to a new directory, and explicitly passed that directory to `INCLUDES` that my compilation succeeded. Any ideas what's going on here? Thanks! Grant Jurgensen

3 6

Is the project port Minix 3 to run on seL4 already in work?
by christian.sagstetter＠googlemail.com 24 Aug '21

24 Aug '21

hello everyone, I would be interested in the project and wanted to know if it is already being worked on. best christian

3 3

Uses and description for seL4_CNode_Mutate?
by Mark Jones 23 Aug '21

23 Aug '21

This isn't a big issue, but I'm curious about how seL4_CNode_Mutate is intended to be used, and have found that the description in the seL4 reference manual doesn't seem to match the implementation. Is it for changing rights? The manual (Section 3.1.2) says: "seL4_CNode_Mutate() can move a capability similarly to seL4_CNode_Move() and also reduce its rights..." Section 3.1.4 also refers to the possibility to specify a new set of rights with an invocation of seL4_CNode_Mutate(). However, the summary of seL4_CNode_Mutate in Section 10.3.1.6 does not include a parameter that specifies any rights information, so it appears that it cannot actually be used in this way. Is it for changing badges? In Section 4.2.1, the manual says that "An endpoint capability with a zero badge ... can be badged with the seL4_CNode_Mutate() or seL4_CNode_Mint() invocations" There is a similar statement for Notifications in Section 5.1. But a comment in the (Haskell version of the) spec says "endpoint capabilities may not have their badges changed" when they are updated by a Mutate or Rotate operation. And the kernel seems to follow this: I added a test to sel4test to confirm that you get an illegal operation error if you try to badge an endpoint using Mutate. (Assuming I wrote the test correctly ...) Unless there are other arch-specific use cases, it looks like the only thing you can do with Mutate is to change the guard of a CNode capability. Even then, that is only possible if you are moving the capability at the same time. Of course, you could combine a mutate with a regular move to simulate an in-place update ... but you could also use an in-place mutate and a separate move to simulate the current behavior, without having to find an empty slot if you just wanted the in-place operation. One conclusion is that the manual's description of Mutate probably needs an update. But if nobody else has tripped over problems using it to create badged endpoints, then perhaps Mutate just isn't being used very much at all and could be removed altogether? A second thought is whether Mutate could be modified to perform an in-place update if the source and destination are the same (i.e., similar in some ways to how you specify a swap with Rotate)? Best wishes, Mark

4 5

bingup the new platform not in Linux repository
by niewei1899＠163.com 20 Aug '21

20 Aug '21

about portint doc：(https://docs.sel4.systems/projects/sel4/porting) “You may need to add device nodes depending on what Linux uses and what is required by seL4. For example, in the port of the Rockpro64 a memory node and an extra timer node were needed so these had to be defined manually.” how can I get the required by seL4? have any doc about it?

1 0

smp camkes
by David Lorentz 19 Aug '21

19 Aug '21

Hi, I've been trying to extend one of the tutorial / example projects to run on more than one core with no success. After reading the camkes manual https://docs.sel4.systems/projects/camkes/manual.html#thread-cpu-affinity I assumed that you need to set core affinities for different components in your camkes file and set the KernelMaxNumNodes to a number greater than one. I tried this with the adder sample (as below) with no luck. Can anyone point me to some information on how to get smp to work, what hardware is supported and the like? configuration { adder.affinity = 1; client.affinity = 0; } Thanks David

1 0

VM support for iMX8MM/MQ dev boards
by Zippy Manaic 18 Aug '21

18 Aug '21

Hi, I have been attempting to follow some breadcrumbs to get vm_minimal app running on an IMX8 dev board. I am attempting to follow the commits by Sylvain but I think there may be a missing push to seL4/camkes-vm. Are there any plans to more formally support iMX8 platforms for VM development on seL4? Assuming I manage to get vm_minimal running on iMX8 what would be the odds of getting 2 VMs running on iMX8? Are there known limitations to the current CAmkES VM implementation that would cause me problems? Thanks, Zippy

1 0

seL4 Kernel: ARMv8.2 support
by Jorge Pereira 17 Aug '21

17 Aug '21

Hi all, Is the seL4 Kernel (with VE enabled) supporting versions of ARMv8 (e.g. ARMv8.2) other than the original one - v8.0? We'd like to port seL4 for a board that features ARMv8.2 CPUs. Is there any foreseeable roadblock? Thanks.

1 0

[Tutorial] Should the tutorial of seL4 be updated?
by Zheng Wenxin 10 Aug '21

10 Aug '21

It seems that the tutorial "CAmkES VM: Cross VM Connectors" has something missing. The part "Add modules to the guest" says that "There is a library in projects/camkes/vm-linux/camkes-linux-artifacts/camkes-linux-apps/camkes-connector-apps/libs containing Linux system call wrappers ...". But no folder named camkes/vm-linux and in camkes-vm-linux/camkes-linux-artifacts/camkes-linux-apps/camkes-connector-apps, no folder named libs. Is the tutorial should be updated?

1 0

seL4 how to access el3 secure world on ARM platfrom
by yadong.li 07 Aug '21

07 Aug '21

Hi： We want to create component driver who need to access ARM el3 secure world to read/write hardware register. But I found that seL4 did not offer capability to call smc function for component of native world. Which cap that already existed can offer the syscall or create new smc cap ? Is there some plan to support it ? Thank you very much.

2 1

some unexpected phenomenon about scheduling
by yadong.li 07 Aug '21

07 Aug '21

Hi: Recently, I found some unexpected phenomenon about scheduling on our project. My environment as follows: I run linux guest on seL4, Linux guest has 8 vcpu on 8 Arm PE from core0 ~ core7. WFI is not trap, seL4 is master kernel not mcs kernel I think seL4 idle task will not be run on core1, it will always run vcpu task. But the truth is the idle task will be run. I found when the maintenance and timer interrupt of Linux guest came, it will switch to idle, Because above interrupts handle will call handleFault, the sendIPC will set the ksCurThread(vcpu task) block on send, and the ksReadyQueuesL1Bitmap is empty. The idle task wille be run. But the recv task maybe run on core0, now core1 is in idle, is it reasonable? Thank you very much

2 1

Failure on a CAmkES-VM with more than 150MB RAM
by hamed_ganji＠aut.ac.ir 06 Aug '21

06 Aug '21

Hello, I have a problem on booting a CAmkES-VM with more than 150MB RAM. The following error appears when I set [vm0.guest_ram_mb = 256] in the camkes file of the minimal example of CAmkES-VM and boot the produced image on both QEMU and real hardware system: ------------------------------------------------------------ ... vka_alloc_object_at_maybe_dev@object.h:64 Failed to allocate object of size 4096, error 1 alloc_bios_memory@acpi.c:119 Failed to allocate frame for bios addr 0xe0000 main_continued@main.c:871 [Cond failed: error] Failed to init guest boot structure ------------------------------------------------------------ Please find the full output of the booting process in attachment file. I also examined the effect of other parameters like [vm0.simple_untyped23_pool] and [vm0.heap_size] but no difference was found. Any help/hint would be very appreciated. Best regards, Hamed Ganji

1 0

Where does rumprun mount /
by Ellis 04 Aug '21

04 Aug '21

Hello, I have been messing around with sel4 rumprun and I have been trying to put files onto the file system. Where does rumprun mount the root / ? Sincerely, Ellis

1 0

Operating Systems built on top of seL4
by Sidhartha Agrawal 02 Aug '21

02 Aug '21

Hello sel4-devs, I am a first-year graduate student at the University of British Columbia at their Systopia Lab <https://systopia.cs.ubc.ca/> working on operating systems research. My advisor is Prof. Margo Seltzer <https://www.seltzer.com/margo>. In a past life, I have worked as a software engineer at Oracle and Arista Networks. My research is on General Purpose Isolation Mechanism in the OS. We ask whether we really need to have N different isolation mechanisms or whether instead, we could develop a framework in which all these different mechanisms represent points on a continuum. Here is a write-up <https://sid-agrawal.ca/#research-projects> with some more details. I am using seL4 as the microkernel base to build my research idea. At this stage, I am not looking in to the formal verification aspect of seL4, but that might change once I have a better idea about the type of mechanism I want to build. I would also like to keep the changes in the kernel to be minimum and try to demonstrate my ideas using user space processes. I have tried out the tutorials on the seL4 website. Currently, I am wading through the different helper libraries in seL4/seL4_libs <https://github.com/seL4/seL4_libs>. As someone who is just starting with seL4 ecosystem, I had a few high-level questions: - Are there are example OSes built with seL4, which would be a good place to look at? Specifically, I am looking for components such as basic versions of a process-server, vm-server, pager, file-systems server. - I came across refOS <https://github.com/seL4/refos>, but wasn't sure if it is still being maintained. - Another option was Genode <https://genode.org/documentation/general-overview/index>. This seemed to be maintained by another community and has many layers of abstractions since it supports multiple kernel backends. I am looking forward to engaging with this community, learning about seL4 and making meaningful contributions. Best, Sid sid-agrawal.ca

8 28

Sel4 rumprun has issues compiling
by Vortex 01 Aug '21

01 Aug '21

Hello, I would like to bring this issue to the attention of the community. Sel4’s fork of the rumprun unikernel no longer compiles. Due to the usage of Werror flag, the compiler produces repeated warnings which in turn creates errors. It seems like the rump kernel was tested on an older version of gcc and because it is older, raises warnings and causes the build to fail on newer compilers. This is a similar issue to https://github.com/rumpkernel/rumprun/issues/82 I have tested rumprun in the sel4 docker container. My build logs are also attached to this email. Thank you for taking attention to this issue. Sincerely, Ellis

3 3

Docker for ARM?
by dave＠synergy.org 27 Jul '21

27 Jul '21

I recently moved and my x86-64 machines are in storage. Are there docker images for Debian ARM/32 or Raspbian I can use to build seL4 on my Raspberry Pi? It is my target platform. Thanks, Dave

2 1

Camkes and native tcp/ip and networking
by Amirreza Zarraby 27 Jul '21

27 Jul '21

Hello seL4 team, I am try trying to use camkes to write a simple firewall. I am wondering if you can direct me to any existing camkes project which uses tcp/ip and network driver that I can look into as starting point. There is a seL4 based webserver but it seems to use vm and Linux. Thank you for your time. - Amir

4 3

Jetson AGX Xavier board porting
by bobding＠msn.com 27 Jul '21

27 Jul '21

Has anyone ported to Nvidia AGX Xavier board?

2 1

camkes-vm-examples-manifest cma34cr_centos fails
by christinefragoso＠protonmail.com 27 Jul '21

27 Jul '21

Hello, I'm trying to run the cma34cr_centos application from camkes-vm-examples-manifest, but I get this error: "Kernel entry via Unknown syscall, word: 65". I've set up VMware as described at https://docs.sel4.systems/Hardware/VMware/. In camkes-vm-examples-manifest/cma34cr_centos_x86_build, I've built the kernel: ../init-build.sh -DCAMKES_VM_APP=cma34cr_centos Then I ran these commands: ninja sudo ./seL4vmw.py images/kernel-x86_64-pc99 images/capdl-loader-image-x86_64-pc99 vmrun -T player start $HOME/vmware/seL4/seL4.vmx while :; do socat -d -d UNIX-CONNECT:/tmp/vsock,forever PTY,link=/tmp/mytty done After VMware boots, I ran minicom in a separate terminal to see the serial output: minicom -D /tmp/mytty Here is the full log: Welcome to minicom 2.7.1 OPTIONS: I18n Compiled on Dec 23 2019, 02:06:26. Port /tmp/mytty, 08:47:50 Press CTRL-A Z for help on special keys Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0xcf3000 end=0x3821bb8 size=0x2b2ebb8 name='' Parsing GRUB physical memory map Physical Memory Region from 0 size 9f800 type 1 Physical Memory Region from 9f800 size 800 type 2 Physical Memory Region from dc000 size 24000 type 2 Physical Memory Region from 100000 size bfde0000 type 1 Adding physical memory region 0x100000-0xbfee0000 Physical Memory Region from bfee0000 size 1f000 type 3 Physical Memory Region from bfeff000 size 1000 type 4 Physical Memory Region from bff00000 size 100000 type 1 Adding physical memory region 0xbff00000-0xc0000000 Physical Memory Region from f0000000 size 8000000 type 2 Physical Memory Region from fec00000 size 10000 type 2 Physical Memory Region from fee00000 size 1000 type 2 Physical Memory Region from fffe0000 size 20000 type 2 Physical Memory Region from 100000000 size 140000000 type 1 Adding physical memory region 0x100000000-0x240000000 Got VBE info in multiboot. Current video mode is 16703 ACPI: RSDP paddr=0xf6a00 ACPI: RSDP vaddr=0xf6a00 ACPI: RSDT paddr=0xbfeee733 ACPI: RSDT vaddr=0xbfeee733 Warning: Your kernel was not compiled for the current microarchitecture. Kernel loaded to: start=0x100000 end=0xc1f000 size=0xb1f000 entry=0x100300 ACPI: RSDT paddr=0xbfeee733 ACPI: RSDT vaddr=0xbfeee733 ACPI: FADT paddr=0xbfefef67 ACPI: FADT vaddr=0xbfefef67 ACPI: FADT flags=0x21 ACPI: 0 IOMMUs detected ACPI: MADT paddr=0xbfeee937 ACPI: MADT vaddr=0xbfeee937 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_APIC apic_id=0x2 ACPI: MADT_APIC apic_id=0x4 ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0x6 ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0x8 ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0xa ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0xc ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0xe ACPI: Not recording this APIC, only support 2 ACPI: MADT_IOAPIC ioapic_id=1 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x5 ACPI: 2 CPU(s) detected ELF-loading userland images from boot modules: size=0x3fab000 v_entry=0x408828 v_start=0x400000 v_end=0x43ab000 p_start=0x3822000 p_end=0x77cd000 Moving loaded userland images to final location: from=0x3822000 to=0xc1f000 size=0x3fab000 Starting node #0 with APIC ID 0 Mapping kernel window is done Starting node #1 with APIC ID 2 Booting all finished, dropped to user space create_object@main.c:673 [Cond failed: err != seL4_NoError] Failed to find device frame/untyped at paddr = 0xb0000000 seL4 root server abort()ed Debug halt syscall from user thread 0xffffff823e027400 "rootserver" halting... Kernel entry via Unknown syscall, word: 65 Any idea what's wrong? I just want to get one x86 application with cross VM connectors working. The other x86 applications (optiplex9020, cma34cr_ubuntu, zmq_samples) in camkes-vm-examples-manifest don't work for other reasons.

2 1

Formally verified AES C code
by Hugo V.C. 20 Jul '21

20 Jul '21

Hi all, I don't want to use SSL/openssl in a project I'm working. Thus, I want to just use my own encryption at the app layer. As performance is not a problem (just very small data packets over a socket) I would like to have the most simple implementation possible of AES, preferably, formally verified. Is anyone aware of any public AES encrytion implementation in C that has been formally or semi-formally verified? Thank you!

5 10

Cannot reserve memory for camkes VM guest
by Alex Ling 17 Jul '21

17 Jul '21

Hi All, I'm trying to bring up camkes VM Linux guest on Firefly RK3399 board which is with a GICv3 ARMv8. I'm using the "rockpro64" target and my work is based on [1] and [2]. When I run the "capdl-loader-image-arm-rockpro64", there's error "Range not available at 0xfef10000, size 0x10000". Bootstrapping kernel Booting all finished, dropped to user space Undelivered IRQ: 132 Install gic v3 sel4utils_reserve_range_at_no_alloc@vspace.c:595 Range not available at 0xfef10000, size 0x10000 vm_reserve_memory_at@guest_memory.c:328 Failed to allocate vm reservation: Unable to create vspace reservation at address 0xfef10000 of size 65536 vm_install_vgic_v3@vgic_v3.c:87 Error installing vgic Assertion failed: !err (/mnt/data3/projects/rk3399/build/seL4/camkes-vm-app/projects/vm/components/VM_Arm/src/main.c: main_continued: 1098) Here's my projects/seL4_projects_libs/libsel4vmmplatsupport/plat_include/rockpro64/sel4vmmplatsupport/plat/devices.h content: #define GIC_VERSION_3 #define GIC_PADDR 0xfee00000 #define GIC_DIST_PADDR (GIC_PADDR + 0x00000000) #define GIC_DIST_SIZE 0x10000 #define GIC_REDIST_PADDR 0xfef00000 #define GIC_REDIST_SIZE 0xC0000 #define GIC_REDIST_SGI_PADDR (GIC_REDIST_PADDR + 0x00010000) #define GIC_REDIST_SGI_SIZE 0x10000 I think the problem is related to GIC_REDIST_SIZE. I set it to 0xC0000 according to the rockpro64 device tree file in kernel/tools/dts/rockpro64.dts interrupt-controller@fee00000 { compatible = "arm,gic-v3"; #interrupt-cells = < 0x04 >; #address-cells = < 0x02 >; #size-cells = < 0x02 >; ranges; interrupt-controller; reg = < 0x00 0xfee00000 0x00 0x10000 0x00 0xfef00000 0x00 0xc0000 0x00 0xfff00000 0x00 0x10000 0x00 0xfff10000 0x00 0x10000 0x00 0xfff20000 0x00 0x10000 >; interrupts = < 0x01 0x09 0x04 0x00 >; phandle = < 0x01 >; I tried to reduce it to 0x10000 and it can boot to VM guest but the guest Linux will fail in gic_iterate_rdists() because it cannot read from GIC's GICR_TYPER register correctly. Did I miss anything? Any suggestion is highly appreciated. Thank you very much! [1] https://github.com/seL4/seL4/pull/378 [2] https://github.com/seL4/seL4_projects_libs/tree/sylvain/gicv3 Regards, Alex

2 2

Passing caps through CAmkES procedures?
by Austin Appleby 14 Jul '21

14 Jul '21

Hi, I've got what seems like a simple task that I can't quite figure out how to implement - I am sketching out a key-value-store component where the "values" can be quite large (tens or hundreds of K). I would like clients of the component to pass caps to their own buffers in and out of this component's API to minimize copying and temporary buffer allocation and ensure that multiple clients can't see each other's data. In plain seL4 this would be done via the client passing a cap in its seL4_Call(), but I don't see an equivalent for this in CAmkES. Is there a way of declaring this in the .camkes syntax? If not, is there a way to build this component outside of CAmkES and still allow it to interact with existing CAmkES components? -Austin Appleby @ Google

1 0

CI infrastructure outage
by Peter Chubb 09 Jul '21

09 Jul '21

Hi Folks, Our continuous integration testing infrastructure is being relocated from CSIRO to UNSW premises this weekend. Because Sydney is in COVID lockdown, and because we're reworking the system not to rely on commercial software we no longer have a licence for (Atlassian Bamboo), we will probably not have everything working again for two or three weeks. The upshot for you is that any pull request that needs extensive testing will not be merged for at least two weeks, possibly longer. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW

1 0

gic v2 vs gic v3
by Chris Koziarz 09 Jul '21

09 Jul '21

Hi all, I'm trying to port camkes-arm-vm to a different platform, that supports gic-v3 In the process, I hit a compilation error: Building C object kernel/CMakeFiles/kernel_all_pp_...rapper_temp_lib.dir/ kernel_all_pp_prune_wrapper_temp.c.obj FAILED: kernel/kernel_all_pp_prune_wrapper_temp.c In file included from /home/chris/camkes-tqma8xqp- vm/kernel/src/arch/arm/object/vcpu.c:15: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v2.h:23: error: "IRQ_MASK" redefined [-Werror] 23 #define IRQ_MASK MASK(10u) In file included from kernel/gen_headers/plat/platform_gen.h:23, from /home/chris/camkes-tqma8xqp-vm/kernel/include/plat/ default/plat/machine.h:8, from /home/chris/camkes-tqma8xqp- vm/kernel/include/machine.h:9, from /home/chris/camkes-tqma8xqp- vm/kernel/include/api/syscall.h:10, from /home/chris/camkes-tqma8xqp- vm/kernel/src/api/faults.c:10: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v3.h:30: note: this is the location of the previous definition 30 #define IRQ_MASK MASK(16u) which is an indicative that both gic_v3.h & gic_v2.h headers have been included, which is an error because said headers are not compatible: kernel/include/arch/arm/arch/machine/gic_v3.h:#define IRQ_MASK MASK(16u) kernel/include/arch/arm/arch/machine/gic_v2.h:#define IRQ_MASK MASK(10u) So my question is: how can I configure the build to avoid such a conflict? I can grepp the relevant configuration option in CMakeCache.txt: build_tqma8/CMakeCache.txt:CONFIGURE_INTERRUPT_CONTROLLER:INTERNAL=arch/machine/gic_v3.h but cannot see it in ccmake gui because it's "INTERNAL" What is the solution? - replace this option somehow to use gic_v2 and have my HW use gic v.2, or - change compilation options to use gic_v3 everywhere Thanks for any help, Chris.

4 5

Re: gic v2 vs gic v3
by Alex Ling 凌云 08 Jul '21

08 Jul '21

Hi All, What is the status of virtualization support on ARM SOCs with GICv3? According to section “FAQ and Implementation Notes” of [1], seems it is still under development. Any plan or progress on this? Thank you very much. [1] https://docs.sel4.systems/projects/camkes-arm-vm/ Regards, Alex

1 0

Re: Tutorial Problem
by Kent Mcleod 08 Jul '21

08 Jul '21

On Wed, Jun 30, 2021 at 11:53 AM Michael Neises <neisesmichael(a)gmail.com> wrote: > > Kent, > > > > I tried using those extra arguments and got the same error regarding kvm I reported a few minutes ago: > > > > ./simulate: qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,+syscall,+lm,enforce,+vmx -nographic -serial mon:stdio -m size=2G -enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 Could not access KVM kernel module: No such file or directory > > qemu-system-x86_64: failed to initialize KVM: No such file or directory > There are instructions on how to setup KVM and nested virtualization on the tutorial that I've pasted here: "Note if you are using QEMU it is important to ensure that your host machine has VT-x support and KVM (https://www.linux-kvm.org/page/Main_Page) installed. You also need to ensure you have enabled nested virtulisation with KVM guests as described here (https://www.linux-kvm.org/page/Nested_Guests)" A quick way to check if nested virtualization is enabled (and therefore supported) on your host is to run `cat /sys/module/kvm_intel/parameters/nested`. `Y` should be returned if it's enabled. It may be easier to run the image on an actual machine instead of in qemu. The images produced can be loaded by a multiboot loader such as grub or pxelinux. (https://docs.sel4.systems/Hardware/VMware/#add-grub2-option-to-run-sel4) has an example grub config.

4 7