- Devel - lists.sel4.systems

The seL4 Microkit tutorial is now available
by Ivan Velickovic 04 Oct '23

04 Oct '23

Hello everyone, For those who are new to seL4 or want to learn about the seL4 Microkit, the Microkit tutorial is now available to everyone on the Trustworthy Systems website: https://trustworthy.systems/projects/microkit/tutorial/welcome.html. This is the same tutorial that ran at this year’s seL4 Summit. The tutorial code and infrastructure is also open-source, available here https://github.com/au-ts/microkit_tutorial. Feel free to provide feedback or ask questions there. Thanks, Ivan

1 0

Re: [oss-security] Xen Security Advisory 439 v1 (CVE-2023-20588) - x86/AMD: Divide speculative information leak
by Solar Designer 03 Oct '23

03 Oct '23

On Tue, Sep 26, 2023 at 09:59:19PM -0400, Demi Marie Obenour wrote: > These detailed security advisories are one of the things I love about > Xen. It's hard to trust a hypervisor (KVM) that will not issue them, > for then one has no way to know if a particular problem got fixed. I concur. I'd appreciate security advisories from the KVM project. > I'm CCing KVM here to make sure they have a fix. From their Git commit > history, I am almost certain that seL4 does not. I'm CCing the seL4 > developers to alert them of this and suggest that the x86 port be > removed or at least have a big warning. I strongly oppose removal of a port/support for a certain architecture just because some implementations of it are/were problematic. Adding a warning is fine. Alexander P.S. Demi Marie, please note that oss-security list content guidelines explicitly discourage CC'ing other lists(*), and Xen advisories are already stretching this. In this reply, I am still CC'ing many of what you had CC'ed as I am following up on your specific points relevant to those lists, but in general let's be more careful about this. (*) Because we may then get off-topic follow-ups from there, especially if CC'ing project user lists or high-volume lists like LKML. In this specific case, we're lucky so far.

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 02 Oct '23

02 Oct '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Oct 4, 8am For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Add GICv3 emulation support for vmm on arm platform
by colorglass4＠outlook.com 27 Sep '23

27 Sep '23

Hi, I am trying to run a guest Linux using seL4's vmm library on the rk3568 platform, which uses gicv3 as its irq controller. But there is only gicv2 emulation officially supported in the vm library. I did find that there are 2 "gicv3" branch of the repository, but they are all outdated and have not being maintained for a long time. Is there any plan to formally add the gicv3 support to vmm library? Thanks.

2 3

Sel4 VMM on zcu102
by An,Jianjun 26 Sep '23

26 Sep '23

Hi I have run sel4 on the development board of zcu102. I found on the official website that the camkes-vm project does not support the platform zcu102. Could you please give me some guidance to make the functions of this vmm run and run a linux on the guest. Thanks

2 4

Bug on sel4 rootserver?
by chenpingyuan＠xiaomi.com 12 Sep '23

12 Sep '23

Hello guys, I'm trying to run sel4 using qemu under macosx, but it looks crash happened(Same steps were done on Ubuntu, but nothing bad happened.). More info: I'm following the doc here with docker as the build environment: https://docs.sel4.systems/GettingStarted.html Any tips are appreciated. Logs: chenpingyuan@in-container:/host/sel4_arm64/build_aarch64$ ./simulate ./simulate: QEMU command: qemu-system-aarch64 -machine virt -cpu cortex-a53 -nographic -m size=2G -kernel images/sel4test-driver-image-arm-qemu-arm-virt Not in hyp mode, cannot reset CNTVOFF_EL2 ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[40a27000..40eed0b7] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 40b61eb8. Loaded DTB from 40b61eb8. paddr=[4023d000..4023efff] ELF-loading image 'kernel' to 40000000 paddr=[40000000..4023cfff] vaddr=[ffffff8040000000..ffffff804023cfff] virt_entry=ffffff8040000000 ELF-loading image 'sel4test-driver' to 4023f000 paddr=[4023f000..40634fff] vaddr=[400000..7f5fff] virt_entry=40e568 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. available phys memory regions: 1 [40000000..80000000] reserved virt address space regions: 3 [ffffff8040000000..ffffff804023d000] [ffffff804023d000..ffffff804023ed11] [ffffff804023f000..ffffff8040635000] Booting all finished, dropped to user space Caught cap fault in send phase at address 0 while trying to handle: unknown syscall 0x476dcc in thread 0xffffff807ffca400 "rootserver" at address 0x460964 With stack: 0x6e3ca0: 0x466a53 0x6e3ca8: 0x460b84 0x6e3cb0: 0x457474 0x6e3cb8: 0x0 0x6e3cc0: 0x6e3f30 0x6e3cc8: 0x0 0x6e3cd0: 0x0 0x6e3cd8: 0x4433f0 0x6e3ce0: 0x0 0x6e3ce8: 0x0 0x6e3cf0: 0x0 0x6e3cf8: 0x0 0x6e3d00: 0x0 0x6e3d08: 0x0 0x6e3d10: 0x0 0x6e3d18: 0x0

