- Devel - lists.sel4.systems

Dynamic Loading of application
by PANCHAL Vishalkumar (MORPHO) 18 Dec '17

18 Dec '17

Hello, Can we use ELF-Loader tool functions into the user_space application (here, main_app) to Dynamically load the image of other application (app-1, app-2, app-3) from external device ? [cid:image008.png@01D374F1.2B37E4A0] Regards, Vishal PANCHAL Software Engineer | Noida | R&D P : +91 (120) 4072 549 M. +91 94266 38316 E. vishalkumar.panchal(a)morpho.com<mailto:vishalkumar.panchal@morpho.com> [Idemia]<https://www.idemia.com/> Join us on [Facebook]<https://www.facebook.com/IdemiaGroup/> [Twitter]<https://twitter.com/IdemiaGroup> [LinkedIn]<https://www.linkedin.com/company-beta/3488/> [Youtube]<https://www.youtube.com/user/SafranMorpho/> [www.idemia.com]<https://www.idemia.com/> [OT-MORPHO is now IDEMIA] # " 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

Questions concerning the capability management system
by Timotej Tomandl 18 Dec '17

18 Dec '17

Hi, while reading about seL4 I have found a presentation "The seL4 capability system" by Matthew P. Grosvenor (https://www.cl.cam.ac.uk/resea rch/security/ctsrd/cheri/workshops/pdfs/20160423-sel4-capabilities.pdf), sadly I was able to track down only the slides, not the talk itself. It mentions the "Aurora project", the constraint solver running in static memory + stack space, concerning itself with the capability allocation. There are these questions which popped into my mind: 1. Is the source code of the Aurora project available anywhere? Is there any more information than the presentation available? 2. Is the constraint solver still necessary with the current version of the API? 3. If it is still necessary, then - what is the necessary strength of the constraint solver? - is a design, in which either the root process or the microkernel itself has to include such a constraint solver in static memory + stack space necessary for a microkernel with the guarantees of seL4 or is it a side-effect of the design decisions? Regards, Timotej Tomandl

2 1

Questions about Tx1 Physical Memory usage
by Muneeswaran Rajendran 14 Dec '17

14 Dec '17

Hi all, I’m trying to understand the implementation details and physical memory usage of seL4 for Tx1 we have available physical memory in Tx1 is 6GB. DRAM (4GB) - available address range 8000_0000 - FFFF_FFFF DRAM2 (4GB to 6GB) - available address range - 1_0000_0000 - 2_7FFF_FFFF In the hardware.h file (/kernel/include/plat/tx1/plat/machine/hardware.h),the avail_p_regs[] ={.start = 0x80000000, .end = 0xa7f00000 } '1MiB starting from 0xa7f00000 is reserved by the elfloader for monitor mode hooks'.I understand from the code its required only for Tk1. (/projects/tools/elfloader-tool/src/plat/tk1/monitor.S). As per my understanding is not not applicable for Tx1 so we can use contiguous region of physical ram 2GB to 4GB. Also it's allow to use higher physical memory for seL4 kernel ie > 4GB ? Thanks in advance. Regards, Munees

2 1

Re: [seL4] UEFI support for x86
by Alexander Boettcher 12 Dec '17

12 Dec '17

Hello, On 04.12.2017 18:15, Edward Sandberg wrote: > I modified the demo.run file to use fb_boot_drv and built the uefi > image. I tested it on an UP board, a Minnowboard Turbot, a Dell M3800 > laptop, and a Dell Precision 5810 desktop. I was unable to get > graphical output on any of them. I have pasted the logs for all (except > the laptop which has no serial port) below. > * UP BOARD ******************************** > WARNING: no console will be available to OS > Bender: Hello World. > framebuffer at [80000000+808ca000) 1920x1200@32 > framebuffer at [80000000+808ca000) 1920x1200@32 good > [init -> fb_boot_drv] Framebuffer with 1920x1200x32 @ 0x80000000 type=1 pitch=7680 > [init] child "report_rom" announces service "Report" > [init -> fb_boot_drv] resource_request: ram_quota=4612096 If you see such a message, the driver or component in general will not continue. The specified memory for the driver seems to be too low, try to increase it. It should be something above 9.2M (7680 Byte * 1200 = 9.2 M + some memory for the driver). Maybe 10-11M should suffice. > * MinnowBoard *********************************** > framebuffer at [80000000+808ca000) 1920x1200@32 > framebuffer at [80000000+808ca000) 1920x1200@32 good > [init -> fb_boot_drv] Framebuffer with 1920x1200x32 @ 0x80000000 type=1 pitch=7680 > [init -> fb_boot_drv] resource_request: ram_quota=4612096 Same here, try increase the memory for the framebuffer. > * Dell Precision 5810 ************************************** > Bender: Hello World. > framebuffer at [f1000000+f1300000) 1024x768@32 > framebuffer at [f1000000+f1300000) 1024x768@32 good > > Boot config: parsing cmdline 'sel4 disable_iommu' > Boot config: console_port = 0x3f8 > Boot config: debug_port = 0x3f8 > Boot config: disable_iommu = true > module #0: start=0xf9b8000 end=0xffff228 size=0x647228 name='image.elf' > Physical Memory Region from 0 size a0000 type 1 > Physical Memory Region from 100000 size 997ae000 type 1 > Adding physical memory region 0x100000-0x1f800000 > Physical Memory Region from 998ae000 size 9ac000 type 2 > Physical Memory Region from 9a25a000 size 49000 type 3 > Physical Memory Region from 9a2a3000 size c71000 type 4 > Physical Memory Region from 9af14000 size 492000 type 2 > Physical Memory Region from 9b3a6000 size 65000 type 20 > Physical Memory Region from 9b40b000 size 1000 type 1 > Physical Memory Region from 9b40c000 size e000 type 2 > Physical Memory Region from 9b41a000 size 1be6000 type 1 > Physical Memory Region from a0000000 size 10000000 type 2 > Physical Memory Region from fed1c000 size 4000 type 2 > Physical Memory Region from ff000000 size 1000000 type 2 > Physical Memory Region from 1000000000 size 1760000000 type 1 > Physical memory region not addressable > Adding physical memory region 0x0-0x1f800000 > seL4 failed assertion '!p_region_overlaps(reg)' at /home/esandberg/projects/embedded/genode-17.11/genode-17.11/contrib/sel4-097171f475bff21223783e130445b9be6b3d1bb4/src/kernel/sel4/src/arn > halting... This is a assertion in the seL4 kernel. Probably it complains about that region overlap due to following lines > Adding physical memory region 0x100000-0x1f800000 > Adding physical memory region 0x0-0x1f800000 I'm not sure, whether here the Multiboot 2 information is incorrect or the parsing by the kernel is too strict. Here one would require some more investigation in the Multiboot 2 spec (overlapping regions are valid or not?) and on the target machine in grub2/uefi, potentially bender and the sel4 kernel. Thanks for testing and the infos. -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 4

seL4 bring up on inmate cell of jailhouse.
by Muneeswaran Rajendran 12 Dec '17

12 Dec '17

Hi, I would like to bring up seL4 on inmate cell of Tx1. The jailhouse is running successfully on Tx1 board. I have created root cell and not root cell configuration on jailhouse. I able to load seL4 image successfully on inmate cell then during execution its stuck in the while extracting the program header. I checked with jailhouse forum they suggested some one might have ported seL4 or L4 kernel on jailhouse.also informed that seL4 kernel need to rebuild with some patches. Somehow I do not find the patches for seL4 or Fiasco.OC kernel to bring up on jailhouse.Please share links if you any. Also experimented by changing the PHY_ADDR higher then 2G (0x80000000) configuration ie(0x90000000 to 0xF0000000) and (0x100000000 to 0x170000000) while booting from the u-boot I observed KERNEL DATA abort after boot strapping the kernel. It means that this address cannot accessible in the seL4 kernel. Case 1: 0x90000000 to 0xF0000000 sample logs: ------------------- Bootstrapping kernel KERNEL DATA ABORT! Faulting instruction: 0x1ca9c FAR: 0x90000000 ESR (DFSR): 0x96000044 halting... Kernel entry via Interrupt, irq 0 case 2: 0x100000000 to 0x170000000 It's throwing synchronous data abort during program header extraction. sample logs: ------------------ binaries/elf64: elf64_getNumProgramHeaders "Synchronous Abort" handler, esr 0x96000044 ELR: 82002c8c LR: 820031f4 x0 : 0000000100000000 x1 : 0000000000000000 x2 : 000000000022fc10 x3 : 00000000827a5d40 x4 : 0000000000000000 x5 : 00000000000db8ab x6 : 0000000082007948 x7 : 0000000082008578 x8 : 0000000082008570 x9 : 0000000000000008 x10: 000000000000000f x11: 00000000fed87118 x12: 0000000000000047 x13: 0000000000000040 x14: 0000000000000001 x15: 00000000fed33114 x16: 0000000000000000 x17: 0000000000000000 x18: 00000000fc82ede0 x19: 00000000827a5ff0 x20: 0000000000000002 x21: 0000000082000000 x22: 00000000fc832800 x23: 0000000000000002 x24: 00000000fedaa7fc x25: 0000000000000000 x26: 0000000000000000 x27: 00000000fc8322f0 x28: 0000000000000000 x29: 00000000827a5e80 someone can give suggestion or pointers how we can bring seL4 on Jailhouse. Regards, Munees

3 2

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 04 Dec '17

04 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 04 Dec '17

04 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