December 2021 - Devel - lists.sel4.systems

vm physaddr != virtual?
by Richard Clark 22 Dec '21

22 Dec '21

My VM's can't seem to be untied from actual physical memory.... I've got a nice old moldy version of sel4, around version 8 I think, but it's got some life left if we can figure out how to remap our VMs to 0 instead of mapping virtual directly equal physical... In other words, for some reason, we map virtual == physical, and have to tell the VM that it is up at some high-level address. We would like to be able to pick a physical patch of memory, and map it to zero in the VM, so the VM can believe it is at 0. Honestly I don't understand why that isn't the default anyway... But I've found examples where I can specify a physical address and get back an arbitrary virtual address, and other examples where I can specify a virtual address and get back an arbitrary physical page. What I need, is a way to specify both the physical and the virtual addresses into my VM vspace. Would you happen to have an example or two on hand? For a little more context, I've got the following code, which appears to map the first page ok, but then fails trying to map the next page when called a second time: map_ram_to(vspace_t *vspace, vspace_t *vmm_vspace, vka_t* vka, uintptr_t paddr, uintptr_t vaddr) { vka_object_t frame_obj; cspacepath_t frame[2]; reservation_t res; int err; /* reserve vspace */ printf("map_ram_to, reserve phys mem at %p to vaddr %p\n", (void *)paddr, (void *)vaddr); res = vspace_reserve_range_at(vspace, (void *)paddr, 0x1000, seL4_AllRights, 1); if (!res.res) { ZF_LOGF("Failed to reserve range"); return NULL; } /* map phys addr ro frame obj */ printf("map_ram_to, alloc phys mem at %p\n", (void *)paddr); err = vka_alloc_frame_at(vka, 12, paddr, &frame_obj); if (err) { printf("ERROR VKA alloc ptr: %p\n", vka->data); ZF_LOGF("Failed vka_alloc_frame_maybe_device in devices.c"); vspace_free_reservation(vspace, res); return NULL; } vka_cspace_make_path(vka, frame_obj.cptr, &frame[0]); printf("map_ram vka_cspace_alloc_path\n"); err = vka_cspace_alloc_path(vka, &frame[1]); if (err) { ZF_LOGF("Failed vka_cspace_alloc_path"); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; } printf("map_ram vka_cnode_copy\n"); err = vka_cnode_copy(&frame[1], &frame[0], seL4_AllRights); if (err) { ZF_LOGF("Failed vka_cnode_copy"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; } err = map_page(vspace, frame_obj.cptr, (void *)vaddr, seL4_AllRights, 1, 12); vspace_free_reservation(vspace, res); if (err) { printf("FAILED Failed vspace_map_pages_at_vaddr\n"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); return NULL; } printf("map_ram_to, worked and zeroed at %p\n", (void *)paddr); return (void *)paddr; } Help is greatly appreciated! Richard H. Clark

1 0

mapping tutorial answers?
by Richard Clark 22 Dec '21

22 Dec '21

I'm interested in the ANSWERS to the MAPPING tutorial. I have my own virtual/physical memory management system and need only the ability to map a specific physical address to a specific virtual address. I can find no such thing in all the sel4 code that I have, but it appears that the mapping tutorial is what I need. Does anyone have this? (preferably arm64 and/or x64) Richard Clark

1 0

sel4-sys support
by kgugala＠antmicro.com 16 Dec '21

16 Dec '21

Hi All, We’ve been working on reviving the sel4-sys Rust crate and getting it usable again. Currently, we have it working correctly with RISC-V, we’re working on ARM (including aarch64) and X86. We’d like to contribute this work, but to have it landed we need to extend the test suite to include crate tests - especially the syscalls API. During the build, the crate generates the syscalls functions accessible from Rust code based on seL4 config. We use standard sel4test-tests suite to handle the tests: * We build the crate as static library * Sel4test is built with `-DLibSel4FunctionAttributes=public` and while linking we overwrite the original symbols with the ones from a static library from the crate This allows us to run the standard test suite against Rust syscall stubs. For now the crate generates the syscall stubs with Rust flavor, so functions signatures between Rust and C do not match. To handle this we additionally generate a thin glue code adopting Rust signatures to the C ones. We generate the Rust syscalls with a slightly modified version of the `syscall_stub_gen.py` script - we copied it into the crate’s codebase. Copying the code doesn’t seem to be the best idea - we’d need to maintain the code in both places - seL4 kernel and the crate. We’d like to merge the Rust generator with the current set of tools - is this something you’d be willing to land in the kernel code? If not, how would you see the way forward here? Thanks and best regards Karol

4 5

Re: seL4 developer hangout/video call
by Isaac Beckett 15 Dec '21

15 Dec '21

This is 4pm east coast US/EST. > The next instalment of the seL4 developer hangout is happening as planned tomorrow. It's the last one for this year: > > - Sydney: Wed, Dec 15, 8am > - Central Europe: Tue, Dec 14, 10pm > - US West Coast: Tue, Dec 14, 1pm > > Zoom link: https://unsw.zoom.us/j/82640784431 > > (There is also a separate meeting of the technical steering committee end of this week) > > Cheers > Gerwin

1 0

two questions about cteDelete of sel4 kernel 12.0.0 ?
by yadong.li 12 Dec '21

12 Dec '21

Hi： I have two questions about cteDelete of sel4 kernel 12.0.0？ IF I want to delete slot that slot->cap is cnode object(I called it level 1 cnode). The finaliseSlot function will create zombie capability and call reduceZombie(), param "immediate" is ture. the reduceZombie() call cteDelete() delete the endSlot, if the endSlot->cap is cnode capability again(I call it level 2 cnode), this time param "immediate" is false. and cteDelete() will call reduceZombie again, but because param "immediate " is false ,this time reduceZombie will not call cteDelete recursively. the reduceZombie will call capSwapForDelete, if Swap cap is not cnode or tcb, when it return to finaliseSlot, finaliseSlot will check finaliseCap, because swap cap is not cnode or tcb, almost it capRemovable, and it return directly. 1. I think when call capSwapForDelete in reduceZombie, the level 2 cnode become Cyclic zombie, but when return finaliseSlot, I do not think it will deal with below branch: if (!immediate && capCyclicZombie(fc_ret.remainder, slot)) { } because this time ,slot ->cap is not cnode or tcb, it will not create zombie cap. Who will delete level 2 cnode ? Is it lost as "Cyclic zombie", memory leak? 2. when delete cnode, it will check "preemptionPoint", if our delete is beak, even though fs_ret.success is false, but this false is not deliver to caller, who will delete cnode object again? Thank you very much

2 3

seL4 kernel does not receive PCI interrupts
by hamed_ganji＠aut.ac.ir 12 Dec '21

12 Dec '21

Hi all, I have created a simple CAMKES-VM-x86 app for a PC but its PCI devices are not working due to not receiving corresponding interrupts. By adding a printf to the function "handleInterrupt" inside the seL4 kernel I found that only some limited interrupts such as timer and serial are received. However, capdl_spec.c file contains all necessary declaration of capabilities and objects for the required interrupts such as follows, ... [19625] = { #ifdef CONFIG_DEBUG_BUILD .name = "vm0_irq_10", #endif .type = CDL_IOAPICInterrupt, .slots.num = 1, .slots.slot = (CDL_CapSlot[]) { {0, {.type = CDL_NotificationCap, .obj_id = 19567 /* vm0_irq_notification_obj_10 */, .is_orig = true, .rights = (CDL_CanRead), .data = { .tag = CDL_CapData_Badge, .badge = 0}}}, }, .ioapicirq_extra = { .ioapic = 0, .ioapic_pin = 10, .level = 1, .polarity = 1, }, }, ... and the host endpoint of the VMM thread is properly set to receive IRQ notifications and route them to VM, and the IOAPIC pin number (source) is also true, I checked. How can I solve the problem? Any pointers would be appreciated. Kind regards, Hamed

1 0

Nvidia Tegra SoCs: Has anyone tried running seL4 on them?
by Isaac Beckett 12 Dec '21

12 Dec '21

Has anyone experimented with running seL4 on Tegra SoCs? I’m interested mainly because I own a Nintendo Switch console that is vulnerable to an exploit in the boot rom that allows for booting arbitrary payloads. Most people use it to run modified versions of the official firmware, or to run Linux or Android, so the hardware is at least decently well reverse engineered at this point, and there are even proper Linux drivers for the joy-con detachable controllers. I’m interested in attempting to run seL4 on this device, mostly to see if I can, but I figured I’d ask here first to see if anyone’s attempted similar hardware.

2 2

next seL4 TSC meeting on Fri 17 Dec (16 Dec in US and Europe)
by Gerwin Klein 11 Dec '21

11 Dec '21

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Fri, 17 Dec, 8am - Central Europe: Tue, 16 Dec, 10pm - US West Coast: Tue, 16 Dec, 1pm The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/82827057586 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: - update on GitHub status, test stability, etc - release schedule - change main verification platform to imx8? - RFCs: - Core Platform https://sel4.atlassian.net/browse/RFC-5 - Removing CNode Mutate https://sel4.atlassian.net/browse/RFC-7 - SMC calls https://sel4.atlassian.net/browse/RFC-9 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

1 0

two questions about cteDelete of sel4 kernel？
by yadong.li 11 Dec '21

11 Dec '21

Hi： I have two questions about cteDelete of sel4 kernel？ IF I want to delete slot that slot->cap is cnode object(I called it level 1 cnode). The finaliseSlot function will create zombie capability and call reduceZombie(), param "immediate" is ture. the reduceZombie() call cteDelete() delete the endSlot, if the endSlot->cap is cnode capability again(I call it level 2 cnode), this time param "immediate" is false. and cteDelete() will call reduceZombie again, but because param "immediate " is false ,this time reduceZombie will not call cteDelete recursively. the reduceZombie will call capSwapForDelete，it will swap zombie cap with slot 0 of level 2 cnode, if Swap cap(slot0 of level 2 cnode) is not cnode or tcb(the cnode object slot 0 must point to cnode self ? I did not find this limitation), when it return to finaliseSlot, finaliseSlot will check finaliseCap, because swap cap is not cnode or tcb, almost it call be capRemovable, and it return directly. 1. I think when call capSwapForDelete in reduceZombie, the level 2 cnode become Cyclic zombie, but when return finaliseSlot, I do not think it will deal with below branch: if (!immediate && capCyclicZombie(fc_ret.remainder, slot)) { } because this time ,slot ->cap is not cnode or tcb, it will not create zombie cap. then Who will delete level 2 cnode ? Is it lost as "Cyclic zombie", memory leak? 2. when delete cnode, it will check "preemptionPoint", if our delete is beak, even though fs_ret.success is false, but this false is not deliver to caller who will delete it again? thank you for your help

1 0

How can I port the seL4 microkernel to my unofficially verified hardware？
by yjy 10 Dec '21

10 Dec '21

Does the document provide relevant information or project? I read related articles and I can be sure that my instruction set is common. Thank you.

2 1