Devel December 2021

devel@sel4.systems

22 participants
26 discussions

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

Troubles booting VM with large memory(e.g VM_RAM_SIZE >= 2048MB)
by Han JingLong 韩景龙 09 Dec '21

09 Dec '21

Hello all, Reference to seL4 Docs/Projects/CAmkES ARM VMM, I have successfully run a VM (a Linux guest OS and config VM_RAM_SIZE = 1024MB) on a new ARM(ArmV8a CortexA55) platform. But when I tried to increase the ram size assigned to VM, I encountered the following error: ============================================================================== ram_ut_alloc_iterator@guest_ram.c:295 Failed to allocate page map_vm_memory_reservation@guest_memory.c:470 Failed to get frame for reservation address 0xae7c0000 reservation_size:60000000 …… vm_ram_touch@guest_ram.c:160 Failed to touch ram region: Not registered RAM region 32 bit ARM insts not decoded Pagefault from [Linux]: write fault @ PC: 0xffff000008d9132c IPA: 0xaffff000, FSR: 0x92000046 Context: x0: 0xffff7dfffe639000 x1: 0x0 x2: 0xfc0 x3: 0x4 x4: 0x0 x5: 0x40 x6: 0x3f x7: 0x0 x8: 0xffff7dfffe639000 x9: 0x0 x10: 0x1000 x11: 0x6f01c3b8 x12: 0xc0000000 pc: 0xffff000008d9132c x14: 0x0 sp: 0xffff000009668d80 spsr: 0x40000085 x13: 0x60000000 x15: 0x4 x16: 0x1800 x17: 0xffff7dfffe81c3b4 x18: 0x8 x19: 0xaffff000 x20: 0xffff0000096a1fd0 x21: 0xffff7dfffe80009c x22: 0x58389df x23: 0xffff0000091ce000 x24: 0x4b78e0 x25: 0x47b87c x26: 0x0 x27: 0xa0000000047b818 x28: 0x614f0018 x29: 0xffff000009643eb0 x30: 0xffff0000094f7ad0 m-------- Assertion failed: rt >= 0 (/home/hjl/workdir/vmm_sel4_sdx_android/projects/seL4_projects_libs/libsel4vm/src/arch/arm/fault.c: fault_get_width: 623) Attach config file for reference： 1. overlay dts reserved-memory { #address-cells = < 0x02 >; #size-cells = < 0x02 >; ranges; vm-memory@60000000 { reg = < 0x00 0x60000000 0x00 0x60000000 >; no-map; }; }; 1. devices.camkes #define VM_INITRD_MAX_SIZE 0x5000000 //80 MB #define VM_RAM_BASE 0x60000000 #define VM_RAM_OFFSET 0 #define VM_RAM_SIZE 0x60000000 #define VM_DTB_ADDR 0x6F000000 #define VM_INITRD_ADDR 0x6A000000 vm0.untyped_mmios = [ “0x35436000:12”, // Interrupt Controller Virtual CPU interface (Virtual Machine view) /* The purpose of these untyped regions is to force the untyped * allocator to treat this memory region as reserved so that when we * try to ensure that the VMM is placed into this region in RAM, it * will definitely be available for placement. * * This address pertains to vm-memory@60000000 in the overlay DTS */ “0x60000000:28”, // RAM “0x70000000:28”, // RAM “0x80000000:28”, // RAM “0x90000000:28”, // RAM “0xa0000000:28”, // RAM “0xb0000000:28”, // RAM ]; 1. guest linux dts memory@60000000 { device_type = “memory”; reg = <0x00 0x60000000 0x00 0x60000000>; }; ============================================================================== In contrast, I tried to expand the VM memory based on QEMU and encountered the same problem. Attach config file for reference： 1. settings.cmake if(${PLATFORM} STREQUAL “qemu-arm-virt”) set(QEMU_MEMORY “4096”) set(KernelArmCPU cortex-a53 CACHE STRING “” FORCE) set(VmInitRdFile ON CACHE BOOL “” FORCE) endif() 1. overlay-reserve-vm-memory.dts reserved-memory { #address-cells = < 0x02 >; #size-cells = < 0x02 >; ranges; vm-memory@40000000 { reg = <0x0 0x40000000 0x0 0x50000000>; no-map; }; }; 1. devices.camkes #define VM_INITRD_MAX_SIZE 0x1900000 //25 MB #define VM_RAM_BASE 0x40000000 #define VM_RAM_SIZE 0x50000000 #define VM_RAM_OFFSET 0x00000000 #define VM_DTB_ADDR 0x4F000000 #define VM_INITRD_ADDR 0x4D700000 vm0.untyped_mmios = [ “0x8040000:12”, // Interrupt Controller Virtual CPU interface (Virtual Machine view) “0x40000000:29”, // Linux kernel memory regions “0x60000000:29”, // Linux kernel memory regions “0x80000000:28”, // Linux kernel memory regions ]; 1. guest linux dts memory@40000000 { reg = <0x0 0x40000000 0x0 0x50000000>; device_type = “memory”; }; Is there any memory limit for VM? or Configuration problem? Anyways anyone any help can provide would be awesome and thanks in advance for any help! 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

getKernelWcetUs: where does the 10us return value come from?
by Jack Chen 09 Dec '21

09 Dec '21

Hi all, Quick questions regarding the return value of getKernelWcetUs(): 1. For ARM the value is assigned during build process taking config.cmake files, where KERNEL_WCET's are all 10us (except for tk1 it's 100us, typo?) For x86 the function returns 10 directly, and for risc-v, comment suggests it's copied from x86 hoping it's an overestimate. Where does this "10us" come from? Based on static estimate done previously on Armv6 (imx31)? AOS lecture mentioned a "378us" kernel WCET estimate and 99.5us observed WCET for Armv6. 2. Is this 10us WCET value the one used as padding in the Temporal Partitioning routine? ("worst-case flushing time"?) Regards, Jack

