- Devel - lists.sel4.systems

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

15 Jun '22

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

3 2

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

14 Jun '22

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

2 2

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

14 Jun '22

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

1 1

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

14 Jun '22

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

3 3

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

14 Jun '22

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

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 10 Jun '22

10 Jun '22

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

1 0

sel4 on bare-metal | Questions and comments
by Sid Agrawal 10 Jun '22

10 Jun '22

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

2 5

Implementation of SeL4
by Sriram 09 Jun '22

09 Jun '22

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

3 2

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

03 Jun '22

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

3 4

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

01 Jun '22

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

1 0