December 2017 - Devel - lists.sel4.systems

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 16 Oct '24

16 Oct '24

Hi seL4 Dev team, Can someone explain the reason (share the reference) to invalidate the local TLB during kernel vspace activation as part CPU initialisation. The Tx2 board stuck while performing this operation. As per my understanding both Tx1 and Tx2 are using same A57 core. so the TLB initialisation and invalidation remain same for Tx2 and should not stuck during invalidation.Please correct me if anything wrong here. I understand from that instruction (tlbi vmalle1) which is invalidating stage 1 entries associated to the current VMID. Also from arm mmu code the seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as 16bit and page table setup 4k granular size. I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the state of processor but its throwing synchronous exception. Do we have any other option to dump all the register content to see the state of processor like we have one in 'sel4debug_dump_registers' which is used in sel4test code. Regards, Muneeswaran R

3 4

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

RefOS Building and Execution Error
by ALVI Aslam (MORPHO) 09 Feb '18

09 Feb '18

Hello Team, I was currently understanding the RefOS but the current code which is present in GIT is not Buildable at all. But after doing some workaround by myself I was able to build it successfully. While executing it on simulator for Kzm 1. Bootstrapping Kernel all finished successfully 2. Dropped to user Space successfully 3. RefOS initialize done successfully 4. Running RefOS Process Server failed In the step 4 while running the Process server it failed while proc_config_new() Failed to spawn Process for Console_server. So Far as per my debugging while coping and writing the elf Header it get failed while getting the capabilities. Excat error line vspace_internal.h line number 396. I would be a great support if anybody help me to resolve the issue. Thank You in advance Regards Aslam Alvi

2 1

x86 kernel address space side channels
by Corey Richardson 05 Jan '18

05 Jan '18

https://lwn.net/Articles/738975/ That's really painful, for Linux ;) I don't think seL4 is really impacted? I'm having a hard time thinking about what sensitive information could be disclosed by probing the kernel window. Maybe which memory regions caps being accessed by other concurrently running threads occupy? You could use that to make a covert channel, if the two threads trying to communicate are running in parallel. It seems really dubious that that could give you anything useful otherwise, and as the literature shows timing side channels are unavoidable on x86. Thought it was interesting and worth sharing! -- cmr http://octayn.net/ +16038524272

6 8

I/O and PCIE on TX1
by Jon Lamb 04 Jan '18

04 Jan '18

Hi seL4 Dev Team, I'm currently working on (mostly learning at this point) how we could add TX1 platform support for a PCIE network card (Intel 82580), using TK1 and others as a reference. I'm fairly new to working with PCI, but after looking around I think I have a general idea on what I need to do. I would appreciate it very much if someone with more experience could tell me if I'm on the wrong path here: * Using the TX1 TRM, I would populate the missing physical device region definitions in 'tx1/plat/machine/devices.h', and update the 'dev_p_regs[]' struct in 'tx1/plat/machine/hardware.h' * Figure out if I need to build up SMMU support (also a newbie here), I'm having doubts on whether I can bang on physical addresses or not without it * Construct a suitable implementation of 'ps_io_port_ops_t' for handling the I/O routines for libpci * Put together a hello world main program to exercise some of libpci's functionality * Once things are looking good there, move up to libethdrivers and port the needed bits for our Ethernet adapter using existing references (and eventually hooking up to lwip hopefully) At this point, I've been avoiding camkes for the sake of learning how everything works and if anyone can recommend a good starting C project for doing I/O on an ARM platform, that would be very helpful. Thanks in advance. -- Jon Lamb Software Engineer | *PolySync* 1020 SE 11th Ave, Portland, OR 97214 *c* 888.810.4284 x701 <888.810.4284%C2%A0x713> | *e* jlamb(a)polysync.io | *w* polysync.io <http://www.polysync.io/>

2 2

iMX6 dvfs registers
by Zippy Maniac 02 Jan '18

02 Jan '18

Hi, Sorry for pestering (again). I am trying to access the DVFS registers from a seL4 component and they seem to be read only. I can read/write them from UBoot and the kernel. So my guess is the registers require privilege even though I have yet to find a definitive statement to this effect in the ARM / NXP documentation. So the question is. Is it possible to give a component the necessary access rights to the DVFS registers via camkes? Or is there some other sort of workaround I could employ to gain access? Cheers, Zippy

2 1

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

13 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