- Devel - lists.sel4.systems

Error while building in docker
by Edward Sandberg 09 Jan '20

09 Jan '20

This morning I saw this error when building sel4: /bin/sh: 1: PROTOBUF_PROTOC_EXECUTABLE-NOTFOUND: not found I noticed a warning when starting the docker container about trustworthysystems/camkes:latest being over 30 days old. I thought that using an up to date pull of: https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git would keep the build env up to date but that apparently is either not the case or there is a problem with the repo. I ran: docker pull trustworthysystems/camkes … [View More]

2 1

fastpath performance test
by Dd Nirvana 05 Jan '20

05 Jan '20

Hi guys, I have downloaded the lastest seL4 repo and built the seL4 kernel. And I reuse the code in sel4test/projects/sel4test/apps/sel4test-tests/src/tests/ipc.c. To test the fast, I made minor modifications: first, set caller and callee to the same priority; second, caller uses seL4_Call while callee uses seL4_ReplyRecv. However, the fastpath takes more than 2000 cycles (a round trip). Build: use the lastest provided docker and ../init-build.sh - DPLATFORM=… [View More]

2 1

Understand seL4 x86_64 Kernel ABI calling convention
by Alexandre Mutel 03 Jan '20

03 Jan '20

Hello! While looking at the code base and checking generated code, I'm not sure about the pertinence of having a different ABI from user System V ABI for kernel calls, as it is implying a bit more unnecessary register shuffling, and I was wondering why this choice was made to have r10, r8, r9, r15? instead of keeping System V ABI and just replace rcx by r10 as it is discarded by syscall: SystemVABI_x86_64_user: rdi, rsi, rdx, rcx, r8, r9 SystemVABI_x86_64_Linux_kernel: rdi, rsi, rdx,… [View More]

1 1

Hardware-aided Trusted Computing devroom at FOSDEM
by Vasily A. Sartakov 01 Jan '20

01 Jan '20

Hello I would like to invite your to participate in a new devroom: Hardware-aided Trusted Computing. The devroom is devoted to open source projects on top of modern TEEs like Intel SGX, AMD SEV/SVE, Arm TrustZone. You can find the schedule here: https://fosdem.org/2020/schedule/track/hardware_aided_trusted_computing/ I hope this will be interesting for the community. See you at FOSDEM. -- Dr.-Eng. V. A. Sartakov

2 1

some question about the compile of global-components in camkes_arm_vm project
by yadong.li 28 Dec '19

28 Dec '19

hi， I have some question about the compile of global-components in camkes_arm_vm project. 1、In projects/global-components/components, there are some directory include FileServer, SerialServer, TimeServer and the others. I found FileServer had been compiled to project， but the other directory have not been compiled Is there some on-off switch control the compile ？ But I did not find it. 2、The CAmkES of FileServer component did not have a "int run(void) {}, If I want to add an new … [View More]

1 0

Camkes Project on Sabre Lite i.mx6 board
by Parvaneh Ahgajani 19 Dec '19

19 Dec '19

Hello all, I am trying to have my own seL4 demo on Sabre Lite board. I am using this command to create the image file: ../init-build.sh -DPLATFORM=sabre -DCROSS_COMPILER_PREFIX=arm-linux-gnueabi- -DCAMKES_APP=adder After that I run this commands to boot the image: fatload mmc 1 0x41000000 adder(image file) The bootm command gives this error: Wrong Image Format for bootm command ERROR: can't get kernel image! I tried bootelf but it stuck and does not show the correct answer: bootelf … [View More]

2 1

Blog on seL4 licensing
by Heiser, Gernot (Data61, Kensington NSW) 10 Dec '19

10 Dec '19

The question of what the seL4 license actually means, in particular, to which degree it may force deployer’s IP to be open-sourced (*), has come up repeatedly, and from informal discussions I realised that misconceptions abound. I tried to clear up such confusion in a blog that I just posted: https://microkerneldude.wordpress.com/2019/12/09/what-does-sel4s-license-im… Enjoy, Gernot (*) short answer: normally not at all!

1 0

try to add vm in zynqmp, but when run rootserve crash.
by yadong.li 03 Dec '19

03 Dec '19

hi： I try add vm in zynqmp, but when run rootserve crash. print See appendix for the log Function call stack create_objects for (int ut_index = 0; ut_index < spec->num_untyped; ut_index++) { .... CDL_Object *obj = &spec->objects[obj_id]; CDL_ObjectType capdl_obj_type = CDL_Obj_Type(obj); ----case crash } I fount when it access 0x440010 (the 42th of … [View More]

1 0

Userspace debugging with QEMU/gdb
by Jiusheng Liu 02 Dec '19

02 Dec '19

Hi, >From the page https://docs.sel4.systems/DebuggingGuide.html (section Userspace debugging), I know we can debug userspace process by command below: ---------------------------- cmd example start ---------------------------------------- gdb ./dynamic-2 Reading symbols from ./dynamic-2...done. (gdb) target remote :1234 Remote debugging using :1234 0x000000000000fff0 in ?? () (gdb) break main Breakpoint 1 at 0x402011: file sel4-tutorials-manifest/dynamic-2/main.c, line 161. (gdb) c … [View More]

2 2

Re: [seL4] Devel Digest, Vol 66, Issue 26
by Millar, Curtis (Data61, Kensington NSW) 26 Nov '19

26 Nov '19

> As I'm playing with a prototype language and OS while building it on > top of seL4, > I'm not using any intermediate C layers to connect to the seL4 API (so > custom build and > integration and no C runtime), while most of the samples out there are > heavily relying on > some foundations, which is completely understandable, considering how > it can be involving > to build anything relevant on top of the seL4 API. > So as I'm just really getting started to … [View More]

1 0