Devel

devel@sel4.systems

19 participants
1383 discussions

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

15 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 09 Mar '24

09 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 09 Mar '24

09 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 04 Mar '24

04 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 19 Feb '24

19 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

SeL4 Question: Implementation of encrypted file types
by info＠wolffgames.com 12 Feb '24

12 Feb '24

Greetings SeL4 Development, My name is Marc Wolff, currently located in Portland, Oregon, USA. I'm CEO of Leyline Nexus, an R&D team primarily for game development, but also some other things. I have an implementation question for the SeL4 microkernel, and I was hoping you could point me in the right direction. Unfortunately I'm not a computer scientist and my knowledge is both self-taught and currently very limited. Right now we're focused on tabletop games, but our next development target is video games and hardware development. I see based on what I can understand from the whitesheet that SeL4 can hypervise, but I'm wondering about an idea to fully secure it on the hardware side, essentially solving one its primarily vulnerabilities. The basic idea starts with a modified risc-based CPU architecture on an FPGA (since x86 is compromised) for testing. This includes a microcode-embedded SeL4 mk with an added feature for encrypting a NEW SYSTEM of FILE TYPES. Here, all files types become a system-specific encrypted file type which presents a virtual (more common) file type externally for readability, e.g. ".doc" or ".exe". I suppose this would be at -0 privilage, since it happens in microcode and the processs would not be accessible through ASM instructions, except through dedicated query ports and flag registers. The result is that the system comes up with its own hidden and encrypted name, for example, for the .exe file type. I guess it could do this for any arbitrary file name, so long as its source code could be validated by the hyperviser (possibly modified?; it would have to do this both at runtime when executing code and when compiling). When compiling files, if the microkernel discovers exploits in the code (invalid requests, etc.), then it can simply compile it as the standard file type that could run on other systems (.exe) but not on this system - since this system only reads its own encrypted file types. If there's an existing standard output for invalid programs in SeL4 then this could modify that or be added to it for certain cases. I suppose this would entirely depend on the quality of encryption, save for reverse-engineering through decapping or something, but it seems like a potential solution for fully separating virtual memory from runtime execution. I definitely DO NOT know what I'm talking about, but from my perspective this seemed like a great way to implement copyright protection on game hardware SOC's. Maybe on the FPGA you could even do a sub-GPU within a microkernel core that was dedicated to encrypting? Maybe someone has already thought of all this before? If yes, we'd be very interested to know - as it could save us a lot of time and headaches... Best regards, Marc Marc Wolff Email: info(a)wolffgames.com Phone: 530.210.4811

3 4

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel