- Devel - lists.sel4.systems

Dynamic Loading of application
by ALVI Aslam (MORPHO) 12 Dec '17

12 Dec '17

Hi everyone, Greetings, I'm just started with seL4. Current Progress: - I have built an application on top of seL4 as learning from tutorials, so this is my current design [seL4,My main_APP,App2,App1,App3] Here My main_App is my main application build on seL4 and App1, App2 and App3 are sub components link with My main_App.( Just like in Tutorial 4 of seL4). When i build and run , this is working fine, no issue with it. when i run make command first i build kernel then libraries, then App1 , App2, App3, then My main_app and in the end it generate a single image file to execute. My Question :- Can i dynamic load my sub components(App1, App2, App3) which is required by My_main_App in run time ? Can we do that in seL4 is yes then how ? i dont want my App1, App2 and App3 part of final image, I want to load them and run them separately using My_main _App? Thank you in Advance, Please Help. Regards, Aslam ALVI # " This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, you are notified that any dissemination, copying of this e-mail and any attachments thereto or use of their contents by any means whatsoever is strictly prohibited. If you have received this e-mail in error, please advise the sender immediately and delete this e-mail and all attached documents from your computer system." #

2 1

AARCH64 with CAMKES (Questions)
by Michael DeFrancis 06 Dec '17

06 Dec '17

Can camkes be used with ARM AARCH64? I am attempting to build a linux virtual machine on top of the zynqmp ultrascape+ / sel4 kernel, and using the tk1 vmm project as my reference point. When the build system attempts to generate camkes-gen.mk, it fails - displaying an error indicating that aarch64 is not a valid architecture specification for camkes. I see that valid arm options are aarch32 or arm_hyp. Is arm_hyp what I am looking for here? What would I need to do in order to strip the camkes dependencies out of the tk1 vmm project? Thanks, Mike D Computer Security Engineer - Intelligent Automation, Inc. (301)294-5263 ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

3 3

UEFI support for x86
by Edward Sandberg 05 Dec '17

05 Dec '17

Is there a plan to add UEFI support in seL4 for x86 hardware in the near future? Newer x86 boards are frequently UEFI only. It is possible to get around the lack of UEFI support, as I have done with the UP board: https://up-community.org/wiki/Hardware_Specification but I am hitting problems which I will detail below. When I compile using ia32_debug_xml_defconfig and boot using the resulting images the board fails to find the RSDP location. To fix this I had to modify the source code a bit: * seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.h + #define UPBOARD_RSDP 0x5B161000 * seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.c - acpi->rsdp = acpi_sig_search(acpi, ACPI_SIG_RSDP, strlen(ACPI_SIG_RSDP), - (void *) BIOS_PADDR_START, (void *) BIOS_PADDR_END); + acpi->rsdp = (void *)UPBOARD_RSDP; * seL4test/kernel/src/plat/pc99/machine/acpi.c - for (addr = (char*)BIOS_PADDR_START; addr < (char*)BIOS_PADDR_END; addr += 16) { + for (addr = (char*)0; addr < (char*)PPTR_BASE; addr += 16) { It would be handy to have this as a kernel parameter to cover cases where it is not successfully discovered automatically. With these changes I can boot the board and several tests pass but then I get stuck on INTERRUPT0001 (Test interrupts with timer). I don't get a test failure or an error the board just sits and makes no more progress. Someone had that test fail in this post: https://sel4.systems/pipermail/devel/2017-February/001328.html and the first recommendation was to check if the irq of the timer was correctly found. I booted the board into linux to find the correct irq which was listed as 0 in /proc/interupts. I added a printf to handleInterrupt in the kernel source, recompiled and when I booted seL4 I found that the irq reported to handleInterrupt is 125 (which sel4 reports as the max interrupt value) every time that function is called. Adding this printf also showed me that when the test hangs the board hasn't crashed or locked up as calls to handleInterrupt are made continuously. At this point I noticed that before any tests started to run several ACPI tables are not recognized: Parsing ACPI tables Skipping table FPDTD, unknown Skipping table FIDT<9c>, unknown Skipping table UEFIB, unknown Skipping table TPM24, unknown Skipping table LPIT^D^A, unknown Skipping table BCFG9^A, unknown Skipping table PRAM0, unknown Skipping table CSRTL^A, unknown Skipping table BCFG9^A, unknown Skipping table OEM0<84>, unknown Skipping table OEM1@, unknown Skipping table PIDVÜ, unknown Skipping table RSCI,, unknown Skipping table WDAT^D^A, unknown Warning: skipping table ACPI XSDT Maybe one or more of those tables needs to be loaded to handle interrupts properly. The LPIT table is conspicuous in the case of the timer test but I think other tests are likely to depend on the other tables. Any suggestions about porting this type of hardware? -- Edward Sandberg Adventium Labs 111 3rd Avenue S. Suite #100 Minneapolis, MN 55401 ed.sandberg(a)adventiumlabs.com

4 10

seL4_Send vs. seL4_Call
by Stefan Wallentowitz 05 Dec '17

05 Dec '17

Hi everyone, I have built a very simple application that loads another process, which is very similar to the tutorials. For testing I wanted to send from the second process to the first one using seL4_Send and observe that the second process never continues after the seL4_Send blocked, despite the receiver called seL4_Recv and got the message. If I call seL4_Call and the receiver does seL4_Recv + seL4_ReplyRecv it works without any other changes to the code. I am wondering if I am understanding something fundamentally wrong and/or what the best strategy to debug this behavior is. Thanks for your help! Cheers, Stefan

2 1

camkes-gen.mk generated prerequisites
by Gordon Clark 01 Dec '17

