March 2018 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 29 Jan '25

29 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

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

15 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 18 May '23

18 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

Questions on U-boot Verified Boot with CAmkES-ARM-VM
by Daniel Wang 10 Jul '18

10 Jul '18

Hi all, I’m trying to test secure boot with the CAmkES-arm-vm. I found that U-boot has its implementation of secure boot called verified boot, but it seems only support FIT image format. I’m wondering is there a way to convert the final ELF image to an FIT image? I’m studying the details of different booting image format. I’m not sure how it would work with seL4 camkes demo specifically, since there are so many binary files and cpio archives packed in the final ELF image. Would love to hear your opinions. Thank you very much! Best Regards -Daniel Wang

2 1

ARM Vchan Error
by Daniel Wang 10 Jul '18

10 Jul '18

Hi all, I’m trying to make Vchan work on camkes-arm-vm in the process I encountered a couple problems. Hope you can give me some advice. I knew that Vchan is out dated and never finished on ARM. But it seems the only option for now (please correct me if I’m wrong). Here is what I did so far: 1. modified tk1_vmlinux.c by adding the virtual device and fault handler and installed it to guest linux with vm_add_device(vm, &vchan_dev); --------------------------------------------------- vchan_device_fault_handler(struct device* d UNUSED, vm_t* vm, fault_t* fault){ //uint32_t data = fault_get_data(fault); uint32_t data = fault_get_ctx(fault)->r1; vchan_entry_point(vm, data); // fflush(stdout); advance_fault(fault); return 0; } struct device vchan_dev = { .devid = DEV_CUSTOM, .name = "vchan-driver", .pstart = 0x2040000, .size = 0x1000, .handle_page_fault = &vchan_device_fault_handler, .priv = NULL, }; --------------------------------------------------- 2. compiled linux-tegra using buildroot (by the way the current linux-tegra is 4.9.0 which is not supported by buildroot-2016, the earliest version works for me is buildroot-2017-2), added a vmm-manager kernel driver similar to the one in camkes-x86-vm. But I changed the call_into_hypervisor() to the following: --------------------------------------------------- int call_into_hypervisor(int cmd, void *data, size_t sz, vmcall_args_t *vmcall) { int res = 0; int err; unsigned phys_ptr = virt_to_phys(vmcall); vmcall->data = data; vmcall->cmd = cmd; vmcall->phys_data = virt_to_phys(data); vmcall->size = sz; down(&hyp_sem); /* Set up arguments for the ARM hyp call */ asm volatile ("mov r0, %0; mov r1, %1" : : "r" (VMM_MANAGER_TOKEN), "r" (phys_ptr): "%r0", "%r1"); asm volatile (".arch_extension virt\n\t” "hvc #0"); asm volatile ("mov %0, r0" : "=r" (res) : : ); err = vargs->err; up(&hyp_sem); return err; } --------------------------------------------------- The kernel built and run correctly. But when I try to install the kernel driver. It crashed with following information. --------------------------------------------------- # modprobe driver.ko [81.826621] driver: loading out-of-tree module taints kernel Bad sys call from [Linux]: scone 0 at PC: 0xbf000214 Assertion failed” !err (/camkes-arm-vm/libs/libsel4arm-vmm/src/vm.c: vm_event: 407) ————————————————————————— I’m not sure if this error is triggered by the modified call_into_hypervisor() or by event_thread_run()->eventfd_signal(). Any help would be appreciated! Thanks in advance. Best Regards -Daniel Wang

2 1

IPC
by tj5527 04 Jul '18

04 Jul '18

Searching on the sel4 repository, I find there is a manual talking about IPC (https://github.com/seL4/seL4/blob/9dba8e67ccb54e207bbec22e25f21c65e5c6a45f/…) In addition to this material, where - particularly source code - would be a good start point to look into IPC design and implementation? Thanks

2 1

Status of cmake support?
by Bruce Mitchener 30 Mar '18

30 Mar '18

Hello! I've been looking at doing some builds with cmake and ninja experimentally again. Is anyone else doing this? I noticed that some bugs are being filed about warnings from clang, but I was only able to get some of the cmake + ninja stuff working when I used gcc. How are people using clang? So far, I haven't gotten a working build with cmake of sel4-tests. Is there a good way to trouble shoot this or should I post more detailed info in a thread on this list? Thanks, - Bruce

2 1

Haskell and language support
by jonas.cl＠protonmail.com 27 Mar '18

27 Mar '18

Hi, Does anyone know when the Haskell support will be released in public? In the Language support section of https://wiki.sel4.systems/Suggested%20projects is says that it will be released in the near future, but the page was last edited on June 2016. I propose that the language section also contains links to where the source can be found. I am also writing since I am working on porting the sel4-tutorial to Idris, which could be added to the list of languages, with a link to https://github.com/mokshasoft/sel4-idris-manifest There is a long way to go before it is finished, but if people want to help I accept patches. /Jonas Sent from [ProtonMail](https://protonmail.com), Swiss-based encrypted email.

2 3

OPENSSL for seL4
by Daniel Wang 27 Mar '18

27 Mar '18

Hi all, Anyone has openssl working for seL4? I compiled a version of openssl it links correctly but as soon as the code calls BIO_new_mem_buf() the system crashed with: FAULT HANDLER: data fault from vm.control (ID 0x03) on address 0xffffffb4 ,pc = 0xe259c, fsr = 0x3800006 If openssl is not available for now I wonder has anyone used other crypto library before, such as wolfssl, bearssl, etc.? Best Regards -Daniel Wang

1 0

Booting BIN abort after elfloader
by Daniel Wang 26 Mar '18

26 Mar '18

Hi all, With help from Dr. Chubb, I found there is a config to build CAmkES-ARM-VM as binary instead of ELF. However when I boot it on TK1 the process abort after loader code as follow. It is the same result when I convert ELF to BIN. Do you have any suggestion why this is happening (the paddrs and virt_entry are correct). Thank you very much! Tegra124 (TK1-SOM) # ext2load mmc 0 0x90000000 capdl-loader-experimental-image-arm-tk1-bin 31897292 bytes read in 884 ms (34.4 MiB/s) Tegra124 (TK1-SOM) # go 0x90000000 ## Starting application at 0x90000000 ... Copy monitor mode vector from 90001000 to a7f00000 size 50 Number of IRQs: 192 Load seL4 in nonsecure HYP mode 600001d3 ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3 paddr=[90000000..91e7ffff] ELF-loading image 'kernel' paddr=[80000000..8003cfff] vaddr=[e0000000..e003cfff] virt_entry=e0000000 ELF-loading image 'capdl-loader-experimental' paddr=[8003d000..81f3efff] vaddr=[10000..1f11fff] virt_entry=184f8 Enabling MMU and paging Jumping to kernel-image entry point... abort() called. Best Regards -Daniel Wang

1 0