- Devel - lists.sel4.systems

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 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

root task executable memory changed
by Leonid Meyerovich 08 Feb '24

08 Feb '24

Hello, I have a seL4 project that creates a number of processes with multiple threads. An application works fine. Every process periodically calculates the checksum of the executable segment and the system (Monitor process) keeps track that these values should be the same over the time. Some time when I change (add) some code in amu process I have an error that Monitor process prints CHECKSUM ERROR -------- Someone modified executable memory process=Startup 0x400000 8868997 last->10daf436f961b809 this->95ebd3119aee7736!!!! It always complains about the root (Startup) task. Checksum value changes every time the Startup process calculates it. The code that calculate executable segment are: typedef struct { unsigned char e_ident[EI_NIDENT]; /* Magic number and other info */ Elf64_Half e_type; /* Object file type */ Elf64_Half e_machine; /* Architecture */ Elf64_Word e_version; /* Object file version */ Elf64_Addr e_entry; /* Entry point virtual address */ Elf64_Off e_phoff; /* Program header table file offset */ Elf64_Off e_shoff; /* Section header table file offset */ Elf64_Word e_flags; /* Processor-specific flags */ Elf64_Half e_ehsize; /* ELF header size in bytes */ Elf64_Half e_phentsize; /* Program header table entry size */ Elf64_Half e_phnum; /* Program header table entry count */ Elf64_Half e_shentsize; /* Section header table entry size */ Elf64_Half e_shnum; /* Section header table entry count */ Elf64_Half e_shstrndx; /* Section header string table index */ } Elf64_Ehdr; extern char __executable_start[]; // function returns executable segment start address and size int initStartupElfSegsParams(Elf64_Ehdr *pELFHeader, uintptr_t *startAddr, uintptr_t *size) { seL4_Word phoff = pELFHeader->e_phoff; Elf_Phdr *currentPH = (Elf_Phdr *)((void *)pELFHeader + phoff); for (int i=0; i<pELFHeader->e_phnum; i++) { ZF_LOGD("ELF: p_type=%x p_flags=%x p_vaddr=%p p_memsz=%lu", currentPH[i].p_type, currentPH[i].p_flags, (void *)currentPH[i].p_vaddr, currentPH[i].p_memsz); if ( ((currentPH[i].p_type & 1) == 1) && ((currentPH[i].p_flags & 1) == 1)) // p_flags & 1 == 1 - executable { *startAddr = (uintptr_t)currentPH[i].p_vaddr; *size = (uintptr_t)currentPH[i].p_memsz / sizeof(uint64_t); return 0; } } return -1; }; initStartupElfSegsParams((Elf64_Ehdr *)__executable_start, &proc_validate_params[STARTUP_INDEX].p_addr, &proc_validate_params[STARTUP_INDEX].p_size); Any help will be appreciated. Thanks

2 6

Reminder seL4 developer hangout
by Birgit Brecknell 05 Feb '24

05 Feb '24

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

fault processing
by Leonid Meyerovich 26 Jan '24

26 Jan '24

I am working on fault processing. When I am a fault I am calling void sel4utils_print_fault_message(seL4_MessageInfo_t tag, const char *thread_name) from sel4libsutils library I have tested it for "page fault" condition and it works fine - I am getting seL4_Fault_VMFault fault type But in certain case I have got seL4_Fault_VCPUFault type, which is not implemented sel4libsutils library I try to process this fault similar to seL4_Fault_VMFault to get all neccessary registers, but the kernel does not have functions like seL4_Fault_VCPUFault_get_IP. What is the message format for VCPU fault? Thanks

2 3