3 5

Incorporating seL4 into your project, risc-v architecture
by so_s＠gmx.de 08 Dec '21

08 Dec '21

Dear seL4 devs and community. I try to create a simple project using the seL4 micro kernel. For setting up my environment I followed this (https://github.com/manu88/SeL4_101) and this (https://docs.sel4.systems/projects/buildsystem/incorporating.html) article. As kernel I'm using the last release of SeL4 (https://github.com/seL4/seL4/releases/tag/12.1.0). I created some kind of user application, like Manu88 did with a simple Hello World C-Program. While building with the delivered init-build.sh script I got a lot of repeating errors like this: CMake Error at tools/cmake-tool/helpers/simulation.cmake:179 (add_custom_command): Error evaluating generator expression: $<TARGET_PROPERTY:rootserver_image,KERNEL_IMAGE_NAME> Target "rootserver_image" not found. Call Stack (most recent call first): CMakeLists.txt:22 (GenerateSimulateScript) While going through Manu88s guide I saw that he also got this errors. But after adding a CMakeList.txt file inside his user code, and declaring it as rootserver inside the CMakeList.txt file (I just copied the contents from here: https://github.com/manu88/SeL4_101/blob/master/projects/Hello/CMakeLists.txt) he got rid of the errors. I still get them and searching through the internet could not find a solution for me. Bellow I added the folder structure of my project. Project/ ├── kernel/ ├── projects/ │ ├── Hello/ │ ├── musllibc/ │ ├── utils_libs/ │ ├── seL4_libs/ ├── build/ ├── tools/ │ └── cmake-tool/ │ └── elfloader-tool/ ├── init-build.sh -> tools/cmake-tool/init-build.sh ├── CMakeLists.txt ├── application_settings.cmake -> tools/cmake-tool/helpers/application_settings.cmake ├── settings.cmake So I cannot tell where the issue lies. Any pointers would be appreciated. Kind regards, Sophia

2 3

capdl-loader questions
by Sam Leffler 08 Dec '21

08 Dec '21

I've been investigating how capd-loader works and have some questions. My apologies if these were previously discussed. 1. CDL_Model is mutable. The capDL specification looks like a perfect candidate for being in .rodata but it's stored+treated as mutable. Why? I see capdl-loader uses the mutability to store mapped page frame caps and, for risc-v, VSpace roots, but both can be easily handled w/o modifying the spec. Having this immutable has many benefits. 2. All page frames are treated as shared. CAPDL_SHARED_FRAMES is #define'd in the code so every frame is treated as shared. This inflates the size of the orig_caps array and the kernel capabilities table but seems unnecessary. Why? I've verified that instead of doing the Copy op on each page you can just check the return of the seL4_Page_Map call and if necessary clone the cap. Better would be for camkes to identify shared page frames so this doesn't require 2x syscalls (which spam's the console w/ CONFIG_PRINTING enabled). 3. Why does copy_addr_with_pt exist? There are two memory regions created for mapping page frames into the rootserver address space for doing fill ops. One is 64KB and the other is 1 page (nominally 4KB). init_frame tries the 4KB region first then falls back to the 64K region if mapping into the 4KB region fails. Why (i.e. why would the 1st mapping call fail)? On my risc-v system I never use the 64K region and I'm not sure when it might be used? Even if it were used, why is 64K always allocated; seems like the region should be sized according to the target platform. Having this extra region has a cost that can be significant on small systems. 4. console output. Why is sel4_DebugPutChar (or similar) not a standard part of the kernel? This forces capdl-loader to depend on libsel4platsupport for console output which in turn affects cap space. I can't imagine an seL4 system that cannot write to the console and I think it's entirely reasonable to have a critical system service like the rootserver use that. 5. duplicate_caps. The scheme for constructing a running system from a spec is straightforward except for duplicating caps. Why are all TCB's and CNode caps dup'd? Why does init_tcbs call init_tcb on the original object but immediately configure_tcb on the dup? There are other places where the dup cap is used instead of the original cap (e.g. init_cnode_slot). None of this seems to matter on risc-v; maybe this matters on some other architectures? 6. On risc-v all pages appear to be marked executable--including ipc buffers! This seems just wrong and a potential security hole. 7. Why does seL4_TCB_WriteRegisters take a _mutable_ seL4_UserContext? I'm guessing this is a mistake in the xml spec (but haven't looked). 8. init_cspaces mystifies me. There are two loops over all CNodes; one that does "COPY" operations and one that does "MOVE" operations. I see nothing explaining what's happening. I've read this code many times and still don't get it; please explain. 9. According to comments, the use of a global static to setup the UserContext for a new TCB is done because one cannot take the address of a local variable. On what architecture is this true? On risc-v the context is copied into "registers" before calling the kernel so this doesn't appear to be an issue with crossing the user-kernel protection boundary. 10. Memory reclamation. I'm unclear what happens to the memory used by capdl-loader. The process does a TCB_Suspend call when it's done. Does this cause the CSpace & VSpace to be reclaimed? For CAmkES this doesn't matter as there's no support for allocating memory but I'm building a system where this isn't true. How do I release memory (in particular) back to the untyped pool? I have a bunch of niggly code complaints/questions but let's start with the above. -Sam

2 4

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel December 2021