2 2

2 weeks left before the seL4 summit; there's still time to register
by June Andronick (seL4 Foundation) 05 Sep '23

05 Sep '23

The seL4 summit 2023 will start in 2 weeks in Minneapolis! There is still time to register if you haven’t done it yet. Summit: https://sel4.systems/Foundation/Summit/2023/ Register: https://events.linuxfoundation.org/sel4-summit/register/ Program: https://sel4summit2023.sched.com/ See you there!

1 0

next seL4 TSC meeting on Tue 12 Sep (Mon 11 Sep in US)
by Gerwin Klein 04 Sep '23

04 Sep '23

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Tue, 12 Sep, 4pm - Central Europe: Tue, 12 Sep, 8am - US West Coast (LA/SF): Mon, 11 Sep, 11pm See also the seL4 calendar feed available from here: https://sel4.systems/contact/home.pml The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/85916669769 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: - action items form last meeting - discuss and vote on RFC-5 (The seL4 Core Platform) - discuss and vote on adding the seL4 Rust support repositories currently at https://github.com/coliasgroup/rust-seL4 to the seL4 GitHub org. - discuss steps for the next seL4 release - if there is time: discuss remaining open RFCs 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

Reminder seL4 developer hangout
by Birgit Brecknell 04 Sep '23

04 Sep '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Sep 6, 8am For your time zone, please see the calendar: https://sel4.systems/contact/ 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 2pm-5pm Fri 9am-5pm

1 0

Standalone experiments
by sean bruno 01 Sep '23

01 Sep '23

I'm investigating some of the different microkernels out there for some graduate exploration. The tutorials were awesome and got me bootstrapped *very* quickly, thank you for the effort on those. I am attempting to build a "hello-world" on my own and seem to be missing a step as base.cmake no longer can see the musllibc that I have in my tree. I'm fairly certain my CMake knowledge here is weak or I just flat out missed a step. My checkout tree looks like the following: $ tree -L 1 ├── build ├── CMakeLists.txt -> tools/cmake-tool/default-CMakeLists.txt ├── init-build.sh -> tools/cmake-tool/init-build.sh ├── kernel ├── projects ├── README.md └── tools $ tree -L 1 projects/ projects/ ├── hello-world ├── musllibc ├── seL4_libs └── util_libs When cmake runs from build, I see the following: ~/build]$ cmake -DCROSS_COMPILER_PREFIX=aarch64-linux-gnu- -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -C ../kernel/configs/AARCH64_verified.cmake ../projects/hello-world/ loading initial cache file ../kernel/configs/AARCH64_verified.cmake -- The C compiler identification is GNU 12.1.1 -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Check for working C compiler: /usr/lib64/ccache/aarch64-linux-gnu-gcc - skipped -- Detecting C compile features -- Detecting C compile features - done -- The CXX compiler identification is GNU 12.1.1 -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Check for working CXX compiler: /usr/lib64/ccache/aarch64-linux-gnu-g++ - skipped -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /usr/lib64/ccache/aarch64-linux-gnu-gcc -- /home/sbruno/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating from DTB... WARNING:root:Only mapping 4096/16777216 bytes from node /iommu@12000000, region 0. Set kernel_size in YAML to silence. -- CPIO test cpio_reproducible_flag PASSED CMake Error at /home/sbruno/tools/cmake-tool/base.cmake:55 (find_package): By not providing "Findmusllibc.cmake" in CMAKE_MODULE_PATH this project has asked CMake to find a package configuration file provided by "musllibc", but CMake did not find one. Could not find a package configuration file provided by "musllibc" with any of the following names: musllibcConfig.cmake musllibc-config.cmake Add the installation prefix of "musllibc" to CMAKE_PREFIX_PATH or set "musllibc_DIR" to a directory containing one of the above files. If "musllibc" provides a separate development package or SDK, be sure it has been installed. Call Stack (most recent call first): CMakeLists.txt:4 (include) -- Configuring incomplete, errors occurred!

2 1