January 2022 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 29 Jan '25

29 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 15 Oct '24

15 Oct '24

Hi seL4 Dev team, Can someone explain the reason (share the reference) to invalidate the local TLB during kernel vspace activation as part CPU initialisation. The Tx2 board stuck while performing this operation. As per my understanding both Tx1 and Tx2 are using same A57 core. so the TLB initialisation and invalidation remain same for Tx2 and should not stuck during invalidation.Please correct me if anything wrong here. I understand from that instruction (tlbi vmalle1) which is invalidating stage 1 entries associated to the current VMID. Also from arm mmu code the seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as 16bit and page table setup 4k granular size. I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the state of processor but its throwing synchronous exception. Do we have any other option to dump all the register content to see the state of processor like we have one in 'sel4debug_dump_registers' which is used in sel4test code. Regards, Muneeswaran R

3 4

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

18 May '23

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

5 4

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 杨竣轶 29 Jan '22

29 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 27 Jan '22

27 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 26 Jan '22

26 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 24 Jan '22

24 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