01 Dec '17

We have a multi component camkes application with each component using a few common services and then having application interfaces to a small number of other components.All these components are imported into a top level system description camkes file. Examining the generated camkes I see that all the generated header and source files have exactly the same make prerequisites meaning a change to logically unrelated components causes them all to be regenerated and recompiled. Now I have discovered the camkes cache this is less of an issue but is there a better way we can structure our application to reduce the edit-compile-go cycle ? Regards Gordon

2 1

seL4SharedData
by Zippy Maniac 30 Nov '17

30 Nov '17

We have a security requirement on our ARM based product using CAmkES 2.2.x to ensure all sensitive data declared in specific seL4SharedData regions are erased on detection of a power failure. We achieve this by overwriting the data with a known pattern that we read back from a separate component before declaring the device as secured. This is working fine. But we need to guarantee that the overwrite data is actually written to DDR and we aren't just using cached values. This means flushing the L1 and L2 data caches specific regions. We could use seL4HardwareMMIO regions and declare our data in the memory map and use these regions as un-cached. Or use the _hardware_cached attribute and call the provided flush method when necessary. Our main issue with doing this, except the fiddle of mapping multiple different sized regions into the memory map, is we could potentially expose the physical locations of the sensitive data rather than having it wrapped in the virtual address space of a component. Having a flush method on seL4SharedData would be the ideal solution. We are not in a position to upgrade our CAmkES version on this product at the moment. Any thoughts? Zippy

4 3

Tx1 UART and GiC distributor PPTR address
by Muneeswaran Rajendran 27 Nov '17

27 Nov '17

Hi, The PPTR address range between UART and GIC distributor was 12k (kernel/include/plat/tx1/plat/machine/device.h). But when refer in TX1 reference sheet the length was specified as 64byte for UART,4k for GIC distributor and 8k for interrupt controller. can you please point out the reference or reason to choose this address for Tx1 board? /* These devices are used by the seL4 kernel. */ #define UARTA_PPTR 0xffffffffffff0000 #define GIC_DISTRIBUTOR_PPTR 0xffffffffffff3000 #define GIC_CONTROLLER_PPTR 0xffffffffffff4000 These addresses are used during kernel device map to access in the userspace map_kernel_devices : kernel_devices[i].paddr :0x50042000 kernel_devices[i].pptr 0xffffffffffff4000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f4 map_kernel_devices : kernel_devices[i].paddr :0x50041000 kernel_devices[i].pptr 0xffffffffffff3000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f3 map_kernel_devices : kernel_devices[i].paddr :0x70006000 kernel_devices[i].pptr 0xffffffffffff0000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f0 Regards, Munees

1 0

Caught cap fault in send phase at address 0x0 @Tx2
by Muneeswaran Rajendran 23 Nov '17

23 Nov '17

Hi seL4 Dev Team, I am bringing up the sel4 kernel on tx2 board with ref of Tx1. I encountered the TLB invalidation hang issue after kernel map window setup. I do not know the exact reason for hang so just disable that piece of code to look further execution of sel4 kernel. After that it dropped into the usersapce and throwing the cap fault or vm fault issue. Does anyone has come across this type of issue and how it debugged?. Please share your thought or pointers to debug this issue. I shared the full log details here. ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p3 paddr=[82000000..827abfff] kernel_phys_start: 0xffffffff80000000 kernel_phys_end:0xffffffff8022fcdf load_elf : image_size 0x230000 ELF-loading image 'kernel' paddr=[80000000..8022ffff] vaddr=[ffffff8000000000..ffffff800022ffff] virt_entry=ffffff8000000000 load_elf : image_size 0x5e9000 ELF-loading image 'sel4test-driver' paddr=[80230000..80818fff] vaddr=[400000..9e8fff] virt_entry=41b160 Enabling MMU and paging Jumping to kernel-image entry point... kernel_info.virt_entry : 0x0 user_info.phys_region_start : 0xffffffff80230000 user_info.phys_region_end:0xffffffff80819000 user_info.virt_region_start:0x400000 user_info.virt_region_end:0x9e9000 user_info.phys_virt_offset:0x7fe30000 user_info.virt_entry:0x41b160 Bootstrapping kernel Booting all finished, dropped to user space Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on code at address 0x41b160 with status 0x82000010 in thread 0xffffff8027ef4200 "rootserver" at address 0x41b160 With stack: halting... Kernel entry via VM Fault, fault type: 4305248 Thanks in advance Muneeswaran R

1 0

Tx1 SMP and Hypervisor support
by Muneeswaran Rajendran 17 Nov '17

17 Nov '17

Hi Sel4 Dev Team, Any update of SMP and Hypervisor feature which fully functional on TX2. If its not available when will get this feature supported . Regards, Munees

3 4

1:1 Mapping of Zynqmp devices
by Chris Guikema 16 Nov '17

16 Nov '17

Hello, I am attempting to port the camkes-arm-vm to the zynqmp platform. For the TK1 and Exynos platforms, the physical address of the hardware devices are well below the kernelBase of 0xe0000000. However, for the zynqmp, these hardware devices are greater than the kernel base. This causes the "map_emulated_device" function call to fail for the GIC and any other passthrough devices. sel4utils_reserve_range_at_no_alloc@vspace.c:589 Range not available at 0xff010000, size 0x1000 Assertion failed: res.res (/home/chrisguikema/seL4/NAMC/camkes-arm-vm/libs/libsel4arm-vmm/src/devices.c: map_device: 160) Is there a way to 1:1 map these devices, even if they are above the kernelBase? Thanks, Chris

2 1