- Devel - lists.sel4.systems

Reminder seL4 developer hangout
by Birgit Brecknell 17 Mar '24

17 Mar '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Tue Mar 19, 9pm UTC 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

Re: DIFFICULTY RUNNING SEL4TEST ON RASPBERRY PI 4 REV 1.5 4GB
by Peter Chubb 14 Mar '24

14 Mar '24

>>>>> "Mario" == Mario CUSANO <mario.cusano(a)rina.org> writes: Mario> I hope this email finds you well. I am reaching out to seek Mario> assistance regarding running sel4test on a Raspberry Pi 4 Mario> Rev1.5 4GB. seL4 is only supported at the moment on the Raspberry Pi 4B with a BCM2711. Each build of seL4 is specific to a particular SoC. The Rev 1.5 has a different SoC. I don't know if anyone has done the work to port seL4 to the Rev 1.5 Pi4, which (I think) uses a BCM2835. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

2 1

How would you approach supporting a new processor architecture?
by Isaac Beckett 09 Mar '24

09 Mar '24

Hello! I’m writing to ask how someone would approach porting seL4 to a new CPU architecture. For example, ppc64le/IBM Power, since those systems can be run with limited or no black box firmware blobs, they could offer stronger security under seL4 since you can audit or replace the platform firmware in many cases. There’s even an OEM manufacturing Power9 systems with this in mind. That said, I know supporting a new architecture is not trivial. New platform code would have to be written and verified, and existing userspace code for Arm and x86-64 may have to be adjusted. How does one approach something like this? Is it feasible for someone less familiar with seL4’s internals to get something quick and dirty running as a proof of concept?

2 2

question about booting camkes Arm VMM on TX1 from SD card
by PX 08 Mar '24

08 Mar '24

Hi, all, I tried to boot the camkes arm vmm on TX1 from a SD Card, but failed. I just follow the instructions at https://github.com/seL4/camkes-vm-examples/blob/master/README.md, and do nothing new. I build the vmm image using the "../init-build.sh -DAARCH64=YES -DCAMKES_VM_APP=minimal DPLATFORM=tx1", I got the image, capdl-loader-image-arm-tx1, and copied it to a SD card. I believe this image is a binary image. On the TX1 board, I try to load it using the u-boot command: 1.mmc dev 1 2.fatload mmc 1 0x80000000 capdl-loader-image-arm-tx1 3.go 0x80000000 However, I cannot boot the guest VM. seL4 failed assertion "cap_get_capType(destSlot->cap)==cap_null_cap" Did I miss something here? Did I set the wrong load address for Tx1? Thanks,

1 0

RISC-V Page Tables for SV39
by Jeff 08 Mar '24

08 Mar '24

Hello, I am trying to understand how the seL4_RISCV_PageTable_Map function works when working with SV39, where we have 3 page tables. The RISCV implementation doesn't have the advantage of the separate levels, so for all the page tables, we can only use the same function. However, based on the description, there are a few questions that I have: *Description:* Starting from the VSpace, map the page table object at any unpopulated level for the provided virtual address. If all paging structures and mappings are present for this virtual address, return an seL4_DeleteFirst error. It says it maps the page table object at *any unpopulated *level for the provided virtual address. What does that necessarily mean? When you attempt to map the pages, how do you differentiate between the different levels? Is it just based on the vaddr or do you have to point the vspace to one of the lower level pages? Or does vspace have to be the root page table? Thanks, Jeff

2 1

Reminder seL4 developer hangout
by Birgit Brecknell 03 Mar '24

03 Mar '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Mar 6, 7am UTC 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

RISC-V Simulation Support
by Jeffery Lim 26 Feb '24

26 Feb '24

Hello, What does the Simulation column mean in the RISC-V table in https://docs.sel4.systems/Hardware/? Does it mean that spike is the only supported platform to run qemu simulations? All the other platforms can only be run on hardware? Thanks, Jeff

2 1

interested in participating in a survey on seL4 website and docsite structure next week?
by June Andronick (seL4 Foundation) 19 Feb '24

19 Feb '24

Hi, We are working on improvements to the seL4 website (https://sel4.systems/) and docsite (https://docs.sel4.systems/) Next week, we will conducting a survey (over a week) to gather feedback on the website and docsite structures. If you’re interested in participating, please email me at june(a)sel4.systems Thanks June

5 5

Reminder seL4 developer hangout
by Birgit Brecknell 18 Feb '24

18 Feb '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * UTC: Tue, 20 Feb, 9pm 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

new RFCs
by Gerwin Klein 13 Feb '24

13 Feb '24

I would like to draw your attention to two new RFCs that have been proposed for discussion and later decision by the technical steering committee: RFC-17: seL4 multikernel IPI (Inter-Processor Interrupt) API https://sel4.atlassian.net/browse/RFC-17 RFC-16: Add new capability for the PMU (Performance Management Unit) https://sel4.atlassian.net/browse/RFC-16 Please comment and give feedback if you have any. The slightly older RFC-15 and RFC-14 that may benefit from further discussion (type RFC-15 or RFC-14 into the search field at the top of the page on https://sel4.atlassian.net/) Cheers, Gerwin

1 0