- Devel - lists.sel4.systems

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

23 Jun '22

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

2 1

SeL4 Tutorial - Camkes CrossVM
by Sriram 22 Jun '22

22 Jun '22

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

1 0

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

22 Jun '22

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

2 1

SeL4 Source Code Documentation
by Sriram 20 Jun '22

20 Jun '22

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

2 2

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

20 Jun '22

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

3 2

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

16 Jun '22

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

3 5

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

16 Jun '22

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

2 1

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

15 Jun '22

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

3 2

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

15 Jun '22

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

2 2

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

15 Jun '22

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

1 1