- Devel - lists.sel4.systems

Only 512mb ram available on capdl-loader-image-arm-qemu-arm-virt image
by skydivebcn＠gmail.com 24 Mar '24

24 Mar '24

Hi! I'm running a an aarch64 Linux guest with qemu with "qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -m size=2048 (...) -kernel capdl-loader-image-arm-qemu-arm-virt". I have noticed that no matter how I set the "-m size" parameter that only 512MB are available to the Linux guest. Removing the "highmem=off" crashes the system. Ok, what is the fastest, easiest way to get a workaround to this (if possible)? and have much more RAM available to Linux guest? Best,

2 1

next seL4 TSC meeting on Fri 22 Mar
by Gerwin Klein 19 Mar '24

19 Mar '24

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Fri, 22 Mar, 6pm - Central Europe: Fri, 22 Mar, 8am - US West Coast (LA/SF): Fri, 22 Mar, 0:00h 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/83417411537 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 from last meeting - RFC-17: IPI API - RFC-16: PMU (for discussion/feedback, not enough detail yet to vote) - RFC-15: Morello (for discussion/feedback, not enough detail yet to vote) - RFC-14: MCS budget limit thresholds — status? - should we remove deprecated sel4lib functions to enable verification? - steps for next seL4 release - discussion if there is time: - use GitHub discussions instead of discourse? (i.e. retire discourse?) - use GitHub for RFC process? (i.e. retire/archive JIRA?) 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 _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems

1 0

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