- Devel - lists.sel4.systems

sel4test data abort when boot strap test program
by Joyce Peng(彭美僑) 19 May '17

19 May '17

Hi all, I tried to run seL4 test suite on my ARM Cortex-A7 target board. There is no error message when boot up seL4 kernel and boot strap test program on seL4 user land. But I got a “data abort” message after call sel4utils_map_page(..vaddr) and do memset(vaddr, 0, PAGE_SIZE_4K); There are some debug information list below. <1> I add debug message before the program that happen data abort diff --git a/libsel4utils/src/vspace/bootstrap.c b/libsel4utils/src/vspace/bootstrap.c index c366a35..70d378a 100644 --- a/libsel4utils/src/vspace/bootstrap.c +++ b/libsel4utils/src/vspace/bootstrap.c @@ -107,13 +107,13 @@ static void *alloc_and_map(vspace_t *vspace, size_t size) { error = sel4utils_map_page(data->vka, data->vspace_root, frame.cptr, vaddr, seL4_AllRights, 1, objects, &num); + LOG_ERROR("my-hacker\n"); if (error) { vka_free_object(data->vka, &frame); LOG_ERROR("Failed to map bootstrap frame at %p, error: %d", vaddr, error); return NULL; } + LOG_ERROR("my-hacker alloc_and_map() before memset vaddr=0x%x\n",vaddr); /* Zero the memory */ memset(vaddr, 0, PAGE_SIZE_4K); <2>Printed messages: ELF-loader started on CPU: ARM Ltd. Cortex-A7 r0p5 paddr=[20000000..2051881f] ELF-loading image 'kernel' paddr=[22000000..22032fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[22033000..22463fff] vaddr=[8000..438fff] virt_entry=15f50 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space Warning: using printf before serial is set up. This only works as your printf is backed by seL4_Debug_PutChar() alloc_and_map@bootstrap.c:111 my-hacker alloc_and_map@bootstrap.c:119 my-hacker alloc_and_map() before memset() vaddr=0xdf7fe000 <3>When happen data abort, the value of CPU registers: r1:0 r3:0xdf7fe000 lr:0xcbe8 <4>Objdump sel4test-driver. 0000cbc8 <memset>: cbc8: e3520000 cmp r2, #0 cbcc: e92d4030 push {r4, r5, lr} cbd0: 08bd8030 popeq {r4, r5, pc} cbd4: e0803002 add r3, r0, r2 cbd8: e6ef1071 uxtb r1, r1 cbdc: e3520002 cmp r2, #2 cbe0: e5431001 strb r1, [r3, #-1] cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6 It seems to write virtual address 0xdf7ff000. <5>The virtual address 0xdf7fe000 is not map in page table It seems sel4utils_map_page() not create page table for user land program correctly. Can anyone help me, how to solve this problem? Thanks! Joyce Peng(彭美僑)

4 12

seL4 on Cortex-A5
by Andrew Gacek 18 May '17

18 May '17

Is there any support for seL4 on the Cortex-A5? -Andrew

3 2

Change Access Right to Memory Pages
by Norrathep Rattanavipanon 04 May '17

04 May '17

Hello, I have some questions about how to change access rights in seL4. (I'm using native seL4, not camkes) 1) Currently, I'm using seL4_ARCH_Page_Remap to change an access right (from R/W to R/O) to a specific page (of other processes) at run-time. I'm doing as follows: seL4_CPtr frame = vspace_get_cap(&(p.vspace), p.thread.stack_top-1); // only for the stack int error = seL4_ARCH_Page_Remap(frame, ppd.cptr, seL4_CanRead, seL4_ARCH_Default_VMAttributes); Am I doing it correctly? The code seems to work fine for me but I just want to double check. 2) If my understanding in 1) is correct, the remap function only takes 1 cap at a time. So if I want to modify access rights of many pages, do I have to call the remap function multiple times? Or is there a more efficient way to do so? 3) I am also curious how the kernel handles the remap function. Does it simply flip/change some bits? Or does it involve page-related operations as well? e.g. unmap that page first and then remap the same region with a new access right? I guess it should be the former but I need to be sure about that. Thank you, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

4 7

seL4 Upgrading Issues
by Chris Guikema 03 May '17

03 May '17

Hello, I have developed an Ethernet application using CAmkES 2.2 and seL4 3.2. Because we are going to open-source the design and other documentation, I thought it would be a good idea to upgrade to the latest version of seL4 and CAmkES. I can pull the latest kernel and merge the compatible libraries with my changes and get everything to compile; however, when I load it on the board it fails... Failed to find any untyped capable of creating an object at address 0x20c4000 Failed to find a way to map address 0x20c4000 Failed to find any untyped capable of creating an object at address 0x20c8000 Failed to find a way to map address 0x20c8000 Failed to find any untyped capable of creating an object at address 0x20e0000 Failed to find a way to map address 0x20e0000 Failed to find any untyped capable of creating an object at address 0x21bc000 Failed to find a way to map address 0x21bc000 Here is my CAmkES configuration which sets up the Ethdrivers cnode and untypes. Keep in mind this works with seL4 3.2 ethdriver.simple = true; ethdriver.cnode_size_bits = 12; ethdriver.simple_untyped20_pool = 4; ethdriver.heap_size = 0; ethdriver.mmios = "0x02188000:0x4000:12, 0x021BC000:0x4000:12, 0x020E0000:0x4000:12, 0x020A4000:0x4000:12, 0x020B0000:0x4000:12, 0x020C4000:0x4000:12, 0x020C8000:0x1000:12"; Can anyone see the problem? Thanks, Chris Guikema

2 2

Re: [seL4] Memory protections within userspace and hardware/driver support
by Devin Harper 03 May '17

03 May '17

Hi, I read the whole FAQ. Does the "bug-free" protections for privacy apply to within each app of the same Linux virtual machine (overcoming memory bugs built in apps), between apps of the same Linux virtual machine (overcoming memory bugs built in the Linux kernel/GNU distro), or merely between different virtual machines (allowing any Linux kernel/GNU distro to be compromised, just not allowing them to compromise each other)? Furthermore, do I understand correctly that sel4 will only work on a few pieces of computer hardware, or will it work on everything the Linux kernel supports (has drivers for)? If sel4 will work on everything the Linux kernel supports (has drivers for), then do the same bug-free promises hold true on those hardwares in addition to the hardwares sel4 has already been tested on? Thanks!

2 1

Can I running camkes-arm-vm on HiKey board
by li94575 02 May '17

02 May '17

Hi all, Now, only exynos5 and tk1 are supported for running virtualised Linux on seL4. If I want to port it to HiKey board, is this possible?

3 2

questions about TK1 VM
by PX 01 May '17

01 May '17

Hi, all I have some questions about TK1 VM. I want to save the execution status of the TK1 VM. First, I stop the VM, then I use the function, seL4_TCB_ReadRegisters() to read the VM's registers into a buffer. Here are my questions: 1. Before I call the function, seL4_TCB_ReadRegisters(), do I need to flush TLB of CPU? If so, where is the library I need to check for this function? 2. The register values in the structure, seL4_UserContext, are VMM's physical addresses or virtual addresses? Best wishes Peng

2 1

sel4test failing TEST_SCHED0004 on iMX6
by Robert Kaiser 19 Apr '17

19 Apr '17

Hi all, I just tried to run the test suite on iMX6. Using the current version from github, I got this result: ---------------------------- ..... Test suite failed. 200/202 tests passed. 200/202 tests passed. *** FAILURES DETECTED *** ---------------------------- Further checking into the log shows this: ---------------------------- ..... Starting test 51: TEST_SCHED0004 TEST_SCHED0004 Running test SCHED0004 (Test threads at all priorities) _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark vka_alloc_object_at_maybe_dev@object.h:46 Failed to allocate cslot: error 1 new_pages_at_vaddr@vspace.c:331 Failed to allocate page sel4utils_configure_thread_config@thread.c:77 ipc buffer allocation failed Assertion failed: error == 0 ([.....]/seL4test/apps/sel4test-tests/src/helpers.c: create_helper_thread: 346) Failure: result == SUCCESS at line 343 of file [.....]/seL4test/apps/sel4test-driver/src/main.c Failure: Test check failure (see log). at line 0 of file ..... ---------------------------- The same test is run a second time further down below the log, giving the same result. I tested this on two different IMX6 platforms (SabreLite and Wandboard). Both showed identical results. Is this a known problem? Cheers Robert -- Robert Kaiser Technische Informatik Hochschule RheinMain Wiesbaden Rüsselsheim Computer Engineering RheinMain University of Applied Sciences robert.kaiser(a)hs-rm.de http://www.cs.hs-rm.de/~kaiser tel:(+49)611-9495-1292 fax:(+49)611-9495-1210 Postanschrift/Postal Address: Robert Kaiser, Hochschule RheinMain, FB DCSM/Informatik Unter den Eichen 5, 65195 Wiesbaden, Germany

2 2

smaccm/sel4arm-vmm-manifest complie problem
by 高文博 18 Apr '17

18 Apr '17

hi everyone! i am doing research about sel4.i used https://github.com/smaccm/sel4arm-vmm-manifest code. and complie it.than it build out kernel.elf only. but where is linux? expecting your answers. thanks very much! gao. -- 高文博数据通信科学技术研究所

2 1

smaccm/sel4arm-vmm-manifest compile problem
by 高文博 14 Apr '17

14 Apr '17

hi everyone! i am doing research about sel4.i used https://github.com/smaccm/sel4arm-vmm-manifest code. and compile it.than it build out kernel.elf only. but where is linux? expecting your answers. thanks very much! gao.

1 0