- Devel - lists.sel4.systems

Re: Modifying the root user thread's CSpace
by Indan Zupancic 16 Nov '24

16 Nov '24

Hi Ben, (Please don't drop CC.) Glad I could help. Don't be too hard on yourself, hindsight is easy. For defensive programming reasons (which also makes attacks harder), it's good to have a non-zero guard for your caps which doesn't overlap with your virtual address space, at least for the first level. For the last level it depends on how you want overflows to behave: If you want to seamlessly continue into the next CNode, have a zero guard size (good for e.g. dynamic CNode allocation). If you want to detect overflow errors on sets of caps, make sure you have a guard size of at least 1 bit. Having a non-zero guard value has less advantage for later CNode levels. Greetings, Indan On 2024-11-15 16:25, Ben McCart wrote: > Indan, > > Thank you so much! seL4_CNode_Mint instead of seL4_CNode_Copy solved > my problem. The piece I was missing was that I needed to change the > guard on the original seL4_CapInitThreadCNode when copying it into the > first CSlot of the new root CNode. (Doh!) I should have caught that > as you said explicitly in you prior response that each CNode capability > can have different guard bits set. (I just didn't think carefully > enough about that.) > > On 11/15/2024 4:55 AM, Indan Zupancic wrote: >> >> seL4_CNode_Copy can't change the guard, you have to use >> seL4_CNode_Mint() if you need to change it: >> >> assert(bi->initThreadCNodeSizeBits <= 16); >> seL4_CNode_Mint( >> cspace_cap, >> 0, // Destination index in the >> new Cap table. >> 16, // Number of bits for the new >> Cap table. >> seL4_CapInitThreadCNode, >> seL4_CapInitThreadCNode, >> seL4_WordBits, >> seL4_AllRights, >> 16 - bi->initThreadCNodeSizeBits); // Zero pad guard to reach 16 >> bits. >> <SNIP> >> Indan > > -Ben

1 0

Modifying the root user thread's CSpace
by Ben McCart 16 Nov '24

16 Nov '24

Hello, I read the manual for v12.0 chapters 1-3, and 10. I have been attempting to experiment with CSpaces for the user space root thread. I am trying to modify the CSpace to support multiple CNode levels by changing the guard from all zero bits above the radix (16 bits of radix on PC99 x64), to support multiple CNode levels. I have been using seL4_TCB_SetSpace to modify the CSpace for seL4_CapInitThreadTCB. The result is seL4_NoError and once I make this call the previously working capabilities tutorial quits working as expected. (Calls taking the original seL4_CapInitThreadTCB value are now returning seL4_InvalidCapability). I have studied chapter three of the manual and I think I understand how the CSpace addressing works in depth. What I can't seem to figure out is how to construct a cspace_root_data argument for the call to seL4_TCB_SetSpace for the number of guard bits and the guard values I want to use. For example, if I wanted two levels each with a 4 bit guard and a 16 bit radix how would I construct cspace_root_data argument for a gaurd value of 0x0? And for a gaurd value of 0xF? (I intend to keep the original seL4_CapInitThreadTCB CNode as my level-1 CNode for this experimentation.) Thank you in advance if you can point me to some reference documentation that may cover how to construct the cspace_root_data argument, guidance, or direction you may be able to give. Sincerely, Ben McCart

3 6

Potential vulnerabilities
by Hugo V.C. 15 Nov '24

15 Nov '24

I'm forwarding this question here (tried on Mattermost Trustworthy Systems group first) hoping someone can put some light on this? --- Hi, I'm having a look to the vulns (in areas of the kernel that have not been formally verified) patched in seL4 13.0.0. We have: 1) "NULL pointer dereference when injecting an IRQ for a non-associated VCPU on SMP configurations." 2) "On AArch64, when seL4 runs in EL1 the kernel would fault with a data abort in seL4_ARM_Page_Invalidate_Data and seL4_ARM_VSpace_Invalidate_Data when the user requested a dc ivac cache maintenance operation on a page that is not mapped writeable." Extremely simple question: running version < 13.0.0 on top of Qemu (in example like https://docs.sel4.systems/projects/sel4webserver/) would it be vulnerable to any of those? --- Best,

4 13

seL4 developer hangout reminder
by Birgit Brecknell 11 Nov '24

11 Nov '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 13 Nov, 7:00am UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

ci-actions/preprocess
by Yanfeng 07 Nov '24

07 Nov '24

Dear experts, I am seL4 newbie. When I changed compile options in seL4/CMakeLists.txt, I got check errors from "ci-actions/preprocess" check like this one: https://github.com/seL4/seL4/actions/runs/11682457028/job/32529623251 Can someone teach where I can see details of "ci-actions/preprocess" check? Regards, yf

2 2

Introduction to seL4's Architecture & Concepts
by tunacici7＠gmail.com 03 Nov '24

03 Nov '24

Hey everyone. I've created an introductory documentation to seL4’s architecture & concepts. I thought it would be helpful for anyone interested in seL4 and wanted to share. The documentation includes many hand-written visualizations to make seL4 (and its abstractions) more accessible to people. You can access it on GitHub: https://github.com/TunaCici/seL4_Architecture Hope you enjoy it! NOTE: I’m sorry if this isn’t the best place to share this. I don’t know of any other active seL4 communities besides the mailing list.

6 6

AMD64 - how much virtual address space does the kernel map?
by Ben McCart 31 Oct '24

31 Oct '24

Hellow all, I have been working through the tutorials and doing some experimenting and ran into behavior that very much surprised me. I can seL4_X86_PageTable_Map & seL4_X86_Page_Map to virtual addresses starting at the 96 MB address (0x06000000) with no errors. However, as soon as I try to seL4_X86_PageDirectory_Map that same virtual address I get the error seL4_DeleteFirst. I didn't think the kernel mapped anything for the root address above 64 MB virtual address range for the root address in these tutorials. If it did I would have expected an error for seL4_X86_PageTable_Map & seL4_X86_Page_Map. What is going on? What am I missing? How can I avoid expecting to map a virtual address in a range already mapped by the kernel for the root process on a given architecture? - Ben McCart

2 1

seL4 fails to boot multiple core at CPU 0x1.
by Vishal Gupta 31 Oct '24

31 Oct '24

Dear All, I am a seL4 enthusiast , I am trying to port , build and test seL4 for ARM64 Cortex A53 based hardware. For Single core , I am able to boot via elf-loader then jump to kernel and successfully run Hello World program without any issues. But when I am trying to change it to multiple core SMP enabled on my hardware or even in ARM Qemu setup it is failing to boot. Can anyone please guide me , if seL4 supports multicore than for which version of ARM / board it currently supports , as I could see support for only Sabre-Arm32, which is ARMv7A. Boot log attach for reference. ———————————————————————— ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[40a4c000…40f57137] No DTB passed in from boot loader. Looking for DTB in CPIO archive…found at 40bacbe8. Loaded DTB from 40bacbe8. paddr=[4024c000…4024dfff] ELF-loading image ‘kernel’ to 40000000 paddr=[40000000…4024bfff] vaddr=[ffffff8040000000…ffffff804024bfff] virt_entry=ffffff8040000000 ELF-loading image ‘sel4test-driver’ to 4024e000 paddr=[4024e000…40654fff] vaddr=[400000…806fff] virt_entry=40e700 Boot cpu id = 0x0, index=0 HVC is not supported for PSCI! Failed to boot cpu 0x1: 18446744073709551615 abort() called. ——————————————————————————— Looking for any guidance, as it will be helpful for me to move forward . Regards, Vishal

2 1

seL4 developer hangout reminder
by Birgit Brecknell 28 Oct '24

28 Oct '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 29 Oct, 9:00pm UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Device memory access issue on sel4 user driver
by misbah khan 25 Oct '24

25 Oct '24

Hello sel4 developers, I am using seL4 for in our arm64 based hardware platform. I need to write a simple driver where i need to read/write some memory mapped registers The device physical address is "0x40520000" When i print the bootinfo using the below code: /*-- filter TaskContent("untyped-start", TaskContentType.ALL, subtask='init') -*/ printf(" CSlot \tPaddr \tSize\tType\n"); for (seL4_CPtr slot = info->untyped.start; slot != info->untyped.end; slot++) { seL4_UntypedDesc *desc = &info->untypedList[slot - info->untyped.start]; printf("%8p\t%16p\t2^%d\t%s\n", (void *) slot, (void *) desc->paddr, desc->sizeBits, desc->isDevice ? "device untyped" : "untyped"); I get the following output: CSlot Paddr Size Type 0x1ac 0 2^30 device untyped 0x1ad 0x40000000 2^28 device untyped 0x1ae 0x50000000 2^23 device untyped 0x1af 0x50810000 2^16 device untyped 0x1b0 0x50820000 2^17 device untyped I am mappint the physical address to virtual and trying to access it as: va = ps_io_map(&ops.io_mapper, (uintptr_t) 0x40520000,0x3000, PS_MEM_NORMAL); ZF_LOGE("Physical address 0x%x mapped to virtual address %p \n",DEV_REG_PADDR,va); for(int j=0;j<DEV_REG_SIZE;j+=sizeof(unsigned int)) { ZF_LOGE("Loc %d --> 0x%x ",j,*(unsigned int*)(va+j)); } I am able to access some registers, but then it gives a fault (after printing 5-6 register values) Similar is the behaviour with any reg between the range 0x40000000 - 0x50000000 Attaching the sample code and output: I am able to access first two address location, after that it gives halt. Regards, Misbah

2 2