- Devel - lists.sel4.systems

Combined Ada and C project with Kbuild
by Noah Kennedy 08 Aug '18

08 Aug '18

I'm currently working on a project that is using the old Kbuild system. The project has been primarily implemented in C, however we would like to integrate some Ada code into the project. I am familiar with how to use gcc and makefiles to build polyglot projects on linux, however, I have no idea how to do so with the Kbuild system, as I cannot find out how to build anything other than .c or .h files with the makefile. How would I go about adding ada code to the project? Is there any way for me to build .ads and .adb, or .a files with the makefile?

2 1

camkes-project error
by talos 07 Aug '18

07 Aug '18

Hi, When I followed this tutorial: https://sel4.systems/Info/CAmkES/GettingStarted.pml The error is: /home/talos/camkes-project/build/arm/imx31/simple/src/echo/generated/camkes.o: In function `post_main': /home/talos/camkes-project/build/arm/imx31/simple/src/echo/generated/camkes.c:601: undefined reference to `component_control_main' collect2: error: ld returned 1 exit status /home/talos/camkes-project/build/arm/imx31/simple/camkes-gen.mk:630: recipe for target 'echo.instance.bin' failed make[1]: *** [echo.instance.bin] Error 1 tools/common/project.mk:333: recipe for target 'simple' failed make: *** [simple] Error 2 But when I followed this tutorial: https://docs.sel4.systems/CAmkES/ the error is: [230/232] Building C object elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj FAILED: /usr/bin/arm-none-eabi-gcc --sysroot=/home/talos/camkes-project/build -DHAVE_AUTOCONF -I../tools/seL4/elfloader-tool/include -I../tools/seL4/elfloader-tool/include/plat/imx6 -I../tools/seL4/elfloader-tool/include/arch-arm -I../tools/seL4/elfloader-tool/include/arch-arm/32 -I../tools/seL4/elfloader-tool/include/arch-arm/armv/armv7-a -I../tools/seL4/elfloader-tool/include/arch-arm/armv/armv7-a/32 -Iautoconf -Ikernel/gen_config -Ielfloader-tool/gen_config -Ilibsel4/gen_config -Iprojects/camkes/gen_config -Iprojects/capdl/capdl-loader-app/gen_config -Iprojects/rumprun/gen_config -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -Iprojects/seL4_libs/libsel4platsupport/gen_config -Iprojects/seL4_libs/libsel4serialserver/gen_config -Iprojects/seL4_libs/libsel4debug/gen_config -Iprojects/seL4_libs/libsel4test/gen_config -Iprojects/seL4_libs/libsel4muslcsys/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Iprojects/util_libs/libutils/gen_config -Iprojects/util_libs/libplatsupport/gen_config -Iprojects/util_libs/libethdrivers/gen_config -I../projects/util_libs/libcpio/include -march=armv7-a -marm -D__KERNEL_32__ -g -D_XOPEN_SOURCE=700 -ffreestanding -Wall -Werror -W -Wextra -fno-pic -fno-pie -MD -MT elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj -MF elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj.d -o elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj -c ../tools/seL4/elfloader-tool/src/string.c ../tools/seL4/elfloader-tool/src/string.c:97:29: error: expected ';', ',' or ')' before 'dest' void *memcpy(void *restrict dest, const void *restrict src, size_t n) ^ ninja: build stopped: subcommand failed. I used Ubuntu 16.04 x86_64 Thanks

3 2

How to write safe C code for free?
by Wean Irdeh 05 Aug '18

05 Aug '18

Hello. I'm a poor person looking for an advice. I know this is the right place since all of you have huge expertise in formal verification. I'm not a smart person (maybe I'm stupid), but I'm interested in open source contribution using C language. Is there any solution to write C code free from undefined behavior and vulnerability without paying for any tools?

3 2

using libmuslc library question
by Leonid Meyerovich 03 Aug '18

03 Aug '18

Hello, I have tried to call usleep() function from seL4 'main' thread and it crashes the system with error: Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on code at address 0x200 with status 0x82000006 in thread 0xff807bfe2200 "rootserver" at address 0x200 With stack: How to use this library? Thank you, Leonid

1 0

about compile error
by wong xuguo 03 Aug '18

03 Aug '18

Dear Sir/Lady, This is a student from china, I am very interested in the sel4, works on the camkes, When I first compile the project camkes, I met a problem: camkes.c:502: undefined reference to `component_control_main' I know this means it not implemented this function, but this function seems produced by a auto method, so could you tell how to solve this problem? I follow the command: https://docs.sel4.systems/CAmkES/ to compile the : repo init -u https://github.com/seL4/camkes-manifest.git

2 1

Question on multi-partition seL4 image/load for x86
by Jim Marek 02 Aug '18

02 Aug '18

seL4 Developers/SMEs: Does anyone have a seL4 load/configuration that includes more than 2 partitions with at least 2 of the partitions each having a dedicated Ethernet interface assigned to it? I am focused on an x86 host platform. Currently I have a Dell 7910 19" rack unit I am wanting to host on and it has 4 Ethernet ports. Thanks, Jim Marek Enterprise Architect Rockwell Collins

2 3

Question about wrapper files
by Holm, Elinor M 30 Jul '18

30 Jul '18

I built sel4test using the init-build.sh command with -DPLATFORM=x86_64 and -DSIMULATION=TRUE and then ran ninja. I'm using QEMU as my emulator. Within the build directory I created, there's a kernel directory. In that directory, there are a bunch of C files with names that include "wrapper." For instance, there's a file named kernel_all_pp_prune_wrapper_temp.c. I'm having trouble understanding what the wrapper files do. Are there for testing, or something else? Elinor Holm Software Engineer 781-410-5221 This message and/or attachments may include information subject to GDC4S S.P. 1.8.6 and GD Corporate Policy 07-105 and are intended to be accessed only by authorized recipients. Use, storage and transmission are governed by General Dynamics and its policies. Contractual restrictions apply to third parties. Recipients should refer to the policies or contract to determine proper handling. Unauthorized review, use, disclosure or distribution is prohibited. If you are not an intended recipient, please contact the sender and destroy all copies of the original message.

3 2

CAmkES 3.5.0 Build Error
by Amit Goyal 28 Jul '18

28 Jul '18

Hi, I am running CAmkES 3.5.0 on Ubuntu 16.04, 64 Bit, i5 machine, CMake 3.11.4. I am getting the following error on running ../init --plat pc99 --tut hello-camkes-1 --solution (although seL4 10.0.0 works perfectly fine). ------------------------------------------------------------------------------------------------------------------------------- Traceback (most recent call last): File "../init", line 76, in <module> sys.exit(main()) File "../init", line 62, in main result = common.init_build_directory(args.plat, args.tut, args.solution, os.getcwd()) File "/home/akshat/Desktop/sel4_10.0/try/camkes-tutorials-manifest/projects/sel4-tutorials/common.py", line 58, in init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 774, in __init__ self.wait() File "/usr/local/lib/python2.7/dist-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL=hello-camkes-1 -DBUILD_SOLUTIONS=TRUE .. STDOUT: -- The C compiler identification is GNU 5.3.1 -- The CXX compiler identification is GNU 5.3.1 -- Check for working C compiler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Check for working CXX compiler: /usr/bin/g++ -- Check for working CXX compiler: /usr/bin/g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc -- Performing test HARD_FLOAT with flags -mfloat-abi=hard -- Test HARD_FLOAT FA... (295 more, please see e.stdout) STDERR: CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:16 (include) CMakeLists.txt:21 (include) CMake Error at tools/camkes/camkes.cmake:581 (message): Failed to generate camkes-gen.cmake: Traceback (most recent call last): File "/usr/lib/python2.7/runpy.py", line 174, in _run_module_as_main "__main__", fname, loader, pkg_name) File "/usr/lib/python2.7/runpy.py", line 72, in _run_code exec code in run_globals File "/home/akshat/Desktop/sel4_10.0/try/camkes-tutorials-manifest/tools/camkes/camkes/runner/__main__.py", lin... (614 more, please see e.stderr) -------------------------------------------------------------------------------------------------------------------------------- Can you please suggest a way around? -- Thanks and Regards, Amit Goyal

2 2

Question about wrapper files
by Holm, Elinor M 27 Jul '18

27 Jul '18

I built sel4test using the init-build.sh command with -DPLATFORM=x86_64 and -DSIMULATION=TRUE and then ran ninja. I'm using QEMU as my emulator. Within the build directory I created, there's a kernel directory. In that directory, there are a bunch of C files with names that include "wrapper." For instance, there's a file named kernel_all_pp_prune_wrapper_temp.c. I'm having trouble understanding what the wrapper files do. Are they for testing, or something else? Elinor Holm

1 0

Image lies outside of usable physical memory v2
by Jeremy Fields 26 Jul '18

26 Jul '18

http://sel4.systems/pipermail/devel/2016-July/000918.html I'm running into the same issue, with likely the same cause. I wanted to see if there is any further insight that can be given on this? I'm guessing there hasn't been any updates to seL4's memory allocation in this aspect. (I'm using seL4 9.0.1) My naive attempt of commenting out that particular check in seL4 just results in the machine hard resetting when it runs (if only it were that easy). >Unfortunately I cannot say that we will get around to fixing this in a particularly timely manner. (2016) Any chance this is on a roadmap? -- Sincerely, Jeremy ______________________________ Software Engineer Critical Technologies Inc.

2 1

Implementing a Filesystem on CAmkES
by Grant Jurgensen 25 Jul '18

25 Jul '18

Hello all, I was hoping to get some advice on how to implement a filesystem on my CAmkES project. For now I'm targeting FAT32, but that is flexible. So far, my plan is to port the libsdhcdriver to my platform (which shouldn't be too bad. I'm targeting exynos5, and I see exynos4 is already supported). After that, I assume I'm on my own when it comes to creating a filesystem interface. Perhaps there is an existing library for this that can hook into any standard SD controller implementation? Finally, is there an easy way to integrate said filesystem into musllibc such that one could use the standard open/read/write/close functions? Does this sound like the best way to go, or am I missing a simpler solution? Thanks, Grant

3 2

Re: [seL4] Understanding how SEL4 recognises UART on board
by Sathya Narayanan N 19 Jul '18

19 Jul '18

Hi Experts, I am curious to know how SEL4 recognises the existence of UART on the board and mapped to a particular memory address. I see there is no DTB/ DTS files read from memory. could someone help me understand the concept here ? Or is it something hardcoded in the kernel ? -- regards, Sathya

2 1

RISC-V - sel4test and sel4bench running on SiFive's Unleashed Platform
by Hesham Almatary 19 Jul '18

19 Jul '18

Hi everyone, I pushed my local seL4/RISC-V work to GitHub which contains the following new features: * A new option to run seL4 in machine mode. * A port of seL4 to QEMU's SiFiveU and virt platforms. * DTB parsing in seL4 to read and use UARTs when available. * Ported seL4 to run on VC707 FPGA Freedom Unleashed platform. * Initial Benchmarking support in seL4. * Initial sel4bench port that can measure IPC and trap timing. Link for more details: http://heshamelmatary.blogspot.com/2018/07/new-sel4test-and-sel4bench-relea… -- Hesham

1 0

Porting sel4 on RISCV architecture
by Sathya Narayanan N 16 Jul '18

16 Jul '18

Hi Experts, This is Sathya from IIT Madras. We are working on porting SEL4 on RISCV architecture running on FPGA. We have ported linux on the FPGA. I have some doubts regarding OS porting. I am stuck at the end. Before my actual query, let me tell my platform. Hardware - 64 bit RISCV design running on FPGA. It doesn't support compressed instn and multiarch. Operating system - SEL4, repo synced from latest official repository. Tools - Latest synched from RISCV official repo. Query - I simulated sel4test on spike and then I am trying to port it on FPGA. We have UART to be mapped to 0x11400 address location. I set scan->reg to this value. I understood, incase of simulation, the DTB argument passed to init_first_hart function comes from spike simulator (file - sim.cc). Now, for FPGA I want to pass the DTB value to the init_first_hart() function. I am planning to write a DTS file and somehow read the data from DTS file here. I am trying to know, what is the right method to do for SEL4 ? Can you please let me understand, how you went ahead for SEL4 ? Is there any changes, I have to do in the repo code ? any readings would you suggest to proceed ahead ? -- regards, Sathya

3 4

Re: [seL4] How to write safe C code for free?
by Wean Irdeh 14 Jul '18

14 Jul '18

Thanks again for the reply. I was looking for the foolproof way to write safe C code, but seems like the best way to go forward is to carefully design and code. Your advice is helpful to me. On Friday, July 13, 2018, Dean Pucsek <dean(a)lightbulbone.com> wrote: > >> Clang does have a static analyzer builtin that can be help in some > cases. That being said, the best way forward is for you as a developer to > understand the types of code that can lead to problems and not rely > entirely on a static analyzer. > > >>> >>> >

1 0

Re: [seL4] How to write safe C code for free?
by Wean Irdeh 14 Jul '18

14 Jul '18

Thanks a lot for the reply. What is your opinion on static checking tool and safe subset of C? Does that help? On Friday, July 13, 2018, Dean Pucsek <dean(a)lightbulbone.com> wrote: > Hello Wean, > > It is certainly possible to learn how to program in C without spending any > money; all it requires is a basic toolchain and a willingness to learn. > don't sell yourself short by hinting that you might be "stupid" (you almost > certainly aren't). > > In order to get started with C I suggest setting up an environment to > experiment in; for that look into installing LLVM/Clang ( > http://releases.llvm.org/) there are pre-built binaries for most major > operating systems. Once that is done all you need is a text editor (Notepad > on Windows or one of the other many free options) and some patience. As for > tutorials and resources, some options are: > > - Searching on Google for "c tutorial"; one result that looks interesting > is http://www.learn-c.org/. > - Finding an open source project that interests you and trying to > understand the code then implement a change. > - While not free, may people swear by the K&R book as a great resource to > start. > > In terms of writing code that is free of undefined behaviour and > vulnerabilities your best bet is to learn what code constructs cause those > to occur and how to avoid them. A great book for this is The Art of > Software Security Assessment by Mark Dowd, there is a PDF of Chapter 6 (C > Language Issues) available at https://trailofbits.github.io/ > ctf/vulnerabilities/references/Dowd_ch06.pdf. > > Learning about C, undefined behaviour, and vulnerabilities doesn't happen > overnight so be patient and enjoy the journey. > > --Dean > > > >

1 0

Help ! Simulating SEL4 with Zero testcases running
by Sathya Narayanan N 13 Jul '18

13 Jul '18

Hi Experts, I am running sel4 simulation on spike. I want to disable test cases from running. I tried setting default value "" from ".*" in Kconfig file. Is this enough ? Or is something else to be done ? -- regards, Sathya

2 2

Re: [seL4] sel4test cross compiling for arm
by Kofidoku.Atuah＠data61.csiro.au 13 Jul '18

13 Jul '18

?Hey Thad, Thanks for catching that: it turns out that we weren't passing -nostdlib to the linker when linking the ELFLoader, so the cross-toolchain's linker was trying to link the ELFLoader against the cross toolchain's libc, but it shouldn't be doing that and it should instead be using our libmuslc. A fix has been pushed out and you should be seeing it shortly. Thanks for your patience, -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

seL4 vm examples with Qemu
by Mike Clark 12 Jul '18

12 Jul '18

Is it currently possible to boot the camkes-vm-example applications using qemu? I followed the directions here (https://github.com/seL4/camkes-vm-examples) to get a build of the minimal application. I then tried to follow the directions here ( https://docs.sel4.systems/Hardware/Qemu/#running-qemu) to boot using qemu. Unfortunately I get an error when trying to boot. The error says: *"seL4 caled fail at /host/camkes_vm/kernel/src/arch/x86/kernel/boot_sys.c:785 in function boot_sys, saying "boot_sys failed for some reason :("* *halting...* *Kernel entry via Interrupt, irq 0* I'm running this on a ubuntu 16.04 machine with an Intel i5-4200U ( https://ark.intel.com/products/75459/Intel-Core-i5-4200U-Processor-3M-Cache… ). Thanks!

2 1

Re: [seL4] Memory Region overlap error
by Jeremy Fields 12 Jul '18

12 Jul '18

> > > On 11.07.2018 01:45, Jeremy Fields wrote: > > Here's my results from these permutations, using Genode 18.05 / sel4 > 9.0.1 > > (hopefully the formatting works). I know some permutations probably don't > > make sense, but I did them anyways. Any thoughts? I have the serial > output > > from these tests as well, but didn't want to overload this message with > > that. Additionally, can you folks share specific machine make/models that > > you know work with Genode/seL4? Hopefully some 'consumer off the shelf' > > stuff. > > We have no specific Genode/seL4 x86 hardware list, but there exists an > unofficial list at [0] which may serve your question. > > > PermuationResult > > Legacy / Multiboot 2 + Bender Memory region overlap > > Legacy / Multiboot 1 + Bender failed assertion > > 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) > > Legacy / Multiboot 1 crashes/reboots > > Legacy / Multiboot 2 Memory region overlap > > UEFI / Multiboot 2 + Bender Memory region overlap > > UEFI / Multiboot 1 + Bender failed assertion > > 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) > > UEFI / Multiboot 1 freezes? > > UEFI / Multiboot 2 Memory region overlap > > Thanks for testing. > > May you please apply the seL4 kernel patch and test, whether this solves > your issue ? > > > [0] http://usr.sysret.de/jws/genode/hcl.html > > -- > 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 1

Re: [seL4] Memory Region overlap error
by Jeremy Fields 11 Jul '18

11 Jul '18

> > Hello, > > On 05.07.2018 14:34, Jeremy Fields wrote: > > Sure - I've tried a few different combinations, but the latest Genode 18.5 > > used seL4 9.0.1. I'm attempting to use this on an x86 machine that has a > > Xeon 1607 and a dedicated GPU. The thread I referenced in my initial post > > implied that UEFI might be an issue, but I've tried both UEFI and legacy > > boots without success. I tried using/building Genode 17.5 with whatever > > version of seL4 it acquires, but get the same error. Let me know if there's > > anything else I can provide > > some suggestions from my side. > > Try to remove the chain bootloader "bender", just to exclude it as > potential reason of trouble. In genode/tool/run/boot_dir/sel4 remove the > "multiboot2 /boot/bender ..." line and adjust the line below from > "module2 /boot/sel4 ..." -> "multiboot2 /boot/sel4 ...". Use some simple > scenario for testing, like log.run > > If the issue persists, you may try to boot Genode/seL4 the Multiboot 1 > way instead of Multiboot 2, which however will solely work for BIOS > legacy boots (no UEFI). Replace the "multiboot2" and "module2" in > genode/tool/run/boot_dir/sel4 with "multiboot" and "module". > > > Cheers, > > Alex B. > > -- > 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 > Here's my results from these permutations, using Genode 18.05 / sel4 9.0.1 (hopefully the formatting works). I know some permutations probably don't make sense, but I did them anyways. Any thoughts? I have the serial output from these tests as well, but didn't want to overload this message with that. Additionally, can you folks share specific machine make/models that you know work with Genode/seL4? Hopefully some 'consumer off the shelf' stuff. PermuationResult Legacy / Multiboot 2 + Bender Memory region overlap Legacy / Multiboot 1 + Bender failed assertion 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) Legacy / Multiboot 1 crashes/reboots Legacy / Multiboot 2 Memory region overlap UEFI / Multiboot 2 + Bender Memory region overlap UEFI / Multiboot 1 + Bender failed assertion 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) UEFI / Multiboot 1 freezes? UEFI / Multiboot 2 Memory region overlap -- Sincerely, Jeremy ______________________________ Software Engineer Critical Technologies Inc.

2 1

Re: [seL4] sel4test cross compiling for arm
by Kofidoku.Atuah＠data61.csiro.au 11 Jul '18

11 Jul '18

Sorry Thad, I want to correct something I said: I recommended that you try the arm-linux-gnueabihf toolchain, but that should have been the arm-linux-gnueabi toolchain. Aside from that, I went and double checked, and this toolchain works just fine -- one thing to note though, is that you don't have to specify the -DCROSS_COMPILER_PREFIX=foo option, and you should be able to just use -DAARCH32=1 and our build system should automatically select the right toolchain to invoke for you (see: https://github.com/seL4/seL4/blob/master/gcc.cmake#L24?) Feel free to ask more questions about the new build system since we expect adaptation to take some time. -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

ninja build tool error
by 송대영 11 Jul '18

11 Jul '18

Hello, I have question about sel4's new ninja build tool. *1. From now on, sel4-tutorials use ninja build tool, so I repo new sel4-tutorials.Last step, I executue this command "../init-build.sh --plat pc99 --tut hello-1" but It prints with this error messages.What's the problem?---------------------------------------------------------------------------------------------CMake Warning at tools/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does notCall Stack (most recent call first): tools/cmake-tool/base.cmake:58 (include) tools/cmake-tool/all.cmake:16 (include) CMakeLists.txt:23 (include)CMake Error at projects/sel4-tutorials/CMakeLists.txt:34 (message): You must select a tutorial for compilation. Select using -DTUTORIAL=<PREFERENCE>. Choose one of hello-1;hello-2;hello-2-nolibs;hello-3;hello-3-nolibs;hello-4;hello-4-app;hello-timer;hello-timer-client.-- Configuring incomplete, errors occurred!See also "/home/scribnote5/sel4-tutorials-manifest/build_hello_1/CMakeFiles/CMakeOutput.log".2. How can I build sel4 ia32 images in sel4bench?This command "../init-build.sh -DPLATFORM=ia32 -DHARDWARE=TRUE -DAARCH32=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUE" doesn't make sel4bench image file.*

2 1

sel4test cross compiling for arm
by Thad Seeberger 11 Jul '18

11 Jul '18

Good day. Trying to build first test and run on qemu. Cmake failing to compile the test program. Does this with different versions of cross compile. Can someone point me in the right direction of where to start looking. thx Thad localhost build-arm]# ../init-build.sh -DCROSS_COMPILER_PREFIX=arm-none-eabi- -DPLATFORM=kzm -- The C compiler identification is GNU 7.3.1 -- The CXX compiler identification is GNU 7.3.1 -- Check for working C compiler: /opt/arm/bin/arm-none-eabi-gcc -- Check for working C compiler: /opt/arm/bin/arm-none-eabi-gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Check for working CXX compiler: /opt/arm/bin/arm-none-eabi-g++ -- Check for working CXX compiler: /opt/arm/bin/arm-none-eabi-g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /opt/arm/bin/arm-none-eabi-gcc -- Performing test HARD_FLOAT with flags -mfloat-abi=hard -- Test HARD_FLOAT FAILED -- Performing test SOFTFP_FLOAT with flags -mfloat-abi=softfp -- Test SOFTFP_FLOAT FAILED CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:16 (include) CMakeLists.txt:21 (include) -- Configuring done -- Generating done -- Build files have been written to: /home/maddthad/seL4test/build-arm -- Performing test SOFT_FLOAT with flags -mfloat-abi=soft -- Test SOFT_FLOAT FAILED CMake Error at tools/seL4/cmake-tool/flags.cmake:135 (message): Kernel does not support hardware floating point but toolchain cannot build software floating point Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:16 (include) CMakeLists.txt:21 (include) -- Configuring incomplete, errors occurred! See also "/home/maddthad/seL4test/build-arm/CMakeFiles/CMakeOutput.log". See also "/home/maddthad/seL4test/build-arm/CMakeFiles/CMakeError.log". CMakeError.log: compiling the C compiler identification source file "CMakeCCompilerId.c" failed. Compiler: /opt/arm/bin/arm-none-eabi-gcc Build flags: Id flags: The output was: 1 /opt/gcc-arm-none-eabi-7-2018-q2-update/bin/../lib/gcc/arm-none-eabi/7.3.1/../../../../arm-none-eabi/lib/libc.a(lib_a-exit.o): In function `exit': exit.c:(.text.exit+0x2c): undefined reference to `_exit' collect2: error: ld returned 1 exit status Compiling the CXX compiler identification source file "CMakeCXXCompilerId.cpp" failed. Compiler: /opt/arm/bin/arm-none-eabi-g++ Build flags: Id flags: The output was: 1 /opt/gcc-arm-none-eabi-7-2018-q2-update/bin/../lib/gcc/arm-none-eabi/7.3.1/../../../../arm-none-eabi/lib/libc.a(lib_a-exit.o): In function `exit': exit.c:(.text.exit+0x2c): undefined reference to `_exit' collect2: error: ld returned 1 exit status

2 1

Future plans w.r.t. Cortex-R
by piotr＠skrzypek.eu 10 Jul '18

10 Jul '18

Dear seL4 Maintainers, Could you please share what are your future support plans w.r.t. ARM Cortex-R family - the 'reliable' and 'real-time' side of ARM portfolio? Cortex-R implementations include interesting safety features i.a. lockstep processing. It feels like a good match for seL4 safety-oriented philosophy. However, Cortex-R processors have MPU instead of MMU, which seems to be ruling them out for now. Are there any plans to have an seL4 'MPU' branch in order to support these kind of processors? Thank you in advance, Piotr Skrzypek

3 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

sel4 qemu x86 runtime error
by Thad Seeberger 10 Jul '18

10 Jul '18

Compile now no problem however I'm getting error when running. I believe its an invalid opcode exception. I think my build not matching the qemu but I've tried diff machines and they do the same. I also get this warning during build, not sure if this relevant: Warning: Installation path /home/maddthad/camkes-tutorials-manifest/projects/capdl/capDL-tool not found on the PATH environment variable. make: Leaving directory `/home/maddthad/camkes-tutorials-manifest/projects/capdl/capDL-tool' Qemu commanr, lines with ????? suspect: qemu-system-i386 -nographic -m 512 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99 (process:98550): GLib-WARNING **: gmem.c:483: custom memory allocation vtable not supported Boot config: parsing cmdline 'images/kernel-ia32-pc99 ' Boot config: console_port = 0x3f8 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false ???? Warning: Your kernel was not compiled for the current microarchitecture. Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 1fefe000 type 1 Adding physical memory region 0x100000-0x1f800000 Physical Memory Region from 1fffe000 size 2000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 Multiboot gave us no video information Kernel loaded to: start=0x100000 end=0x160000 size=0x60000 entry=0x10005e ACPI: RSDP paddr=0xf7180 ACPI: RSDP vaddr=0xdfcf7180 ACPI: RSDT paddr=0x1ffffbc1 ACPI: RSDT vaddr=0xdffffbc1 ACPI: FADT paddr=0x1ffff1c0 ACPI: FADT vaddr=0xdffff1c0 ACPI: FADT flags=0x80a5 ACPI: 0 IOMMUs detected ACPI: MADT paddr=0x1ffffb11 ACPI: MADT vaddr=0xdffffb11 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd ACPI: 1 CPU(s) detected Detected 1 IOAPICs, but configured to use PIC instead Detected 1 boot module(s): module #0: start=0x161000 end=0x25aed0 size=0xf9ed0 name='images/capdl-loader-experimental-image-ia32-pc99' ELF-loading userland images from boot modules: size=0x189000 v_entry=0x804f544 v_start=0x8048000 v_end=0x81d1000 p_start=0x25b000 p_end=0x3e4000 Moving loaded userland images to final location: from=0x25b000 to=0x160000 size=0x189000 Starting node #0 with APIC ID 0 Booting all finished, dropped to user space Caught cap fault in send phase at address 0x0 while trying to handle: ?????? user exception 0x6 code 0x0 in thread 0xff3f5d00 "rootserver" at address 0x805130e With stack: 0x80cfda0: 0x0 0x80cfda4: 0x0 0x80cfda8: 0x0 0x80cfdac: 0x0 0x80cfdb0: 0x0 0x80cfdb4: 0x0 0x80cfdb8: 0x0 0x80cfdbc: 0x0 0x80cfdc0: 0x0 0x80cfdc4: 0x0 0x80cfdc8: 0x0 0x80cfdcc: 0x0 0x80cfdd0: 0x0 0x80cfdd4: 0x0 0x80cfdd8: 0x0 0x80cfddc: 0x0 QEMU: Terminated Have a great day.

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

reading thread registers
by Michael Neises 10 Jul '18

10 Jul '18

Hello, I know there exists a function seL4_TCB_ReadRegisters, which can read the registers of a certain thread, given a/the capability to the thread. Ultimately, I'm interested in reading memory at runtime to determine whether the data I expect is present. So I'm wondering, is there in seL4 an init process, whose registers contain all the working memory of the system? And furthermore, how can I access a capability to a given thread in order to pass it into the ReadRegisters function mentioned above? Cheers, Michael

2 1

Memory Region overlap error
by Jeremy Fields 09 Jul '18

09 Jul '18

Hello- I'm trying to boot Genode/seL4 on hardware. I've tried a few different combinations of versions, and GRUB configurations, without success. I keep getting the same error despite these different combinations There was a thread that touched on this, but I couldn't find any resolution http://sel4.systems/pipermail/devel/2017-December/001776.html @##################################### Bender: Hello World. framebuffer at [b8000+b8fa0) 80x25@16 warning - unknown framebuffer type framebuffer at [b8000+b8fa0) 80x25@16 warning - unknown framebuffer type 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=0xf8f0000 end=0xffff228 size=0x70f228 name='image.elf' Physical Memory Region from 0 size 9ac00 type 1 Physical Memory Region from 9ac00 size 5400 type 2 Physical Memory Region from e0000 size 20000 type 2 Physical Memory Region from 100000 size 18dbb000 type 1 Adding physical memory region 0x100000-0x18ebb000 Physical Memory Region from 18ebb000 size 12d000 type 4 Physical Memory Region from 18fe8000 size 1000 type 1 Adding physical memory region 0x18fe8000-0x18fe9000 Physical Memory Region from 18fe9000 size 17000 type 4 Physical Memory Region from 19000000 size 4ffd000 type 1 Adding physical memory region 0x19000000-0x1dffd000 Physical Memory Region from 1dffd000 size 3000 type 3 Physical Memory Region from 1e000000 size 8e784000 type 1 Adding physical memory region 0x1e000000-0x1f800000 Physical Memory Region from ac784000 size 94000 type 2 Physical Memory Region from ac818000 size fe8000 type 1 Physical Memory Region from b0000000 size 4000000 type 2 Physical Memory Region from fed20000 size 20000 type 2 Physical Memory Region from fed50000 size 40000 type 2 Physical Memory Region from ffa00000 size 40000 type 2 Physical Memory Region from 1000000000 size 350000000 type 1 Physical memory region not addressable Adding physical memory region 0x0-0x1f800000 seL4 failed assertion '!p_region_overlaps(reg)' at /home/critical/Downloads/genode-18.05/contrib/sel4-c59276cc6e3aa138a1e56af8c8a56ce64cf327b8/src/kernel/sel4/src/ arch/x86/kernel/boot.c:123 in function add_allocated_p_region halting... Kernel entry via Interrupt, irq 0 @##################################### Any thoughts? Anything I can try? Any information I can provide to help diagnose? -- Sincerely, Jeremy ______________________________ Software Engineer Critical Technologies Inc.

3 3

We're hiring OS engineers
by Gernot.Heiser＠data61.csiro.au 06 Jul '18

06 Jul '18

Would you like to work on seL4 inside the TS team? Here’s your chance: https://jobs.csiro.au/job/Sydney%2C-NSW-Operating-System-Engineer/488529400/ https://jobs.csiro.au/job/Sydney%2C-NSW-Operating-Systems-Senior-Engineer/4… Gernot

1 0

Re: [seL4] IOMUX on iMX6 conflict with libethdrivers
by Kofidoku.Atuah＠data61.csiro.au 06 Jul '18

06 Jul '18

Hey Fabrizio?, I'm sorry we took so long to get back to you: The underlying problem here is that we haven't yet finished defining and implementing a driver framework for our userspace code, so in order to satisfy dependencies, we began stuffing them into the io_ops struct. So since lots of devices depend on an initialized mux driver, what you see here is the result of that, unfortunately -- the good news is that we're currently defining a driver framework internally (https://docs.sel4.systems/seL4DriverAPI/ChildEnumeration.html is one of the draft pages of documentation -- but none of this is finalized) over the course of this year. What I'd recommend is that you use the helper function, mux_sys_valid() in mux.h (https://github.com/seL4/util_libs/blob/master/libplatsupport/arch_include/a…) inside of the ethernet driver, and map the whole 16K range inside of the IO-Ops initializer -- essentially what's going on there is that there's a dependency on the mux driver that's satisfied by the IO-Ops object. Thanks very much for your patience,? and this sort of thing should be cleaned up soon. Yours truly, -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

2 3

Re: [seL4] seL4 CNode and capability question
by 송대영 05 Jul '18

05 Jul '18

*I have a question about capability. 1. I know that CNode can consist of hierarchy of CNodes like 1-level, 2-level, 3-level.Can I create new CNode object like them? 2. If I can create hierarchy of CNode, I want to create hierarchy of CNode in order to retype new object to new CNode object.I tried it like below source code but it doesn't work with message "Untyped Retype: Invalid destination address".Would you give some advices?--------------------- source code // ** create CNode & mapping seL4_CPtr new_CNode_cap = info->empty.start + 5; error = untyped_retype_root(untyped, seL4_CapTableObject, seL4_SlotBits, cspace_cap, new_CNode_cap); ZF_LOGF_IFERR(error, "Failed to retype our chosen untyped into an CNode object.\n"); printf("================== seL4_DebugCapIdentify ======================\n"); printf("seL4_DebugCapIdentify seL4_CPtr CNode_cap : %u \n", seL4_DebugCapIdentify(new_CNode_cap)); // ** create new Endpoint object and mapping to new CNode seL4_CPtr new_CNode_cap_Endpoint; new_CNode_cap_Endpoint = info->empty.start + 6; error = seL4_Untyped_Retype(untyped /* untyped cap */, seL4_EndpointObject /* type */, seL4_SlotBits /* size */, new_CNode_cap /* root cnode cap */, new_CNode_cap_Endpoint /* destination cspace */, 32 /* depth */, new_CNode_cap_Endpoint /* offset */, 1 /* num objects */); if(error == 0) printf("error : %d \n", error);3. Can I check CNode level? It means like CNode level number.*

1 0

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

IOMUX on iMX6 conflict with libethdrivers
by Fabrizio Bertocci 26 Jun '18

26 Jun '18

Hi, I need your help in trying to understand what is the best way to implement a permanent fix I can push on the seL4 repository regarding the incompatibility issues between the libethdriver and MUX interface of the platsupport. This apply to the iMX6 ethernet driver. I'm not sure about other platforms. In short, the problem is that platsupport takes ownership of the entire MUX (maps the I/O) when the io_ops are initialized: Repo: seL4/seL4_libs File: libsel4platsupport/src/io.c Function: sel4platsupport_new_io_ops ... mux_sys_init(io_ops, get_mux_dependencies(), &io_ops->mux_sys); ... The above call end up calling the platform-specific mux_sys_init that maps only the first 4Kb of IO space from address 0x020e0000 (the base address of the IOMUX controller - note: the IOMUX controller uses 16Kb of address space for its registers, not 4Kb!!!): Repo: seL4/util_libs File: libplatsupport/src/plat/imx6/mux.c Function: mux_sys_init ... MAP_IF_NULL(io_ops, IMX6_IOMUXC, _mux.iomuxc); return imx6_mux_init_common(mux); The pointer "io_ops->mux_sys->priv" should point to the base address of the IOMUX of the SoC (in the virtual memory space of the calling process). The Ethernet driver unfortunately attempts to map the IOMUX again: Repo: seL4/util_libs File: libethdrivers/src/plat/imx6/uboot/mx6qsabrelite.c Function: setup_iomux_enet ... void *base = RESOURCE(&io_ops->io_mapper, IOMUXC); ... // Modify the IOMUX registers, then release the mapped IO: ... UNRESOURCE(&io_ops->io_mapper, IOMUXC, base); but using a larger size (the full 16Kb from the same base address of the IOMUX controller). So, the ethernet controller attempt to map the IO fails because it is already mapped, and nothing works. Right now in my project I've entirely commented out the initialization of the MUXC from the sel4platsupport_new_io_ops function. I understand that if the io_ops attempt to map the MUX (and leave it mapped) there must be a reason, unfortunately I fail to see it. The structure describing the MUXC register (struct imx6_iomuxc_regs, defined in libplatsupport/src/plat/imx6/mux.c) is private and not accessible outside that file, and the only two interface functions available (mux_feature_enable/mux_feature_disable) are not enough to be usable by the ethernet driver. The ethernet driver could also attempt to reuse the same mapped IOMUX (beside that the size of the mapped area is different and won't work anyway), but that will require using the 'priv' field of the io_ops->mux_sys (beside, even trying to map the whole 16Kb of the IOMUX and have the driver to reuse the same mapped address, for some unknown reasons it doesn't work). So, what is the right approach to fix this problem? Why the MUX subsystem maps some IO, never release it and keep it private for most of it? The IOMUX has been introduced somewhere between version 1.0 and 9.x... and it seems a half-baked job... Can we just comment it out if nobody is using it? Or if you have some ideas/suggestions on how to expand it in such a way the ethernet driver could use, please let me know. I'll be happy to implement it. Regards, Fabrizio

2 2

Problems with tk1 nonsecure
by Mike Clark 26 Jun '18

26 Jun '18

I just checked out a fresh copy of https://github.com/ SEL4PROJ/camkes-arm-vm-manifest and built an image for the TK1 using the docker build environment. I copied the resulting image to an SD card and it boots fine. If I switch to the unsecure mode, I get an error on boot. SMMU Address translation error: ID: 98 address: 0xae5be000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 [ 10.204777] mmc1: ADMA error I have not made any changes, so my vm.smmu settings are all default. Any thoughts or help? Mike

3 9

Question about process and thread in tutorials
by 송대영 21 Jun '18

21 Jun '18

* I have question about process and thread in tutorials. 1. sel4 doesn't have process concept.But making new process is exist in tutorial hello-4.What is the exactly difference trhead in hello-2 and process in hello-4?2. In tutorials hello-4, where can I find access path that hello-4 process link hello-4-app?It means I think hello-4 process should designate hello-4-app's path.*

2 1

camkes and compcert
by Michael Neises 21 Jun '18

21 Jun '18

Hello, I understand that the proof for seL4 implies that the compiler and linker do not need to be trusted, because their output can be verified by a tool. Does this output-verification also apply to CAmkES C code for components and interfaces? Specifically, I'm working on a project where we want to have certain functionality implemented in C to be run on the seL4 microkernel. Would we gain any proof by using compcert, or is the output-verification sufficient? And is there any way to execute previously-compiled C binaries in a CAmkES component? I tried system calls, but I learned that won't work with the microkernel :-) I looked into the build architecture of the project, but I couldn't find where CAmkES components were being compiled. I looked into replacing gcc with compcert for the system, but there are used many flags available to gcc that are not available to compcert, so I scratched that idea. Thank you for your help. -Michael

2 1

Regarding porting SEL4 on RISCV hardware
by Sathya Narayanan N 15 Jun '18

15 Jun '18

Hi Members, I am trying to port SEL4 on RISCV hardware. I am stuck in finding the DTB/DTS files path in sel4test folder. Could someone guide me where these files exist and how to change the memory map for UART console. Actually, We changed the code for putchar in systems.c for Linux. So, I am trying to figure out, how to do something similar for SEL4. Please let me know, if someone has ported SEL$ to RISCV hardware. -- regards, Sathya

2 1

feL4: seL4 + Rust
by Jon Lamb 11 Jun '18

11 Jun '18

Hi all! We've been working on a way to write Rust programs for seL4, and would like to share it with you: https://github.com/PolySync/cargo-fel4.git With cargo-fel4, you can write a seL4 task in Rust, expose it through a prescribed entry point, and then build it along with the kernel. For now, it exposes only the system calls by way of Bindgen (a C-to-Rust bindings generator); however, we have plans to build up more idiomatic and Rusty abstractions in the near future. Cheers! Jon, Dan, Zack, and Nathan at PolySync

1 0

seL4_Wait crash if kernel is compiled with -O0 (qemu, pc99, gcc 4.8.2)
by Fabrizio Bertocci 25 May '18

25 May '18

Hi, After hours of debugging I have discovered a quite nasty issue where seL4_Wait() crash if I build the kernel without optimization (gcc option -O0) on a pc99 tested with qemu. How to reproduce: Just create an endpoint (from a vka) and call seL4_Wait(). The simplest reproducer can be obtained from the hello-2 tutorial: - Copy the main.c from the solution directory in the apps/hello-2/src/main.c - Add the following codes right after the creation of vka (TASK 5, approx line 150): { printf("WAITING----------------------------------------------\n"); seL4_Word myBadge; vka_object_t ep_object = {0}; error = vka_alloc_endpoint(&vka, &ep_object); ZF_LOGF_IFERR(error, "Failed to allocate new endpoint object.\n"); seL4_Wait(ep_object.cptr, &myBadge); printf("---------------------------------------------- DONE!!\n"); } Essentially the added code, creates an endpoint using vka and calls seL4_Wait() on it... I expect the code to block forever since there are no other threads that can unblock it... - Build it and run it with: make pc99_hello-2_defconfig make make simulate Expected output: Booting all finished, dropped to user space 4 untypeds of size 12 4 untypeds of size 13 [...] 6 untypeds of size 29 WAITING---------------------------------------------- - Now change the configuration using 'make menuconfig' and select: seL4 Kernel -> Build Options -> Compiler optimisation flag (-O2) and change it to -O0, save the new configuration. - Rebuild and run: make simulate Now you get a kernel exception: [...] 6 untypeds of size 29 WAITING---------------------------------------------- ========== KERNEL EXCEPTION ========== Vector: 0xd ErrCode: 0xa658 IP: 0xe0118ce5 SP: 0xffaf7e28 FLAGS: 0x86 CR0: 0x8001003b CR2: 0x0 (page-fault address) CR3: 0x142000 (page-directory physical address) CR4: 0x100290 Stack Dump: *0xffaf7e28 == 0xe011a658 *0xffaf7e2c == 0x0 *0xffaf7e30 == 0x0 *0xffaf7e34 == 0xe011a658 *0xffaf7e38 == 0x8 *0xffaf7e3c == 0x202 *0xffaf7e40 == 0x0 *0xffaf7e44 == 0x0 *0xffaf7e48 == 0x10 *0xffaf7e4c == 0x7 *0xffaf7e50 == 0x0 *0xffaf7e54 == 0x0 *0xffaf7e58 == 0x0 *0xffaf7e5c == 0x0 *0xffaf7e60 == 0x0 *0xffaf7e64 == 0x0 *0xffaf7e68 == 0x0 *0xffaf7e6c == 0x0 *0xffaf7e70 == 0x0 *0xffaf7e74 == 0x0 Halting... halting... Kernel entry via Interrupt, irq 157 Version info: - gcc: gcc (GCC) 4.8.5 20150623 (Red Hat 4.8.5-11) - qemu: QEMU emulator version 2.0.0, Copyright (c) 2003-2008 Fabrice Bellard - Build environment: CentOS Linux release 7.3.1611 (Core) Other info: - gcc 4.8.5 doesn't seem to support the 'Nehalem' x86 microarchitecture, so I am selecting the 'Generic' microarchitecture (Toolchain Options -> X86 microarchitecture) - Even the tutorial 'hello-timer' fails exactly with the same exception without any modifications if you build the kernel with -O0. - Tested on a Beaglebone black: no problems compiling kernel with -O0 Regards, Fabrizio Bertocci Real-Time Innovations, Inc.

2 1

Tutorials broken?
by Fabrizio Bertocci 22 May '18

22 May '18

Hi all, I was going through the tutorials, unfortunately I've been finding very challenging to follow the instructions as I keep encountering issues after issue. First, the repo command seems to be incorrect. In document: https://docs.sel4.systems/Tutorials/ it says: repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest -m sel4-tutorials.xml but the manifest file 'sel4-tutorials.xml' does not exist on the git repository (of the sel4-tutorial-manifest). What is the correct manifest file to use? There are two manifests (in any branch and tag): master.xml and default.xml. default.xml seems to use the 'new' format of identifying the individual versions of the libraries (through the hash). Let's assume the correct manifest to use is the 'default.xml' from the 'sel4-tutorials' branch and initialize the workspace with: repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest -b sel4-tutorials repo sync So, now: first tutorial, ok (but this tutorial does very little). Second tutorial (hello-2), not so good... to avoid mistake, I am copying directly the solution into the app area: cp projects/sel4-tutorials/solutions/hello-2/src/main.c apps/hello-2/src/main.c make pc99_hello-2_defconfig make ... and the build fails with: [...]/workspaces/sel4-tutorials-2/stage/x86/pc99/lib/libsel4allocman.a(virtual_pool.o): In function `_add_page': [...]/workspaces/sel4-tutorials-2/libs/libsel4allocman/src/mspace/virtual_pool.c:52: undefined reference to `vspace_get_map_obj' The missing function appears to be part of libsel4vspace, that is missing from the library dependency list. Let's add it to add it to the apps/hello-2/Makefile: diff --git a/exercises/hello-2/Makefile b/exercises/hello-2/Makefile index 25c0b35..97a4fc6 100644 --- a/exercises/hello-2/Makefile +++ b/exercises/hello-2/Makefile @@ -28,6 +28,7 @@ ASMFILES += $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/src/plat/${PLA # Libraries required to build the target LIBS = c sel4 sel4muslcsys \ sel4simple sel4vka sel4allocman \ + sel4vspace \ sel4platsupport platsupport \ utils sel4simple-default sel4utils sel4debug Now it builds successfully, unfortunately when running, the child thread doesn't appear to run at all. This is the output of qemu running 'make simulate': Booting all finished, dropped to user space 4 untypeds of size 12 5 untypeds of size 13 5 untypeds of size 14 4 untypeds of size 15 4 untypeds of size 16 4 untypeds of size 17 4 untypeds of size 18 5 untypeds of size 19 5 untypeds of size 20 2 untypeds of size 21 4 untypeds of size 22 4 untypeds of size 23 2 untypeds of size 24 3 untypeds of size 25 3 untypeds of size 26 3 untypeds of size 27 1 untypeds of size 28 6 untypeds of size 29 main: hello world I would have expected seeing on the output the string 'thread_2: hallo wereld' somewhere... Why the thread 2 does not run? This code was working last time I checked (version 5.2). I tried then to continue testing the tutorials, and I went to the hello-3. Hello-3 is based on the Hello-2 but adds an endpoint for IPC between the main thread and the child thread. Surprisingly, this app not only builds out of the box without errors (apparently libsel4vspace was already added to its Makefile), but even running it, works as expected: Booting all finished, dropped to user space 3 untypeds of size 12 5 untypeds of size 13 5 untypeds of size 14 4 untypeds of size 15 4 untypeds of size 16 4 untypeds of size 17 4 untypeds of size 18 5 untypeds of size 19 5 untypeds of size 20 2 untypeds of size 21 4 untypeds of size 22 4 untypeds of size 23 2 untypeds of size 24 3 untypeds of size 25 3 untypeds of size 26 3 untypeds of size 27 1 untypeds of size 28 6 untypeds of size 29 main: hello world thread_2: hallo wereld thread_2: got a message 0x6161 from 0x61 main: got a reply: 0xffff9e9e Right now I suspect that seL4_TCB_Configure() does not work correctly if we don't provide an endpoint (because that's essentially the main difference between the two tests). Can somebody try to run the tutorials and perhaps confirm the problem? Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA

1 0

docker build error
by Paolo Crisafulli 18 May '18

18 May '18

Hi all, I'm using the docker build environment provided by https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles Currently, "make sel4" fails with this message: E: Package 'ncurses-dev' has no installation candidate Anyone experimenting the same behaviour? Cheers, Paolo

2 2

Help with Isabelle/AutoCorres
by Burkhart Wolff 18 May '18

18 May '18

Dear all, I stumbled into some problems with AutoCorres and would be grateful if someone could help me. I used the recent version autocorres1.4 under Isabelle2017. A) Running under MacOS, cpp is apparently not running inside install_C_file (yes, I installed the cpp wrapper: >>>>>>>>>>>>>>>>>>>>>> !/bin/bash # Wrapper for clang C preprocessor on MacOS export L4CPP="-DTARGET=ARM -DTARGET_ARM -DPLATFORM=Sabre -DPLATFORM_Sabre" llvm-gcc -Wno-invalid-pp-token -E -x c $@ <<<<<<<<<<<<<<<<<<<<<< and made sure that it is in the path of the shell in which I started Isabelle.) Does anyone know a cause for this behaviour or a feasible workaround ? (besides doing the expansions by hand) Is there an explicit Isabelle shell variable where the path to cpp must be set ? B) I get a weird crash of AutoCorres without a clue what might cause it: I have a T4.h file with >>>>>>>>>>>>>>>>>>>>>>> #define N_TEETH ( 100 * MODULO ) // shaft encoder's number of teeth per turn #define SIZE_OF_SPEED_FIFO 10 // number of samples to compute average speed extern const char *InputField[]; enum State { S1=1, S2, S3, S4, S5, S6, SFail=0 }; enum Status { FAIL, SUCCESS }; enum InputPatterns { Ph1 = 1, Ph2 = 5, Ph3 = 4, Ph4 = 6, Ph5 = 2, Ph6 = 3 }; struct OBits { int C1 ; int C2 ; int C3 ; } Obits; /********* Output data *****************/ extern enum Status O_Position_Valid; extern unsigned int O_Position_Count; extern unsigned int Relative_Position; extern int Instantaneous_Speed; extern int Mean_Speed; <<<<<<<<<<<<<<<<<<<<<<<<<<<<< and a T4.c file with: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> #include "T4_AlgoODO.h" enum Status O_P_V = SUCCESS; unsigned int O_P_C = 0; unsigned int Relative_Position = 0; int I_Speed = 0; int Mean_Speed = 0; int Acceleration = 0; int scale = 1000; int PI_approx = 3141; struct OBits Input; enum State OState; const unsigned int Radius = 500; const unsigned int Sampling_Rate = 400; unsigned int F_O_P_C = 0; int Speed_FIFO[10 /*SIZE_OF_SPEED_FIFO*/]; int FIFO_pointer = 0; <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<< Loading this in Isabelle/AutoCorres with: >>>>>>>>>>>>>>>>>>>>>>>>> install_C_file "code/c/T4.c” <<<<<<<<<<<<<<<<<<<<<<<<< results in the following AutoCorres crash: … exception Fail raised (line 175 of "~/codebox/odo_new/odo/autocorres-1.4/c-parser/calculate_state.ML"): translate_inttype: incomplete array! Can anybody tell me what this means and propose a workaround ? Best regards B. Wolff

2 1

Untyped Retype destination not empty?
by Richard Clark 18 May '18

18 May '18

Hi! I could use a clue as to the cause of this problem. The program has its free slots start index set correctly. It is trying to allocate a dma buffer. (4k with a known physical address). The vspace has been properly set up and knows the phys addresses of its free memory. This used to work fine in a different process, but I can't find anything I've done different/wrong in this one... I've added some extra printfs, and some debug code (in kernel/src/object/untyped.c). /* Ensure that the destination slots are all empty. */ slots.cnode = CTE_PTR(cap_cnode_cap_get_capCNodePtr(nodeCap)); slots.offset = nodeOffset; slots.length = nodeWindow; for (i = nodeOffset; i < nodeOffset + nodeWindow; i++) { status = ensureEmptySlot(slots.cnode + i); if (status != EXCEPTION_NONE) { userError("Untyped Retype: Slot #%d from %p in destination window non-empty.", (int)i, (void *)slots.cnode); userError("Untyped Retype: At offset #%d length %d.", (int)nodeOffset, (int)nodeWindow); int j = 0; for(j=0;j<2048;j++){ status = ensureEmptySlot(slots.cnode + (i + j)); if (status == EXCEPTION_NONE) { userError("Next Free Slot at #%d from %p.", (int)(i+j), (void *)slots.cnode); status = EXCEPTION_SYSCALL_ERROR; break; } } return status; } } And finally, here is the output from the console: <<seL4(CPU 0) [decodeCNodeInvocation/94 T0xffffff8001a25400 "Lockmaproc" @4196e8]: CNode Copy/Mint/Move/Mutate: Destination not empty.>> <<seL4(CPU 0) [decodeUntypedInvocation/166 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Untyped Retype: Slot #196 from 0xffffff807f000000 in destination window non-empty.>> <<seL4(CPU 0) [decodeUntypedInvocation/167 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Untyped Retype: At offset #196 length 1.>> <<seL4(CPU 0) [decodeUntypedInvocation/172 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Next Free Slot at #197 from 0xffffff807f000000.>> _refill_pool@split.c:187 Failed to retype untyped, error 8 vka_alloc_object_at_maybe_dev@object.h:59 Failed to allocate object of size 4096, error 1 dma_alloc@page_dma.c:92 Failed to allocate untyped of size 12 I need a hint... help? Thanks! Richard ________________________________ 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.

2 1

Automatic testing using qemu
by Paolo Crisafulli 18 May '18

18 May '18

Hi there, I have written a seL4 app using CAmkES, that I am continuously building using Jenkins. I'd like to add a test step to this continuous integration process, launching the app with qemu and parsing the output to validate my expectations. The thing is, although all the active ("control") components reach their last instruction after a while, seL4 does not "exit" (which is expected I guess) and qemu does not stop, keeping my continuous integration job running for ever. Any idea on how to achieve this? Thank you very much in advance. Cheers, Paolo Crisafulli

3 5

Booting seL4, MMU configuration on armv7a-ve
by Jonas Persson 30 Apr '18

30 Apr '18

Hello, I'm new to seL4 and I'm trying to get seL4 running on an Cortex-A7 with VE extensions (NXP IMX6UL). One of the experiments I wish to do is measure how fast I can get from POR to seL4 doing something meningful. To achive optimal boot speed I have a custom bootloader that does the bare minimum. The boot flow looks like this; 1. POR 2. Init HW 3. Load & verify blobs for trust zone and seL4 4. Jump to TEE init (OP-TEE) 5. Tee init code returns to bootloader with the CPU in HYP mode At this point we're back in the bootloader, there is no MMU, D cache or I cache active 6. Configure MMU 7. Jump to seL4 kernel entry I'm currently struggling with getting the MMU properly setup and I was hoping that someone here might shed some light on what I would need to do. I've looked at the elf-loader and from what I can understand it will setup a basic memory-mapping for the kernel only. Some of the questions that stand out in my head are : 1) How should the hand over work between the BL and seL4 with respect to setting up more mappings, for example IO memory. Should the PGD & PMD tables created by the bootloader be shared with the kernel? 2) What needs to be configured before calling the seL4 entry? Thanks, Jonas

1 0

Announcing seL4 9.0.1: with RISC-V support
by Kent.Mcleod＠data61.csiro.au 26 Apr '18

26 Apr '18

We are pleased to announce initial RISC-V support for the UC Berkeley Spike simulator platform. Instructions are available for building and running the seL4 test suite on RISC-V: <https://docs.sel4.systems/Hardware/RISCV> See an online copy of the release notes at: <https://docs.sel4.systems/sel4_release/seL4_9.0.1> <https://docs.sel4.systems/camkes_release/CAmkES_3.4.0> # seL4 Version 9.0.1 Release Announcing the release of `seL4 9.0.1` with the following changes: 9.0.1 2018-04-18: BINARY COMPATIBLE ## Changes * On 64-bit architectures, the `label` field of `seL4_MessageInfo` is now 52 bits wide. User-level programs which use any of the following functions may break, if the program relies on these functions to mask the `label` field to the previous width of 20 bits. - `seL4_MessageInfo_new` - `seL4_MessageInfo_get_label` - `seL4_MessageInfo_set_label` * Initial prototype RISC-V architecture port. This port currently only supports running in 64-bit mode without FPU or or multicore support on the Spike simulation platform. There is *no verification* for this platform. ## Upgrade Notes --- # Full changelog Refer to the git log in <https://github.com/seL4/seL4> using `git log 9.0.0..9.0.1` # More details See the [9.0.1 manual](http://sel4.systems/Info/Docs/seL4-manual-9.0.1.pdf) included in the release or ask on the mailing list!# CAmkES Version camkes-3.3.0 Release ---- # CAmkES Version camkes-3.4.0 Release Announcing the release of `` with the following changes: camkes-3.4.0 2018-04-18 Using seL4 version 9.0.1 ## Changes ## Upgrade Notes --- # Full changelog Use `git log camkes-3.3.0..camkes-3.4.0` in <https://github.com/seL4/camkes-tool> # More details See the [documentation](https://github.com/seL4/camkes-tool/blob/camkes-3.4.0/docs/i… or ask on the mailing list!

7 10

Further use of Device Tree?
by Jeff Waugh 23 Apr '18

23 Apr '18

Hello, Congrats on the RISC-V release! I noticed some Device Tree code snuck in, replacing some hard coded bits in the platform, and is intended to be exposed to the rootserver… Any interest or intention to bring that to the ARM code, and possibly avoid building kernels for specific platforms? Thanks, Jeff

2 1

UART1 getchar
by Wei Xiang Leow 19 Apr '18

19 Apr '18

Hello all, I'm new to seL4 and embedded systems, please bear with me. I'm trying to use Sabrelite's UART1 (PS_SERIAL0), while I can make it write data (putchar), I can't make it read (getchar). The code is as follows on sel4 7.0.0, using platsupport/sel4platsupport: ps_io_ops_t io_ops; error = sel4platsupport_new_io_ops(vspace, vka, &io_ops); printf("Initialising io_ops: %d\n",error); ps_chardevice_t serial0; ps_cdev_init(PS_SERIAL0,&io_ops,&serial0) ps_chardevice_t serial1; ps_cdev_init(PS_SERIAL1,&io_ops,&serial1); //CONSOLE int character; while (1) { character = ps_cdev_getchar(&serial0); //printf("%d\n",character); if (character != -1) { ps_cdev_putchar(&serial1,character); printf("%d\n",character); } } This runs fine on QEMU with -serial file/ttyUSB -serial mon:stdio. Next I tried to run this on the Sabrelite board: -Clone the 08-09 uboot from git, according to https://sel4.systems/Info/ Hardware/sabreLite/ -Apply patches 1 and 2 (applying 3 and 4 caused uboot to stall) -Put uboot into SPI flash -Restart, run the sel4 image on the SD card, with UART2 connected to PC's RS232 and displayed by minicom, and UART1 connected to /dev/ttyUSB0 -Have a python script writing 'A's to /dev/ttyUSB0 sel4 loads but fails to read anything from /dev/ttyUSB0, UART1 just receives EOFs (-1s). The rxd seems to always be 0. Swapping the UARTs works, at the cost of losing the console: while (1) { character = ps_cdev_getchar(&serial1); //printf("%d\n",character); if (character != -1) { ps_cdev_putchar(&serial0,character); printf("%d\n",character); } } So UART2 (default console) can read and write, while UART1 can write but not read. Has anyone encountered the same problem? Suggestions much appreciated. Regards, Leow Wei Xiang

1 0

Camkes manifest now requires cmake 3.7.2 or higher to be built
by Amit Goyal 13 Apr '18

13 Apr '18

I was running the following commands to build camkes: 1. repo init -u https://github.ls com/sel4/camkes-manifest.git 2. repo sync 3. make clean 4. make ia32_simple_defconfig; make silentoldconfig 5. make -j4 6. qemu-system-i386 -nographic -m 512 -cpu Haswell -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99 Earlier it used to work perfectly fine but now it requires cmake 3.7.2 or higher which can be obviously be done by using pip install. I just wanted to convey this so that the same may be updated on prerequisites page. (https://github.com/SEL4PROJ/sel4-tutorials/blob/master/Prerequisites.md) -- Thanks and Regards, Amit Goyal

1 0

Unable to Run seL4test
by Amit Goyal 13 Apr '18

13 Apr '18

Hi Kofi, I am getting the attached error (Error Log.txt) while running seL4test. Earlier it used to run perfectly fine. I am running the following commands: $ repo init -u https://github.com/seL4/sel4test-manifest.git $ repo sync $ make clean $ make ia32_simulation_release_xml_defconfig $ make -j libmuslc && make $ make simulate-ia32 Can you please look into this. -- Thanks and Regards, Amit Goyal

2 2

New documentation website: https://docs.sel4.systems
by Kent.Mcleod＠data61.csiro.au 12 Apr '18

12 Apr '18

We are pleased to annouce a new documentation website at <https://docs.sel4.systems>! The documentation site is now using GitHub pages, generated from a GitHub repository <https://github.com/SEL4PROJ/docs> using a popular static site generator, Jekyll. GitHub pages hosted documentation is a standard documentation pattern familiar to many in the open-source community. Content from the previous wiki has been migrated to the new site, while the wiki itself is no longer available. The new documentation format should welcome community contributions, and be easier to maintain for the following reasons: * Contributions are welcome via pull request. * Easier editing through Markdown (GFM), an open document format. * Content styling is now separate from presentation. * The site can be checked out and hosted locally. * Contributions are versioned and reviewed, and tagged at released versions of seL4. We hope that this will lead to the quality of our documentation increasing as it is easier and more accessible to update. Contributions, via pull requests or feature requests on github, are welcome. Kent

1 0

seL4 9.0.0 and CAmkES camkes-3.3.0 release
by Kent.Mcleod＠data61.csiro.au 12 Apr '18

12 Apr '18

See an online copy of the release notes at: <https://docs.sel4.systems/sel4_release/seL4_9.0.0> <https://docs.sel4.systems/camkes_release/CAmkES_3.3.0> # seL4 Version 9.0.0 Release Announcing the release of `seL4 9.0.0` with the following changes: 9.0.0 2018-04-11: BREAKING # Changes * Debugging option on x86 for syscall interface to read/write MSRs (this is an, equally dangerous, alternative to dangerous code injection) * Mitigation for Meltdown (https://meltdownattack.com) on x86-64 implemented. Mitigation is via a form of kernel page table isolation through the use of a Static Kernel Image with Microstate (SKIM) window that is used for trapping to and from the kernel address space. This can be enabled/disabled through the build configuration depending on whether you are running on vulnerable hardware or not. * Mitigation for Spectre (https://spectreattack.com) on x86 against the kernel implemented. Default is software mitigation and is the best performing so users need to do nothing. This does *not* prevent user processes from exploiting each other. * x86 configuration option for performing branch prediction barrier on context switch to prevent Spectre style attacks between user processes using the indirect branch predictor * x86 configuration option for flushing the RSB on context switch to prevent Spectre style attacks between user processes using the RSB * Define extended bootinfo header for the x86 TSC frequency * x86 TSC frequency exported in extended bootinfo header * `archInfo` is no longer a member of the bootinfo struct. Its only use was for TSC frequency on x86, which can now be retrieved through the extended bootinfo * Invocations to set thread priority and maximum control priority (MCP) have changed. - For both invocations, users must now provide a TCB capability `auth` - The requested MCP/priority is checked against the MCP of the `auth` capability. - Previous behavior checked against the invoked TCB, which could be subject to the confused deputy problem. * `seL4_TCB_Configure` no longer takes prio, mcp as an argument. Instead these fields must be set separately with `seL4_TCB_SetPriority` and `seL4_TCB_SetMCPriority`. * `seL4_TCB_SetPriority` and `seL4_TCB_SetMCPriority` now take `seL4_Word` instead of `seL4_Uint8`. - `seL4_MaxPrio` remains at 255. * `seL4_TCB_SetSchedParams` is a new method where MCP and priority can be set in the same sytsem call. * Size of the TCB object is increased for some build configurations # Upgrade notes * `seL4_TCB_Configure` calls that set priority should be changed to explicitly call `seL4_TCB_SetSchedParams` or `SetPriority` * `seL4_TCB_Configure` calls that set MCP should be changed to explicitly call `seL4_TCB_SetSchedParams` or `seL4_TCB_SetMCPriority` --- # Full changelog Refer to the git log in <https://github.com/seL4/seL4> using `git log 8.0.0..9.0.0` # More details See the [9.0.0 manual](http://sel4.systems/Info/Docs/seL4-manual-9.0.0.pdf) included in the release or ask on the mailing list! ---- # CAmkES Version camkes-3.3.0 Release Announcing the release of `camkes-3.3.0` with the following changes: camkes-3.3.0 2018-04-11 Using seL4 version 9.0.0 ## Changes * Hardware dataport with large frame sizes issue has been fixed * Bug fix: Enumerating connections for hierarchical components with custom connection types is now done correctly * Bug fix: Data structure caching is now correctly invalidated between builds * Initial CMake implementation for CAmkES. See the CAmkES test apps for examples. ## Upgrade notes * No special upgrade requirements. ## Known issues * Hierarchical components that export dataport connectors create compilation errors as the templates cannot accurately tell that the connector of the parent component is exported from the child and no code should be generated. A temporary workaround involves making the dataport connection explicitly available to the parent component. --- # Full changelog Use `git log camkes-3.2.0..camkes-3.3.0` in <https://github.com/seL4/camkes-tool> # More details See the [documentation](https://github.com/seL4/camkes-tool/blob/camkes-3.3.0/docs/i… or ask on the mailing list!

1 0

camkes tutorial build compilation error
by Thad Seeberger 03 Apr '18

03 Apr '18

Good day, I am working thru the examples. make arm_hello-camkes-0_defconfig; make -- compiles and run on qemu The I tried x86 architecture make ia32_hello-camkes-0_defconfig; make -- build error I cant find declarations for any of the listed errors. I'm guessing these should be dynamically defined before the build based on the architecture. Please let me know what I'm doing wrong. thx [CC] kernel_final.s /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/32/kernel/vspace_32paging.c: In function ‘decodeIA32PageDirectoryInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/32/kernel/vspace_32paging.c:263:10: error: ‘X86PageDirectoryGetStatusBits’ undeclared (first use in this function); did you mean ‘performIA32PageDirectoryGetStatusBits’? case X86PageDirectoryGetStatusBits: { ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~ performIA32PageDirectoryGetStatusBits /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/32/kernel/vspace_32paging.c:263:10: note: each undeclared identifier is reported only once for each function it appears in /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c: In function ‘decodeX86FrameInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:854:10: error: ‘X86PageMap’ undeclared (first use in this function); did you mean ‘ARMPageMap’? case X86PageMap: { /* Map */ ^~~~~~~~~~ ARMPageMap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1012:10: error: ‘X86PageRemap’ undeclared (first use in this function); did you mean ‘X86PageMap’? case X86PageRemap: { /* Remap */ ^~~~~~~~~~~~ X86PageMap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1143:10: error: ‘X86PageUnmap’ undeclared (first use in this function); did you mean ‘X86PageRemap’? case X86PageUnmap: { /* Unmap */ ^~~~~~~~~~~~ X86PageRemap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1166:10: error: ‘X86PageMapIO’ undeclared (first use in this function); did you mean ‘X86PageMap’? case X86PageMapIO: { /* MapIO */ ^~~~~~~~~~~~ X86PageMap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1175:10: error: ‘X86PageGetAddress’ undeclared (first use in this function); did you mean ‘ARMPageGetAddress’? case X86PageGetAddress: { ^~~~~~~~~~~~~~~~~ ARMPageGetAddress /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c: In function ‘decodeX86PageTableInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1236:21: error: ‘X86PageTableUnmap’ undeclared (first use in this function); did you mean ‘ARMPageTableUnmap’? if (invLabel == X86PageTableUnmap) { ^~~~~~~~~~~~~~~~~ ARMPageTableUnmap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1246:21: error: ‘X86PageTableMap’ undeclared (first use in this function); did you mean ‘X86PageTableUnmap’? if (invLabel != X86PageTableMap ) { ^~~~~~~~~~~~~~~ X86PageTableUnmap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c: In function ‘decodeX86MMUInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1365:25: error: ‘X86ASIDControlMakePool’ undeclared (first use in this function); did you mean ‘ARMASIDControlMakePool’? if (invLabel != X86ASIDControlMakePool) { ^~~~~~~~~~~~~~~~~~~~~~ ARMASIDControlMakePool /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1434:25: error: ‘X86ASIDPoolAssign’ undeclared (first use in this function); did you mean ‘ARMASIDPoolAssign’? if (invLabel != X86ASIDPoolAssign) { ^~~~~~~~~~~~~~~~~ ARMASIDPoolAssign /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/interrupt.c: In function ‘Arch_decodeIRQControlInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/interrupt.c:122:10: error: ‘X86IRQIssueIRQHandlerIOAPIC’ undeclared (first use in this function); did you mean ‘invokeIssueIRQHandlerIOAPIC’? case X86IRQIssueIRQHandlerIOAPIC: { ^~~~~~~~~~~~~~~~~~~~~~~~~~~ invokeIssueIRQHandlerIOAPIC /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/interrupt.c:144:10: error: ‘X86IRQIssueIRQHandlerMSI’ undeclared (first use in this function); did you mean ‘X86IRQIssueIRQHandlerIOAPIC’? case X86IRQIssueIRQHandlerMSI: { ^~~~~~~~~~~~~~~~~~~~~~~~ X86IRQIssueIRQHandlerIOAPIC /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c: In function ‘decodeX86PortInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:62:21: error: ‘X86IOPortOut8’ undeclared (first use in this function) if (invLabel == X86IOPortOut8 || invLabel == X86IOPortOut16 || invLabel == X86IOPortOut32) { ^~~~~~~~~~~~~ /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:62:50: error: ‘X86IOPortOut16’ undeclared (first use in this function); did you mean ‘X86IOPortOut8’? if (invLabel == X86IOPortOut8 || invLabel == X86IOPortOut16 || invLabel == X86IOPortOut32) { ^~~~~~~~~~~~~~ X86IOPortOut8 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:62:80: error: ‘X86IOPortOut32’ undeclared (first use in this function); did you mean ‘X86IOPortOut16’? if (invLabel == X86IOPortOut8 || invLabel == X86IOPortOut16 || invLabel == X86IOPortOut32) { ^~~~~~~~~~~~~~ X86IOPortOut16 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:75:10: error: ‘X86IOPortIn8’ undeclared (first use in this function); did you mean ‘X86IOPortOut8’? case X86IOPortIn8: { /* inport 8 bits */ ^~~~~~~~~~~~ X86IOPortOut8 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:89:10: error: ‘X86IOPortIn16’ undeclared (first use in this function); did you mean ‘X86IOPortIn8’? case X86IOPortIn16: { /* inport 16 bits */ ^~~~~~~~~~~~~ X86IOPortIn8 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:103:10: error: ‘X86IOPortIn32’ undeclared (first use in this function); did you mean ‘X86IOPortIn16’? case X86IOPortIn32: { /* inport 32 bits */ ^~~~~~~~~~~~~ X86IOPortIn16 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/iospace.c: In function ‘decodeX86IOPTInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/iospace.c:195:21: error: ‘X86IOPageTableUnmap’ undeclared (first use in this function); did you mean ‘ARMPageTableUnmap’? if (invLabel == X86IOPageTableUnmap) { ^~~~~~~~~~~~~~~~~~~ ARMPageTableUnmap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/iospace.c:201:21: error: ‘X86IOPageTableMap’ undeclared (first use in this function); did you mean ‘X86IOPageTableUnmap’? if (invLabel != X86IOPageTableMap ) { ^~~~~~~~~~~~~~~~~ X86IOPageTableUnmap make[1]: *** [kernel_final.s] Error 1 make: *** [kernel_elf] Error 2

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 28 Mar '18

28 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

3 open positions for Proof Engineers at Data61
by Gerwin.Klein＠data61.csiro.au 20 Mar '18

20 Mar '18

Data61 Seeking Proof Engineers ============================== We are are hiring again! If only there were a place where I could prove theorems for money, change the world, and have fun while doing it... Sounds too good to exist? In the Trustworthy Systems team at Data61 that's what we do for a living. We are the creators of seL4, the world's first fully formally verified operating system kernel with extreme performance and strong security & correctness proofs. Our highly international team is located on the UNSW campus, close to the beautiful beaches of sunny Sydney, Australia, one of the world's most liveable cities. We are looking for 3 motivated proof engineers who want to join our team in Sydney, move things forward, and have global impact. We are expanding our team, because seL4 is going places. There are active projects around the world in - Automotive - because cars have been hacked enough - Aviation - for more security and safety for autonomous vehicles - Defence - protecting confidential information - Connected consumer devices - with security built in from the start - Spaceflight - because awesome To make these projects successful, we need to scale formal verification. You would - work on industrial-scale formal proofs in Isabelle/HOL - develop formally verified infrastructure for building secure systems on top of seL4 - contribute to improved proof automation and better reasoning techniques - apply formal proof to real-world systems and tools To apply for this position, you should possess a significant subset of the following skills. - functional programming in a language like Haskell, ML, or OCaml - first-order or higher-order formal logic - basic experience in C - ability and desire to quickly learn new techniques - undergraduate degree in Computer Science, Mathematics, or similar - ability and desire to work in a larger team We are hiring at two levels, so if you are more qualified or experienced than the above would suggest, you can come in as a senior proof engineer. If you additionally have experience - in software verification with an interactive theorem prover such as Isabelle/HOL, HOL4, or Coq, and/or - with operating systems and microkernels you should definitely apply! If you have the right skills and background, we can provide training on the job. Continual learning is a central component of everything we do. You will work with a unique world-leading combination of OS and formal methods experts, students at undergraduate and PhD level, engineers, and researchers from 5 continents, speaking over 15 languages. Trustworthy Systems is a fun, creative, and welcoming workplace with flexible hours & work arrangements. We value diversity in all forms and welcome applications from people of all ages, including people with disabilities, and those who identify as LGBTIQ. See https://ts.data61.csiro.au/diversity/ for more information. Salary ranges for this position, in AUD (plus superannuation): - Junior: 80-91K - Senior: 95-103K depending on experience and qualifications. Apply online at the following links: - https://jobs.csiro.au/job/Sydney%2C-NSW-Proof-Engineer/464792900/ - https://jobs.csiro.au/job/Sydney%2C-NSW-Senior-Proof-Engineer/464792300/ Your application should include a cover letter, CV, undergraduate transcript (if applicable), and contact information for two references. This round of applications closes 15 April 2018. The seL4 code and proof are open source. Check them out at https://seL4.systems More information about Data61's Trustworthy Systems team at https://ts.data61.csiro.au Still studying? We also have internship opportunities! https://ts.data61.csiro.au/students/

1 0

Unable to Compile Tutorial 2 Exercises
by Amit Goyal 20 Mar '18

20 Mar '18

Hi, I am new to sel4 and was thus practising the tutorials given at: https://wiki.sel4.systems/Tutorials While compiling tutorial 2 exercises, I got the attached error (I have also attached the main.c file). Can someone please help me in resolving it. -- Thanks and Regards, Amit Goyal

2 1

Ethernet driver for TK-1
by Michal Podhradsky 20 Mar '18

20 Mar '18

Hello, I would like to use a similar Ethernet driver component as for x86 platforms here: https://github.com/seL4/camkes-vm/tree/master/components/Ethdriver But in the camkes-vm-arm repository I don't see an equivalent component: https://github.com/SEL4PROJ/camkes-arm-vm/tree/master/apps/vm/components Is the ethernet currently just passed to Linux? And if so, what would entail making a new driver etc similar to x86 platforms? Regards Michal

2 1

VM and VMM Communication for ARM
by Daniel Wang 17 Mar '18

17 Mar '18

Hi all, I have a couple questions about VM an VMM communication for CAMKES-ARM-VM. Please correct me if I’m wrong. I found when VMM load Linux device it installs a vgic (install_linux_devices() -> vm_install_vgic()) But how exactly a interrupt caused by VM is distributed from GIC to VGIC (kernel to VMM)? I saw that we can register a virq to the VGIC (vm_virq_new()), but I’m not sure when a interrupt is generated how it is passed to the VGIC. Second, I found that we can install virtual devices to VM (e.g. for Vchan communication). Seems like when Linux tries to access the mapped virtual device, a page_fault will generated. Does it create a interrupt? How does it processed by VMM code exactly? I found post_main() in the generated camkes.c file has 3 threads, case 3 runs the control thread -> run(), case 5 runs vevent interface vevent__run(), and case 7 runs fault hander. Does it triggers vevent? I’m not sure the control flow. Thank you in advance! Best Regards -Daniel Wang

1 0

irq_server example? Interrupt handlers?
by Richard Clark 14 Mar '18

14 Mar '18

Hi all! I have an Ethernet driver underneath an lwip implementation that I've gotten to run threaded tcpip. It happily passes messages back and forth and all around between half a dozen threads over a dozen ports all on localhost. Every once in a while though, it wants to send a packet to the outside world... this of course invokes the Ethernet driver, which rather annoyingly, is polled. I am looking for the proper way to convert my polled Ethernet driver to be interrupt-driven.... however the sel4 interrupt-handling/dispatching seems to escape my grasp and I could use a little help... It would appear that there is a mechanism to register a request to receive a message whenever an interrupt occurs? irq_server.c? Are there some nice simple examples out there? Is there an easier way perhaps? Thanks! Richard H. Clark ________________________________ 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.

2 1

Questions about Vchan
by Daniel Wang 14 Mar '18

14 Mar '18

Hi all, I’m trying to figure out how to use the Vchan library to setup communication between guest OS and native components. I got couple questions how you can give me some advices. 1. I saw the camkes_vchan_con_t structure in the helloworld components (camkes-arm-vm), but I could not find the implementation for vchan_con_new_connection(), vchan_con_rem_connection(), etc. Are those autogenerated by camkes? If so how it is generated? static camkes_vchan_con_t con = { .connect = &vchan_con_new_connection, .disconnect = &vchan_con_rem_connection, .get_buf = &vchan_con_get_buf, .status = &vchan_con_status, .alert = &vchan_con_ping, .wait = &vevent_wait, .poll = &vevent_poll, .dest_dom_number = 0, .source_dom_number = 50, }; 2. I tried to compile the Vchan support and demo helloworld components for odroid-xu. But the compile shows error due to the VM.h file (camkes-arm-vm/projects/vm/components/VM/src/cmks_vchan_vm.c:23) cannot be found. How can I generate the VM.h file? Thanks a lot! Best Regards -Daniel Wang

4 5

seL4 developer review of RISC-V privileged ISA spec?
by Kelly Dean 14 Mar '18

14 Mar '18

The RISC-V privileged ISA is not yet finalized. Have the seL4 developers reviewed the draft [1], in case they might have any recommendations for improvement? For example, just last year a blunder (H-mode) was removed from the draft per a proposal [2] on the mailing list. Finalization is planned for this year. Speak now or forever hold your peace. The first public draft of the memory consistency model [3] was also released just last December. And platform standardization, especially the IOMMU, is in progress. [1] https://content.riscv.org/wp-content/uploads/2017/05/riscv-privileged-v1.10… [2] https://groups.google.com/a/groups.riscv.org/forum/#!msg/isa-dev/SfEDPLU0NU… [3] https://groups.google.com/a/groups.riscv.org/forum/#!topic/isa-dev/hKywNHBk…

6 5

Questions about Allocman
by Daniel Wang 12 Mar '18

12 Mar '18

Hi all, I’m trying to understand the code a little bit more. This is kind of a random question. I’m wondering that in a case where we call to allocate a frame using allocman library, where is the physical address of a certain region is stored? In allocman_t there are multiple fields: size_t num_utspace_chunks; struct allocman_utspace_chunk *utspace_chunk; size_t *utspace_chunk_count; struct allocman_utspace_allocation **utspace_chunks; struct allocman_utspace_chunk { size_t size_bits; seL4_Word type; size_t count; }; struct allocman_utspace_allocation { seL4_Word cookie; cspacepath_t slot; }; I didn’t find struct that hold the paddr, also after we create a frame where is that paddr stored? It is stored in slot.capPtr? Also What does the field cookie for? Best Regards -Daniel Wang

3 3

Share UART with Guest Linux
by Daniel Wang 10 Mar '18

10 Mar '18

Hi all, For experiment, I created a simple app along with the vmm using CamKES-ARM-VM repository. Currently the simple app only prints strings periodically using printf(). However as soon as the guest Linux starting running. I cannot print anything and also receives error as following: I assumes it is due to the iommu capability got assigned to Linux by VMM. Is there a way to allow native app also prints information on the screen using printf()? ------------------ libsel4muslcsys: Error attempting syscall 162 FAULT HANDLER: data fault from hello.control (ID 0x1) on address 0xffffff80, pc = 0x135ac, fsr = 0x3840046 FAULT HANDLER: pc = 0x135ac FAULT HANDLER: sp = 0x142d20 FAULT HANDLER: lr = 0x135ac FAULT HANDLER: r0 = 0xffffff80 FAULT HANDLER: r1 = 0 FAULT HANDLER: r2 = 0 FAULT HANDLER: r3 = 0 FAULT HANDLER: r4 = 0x26 FAULT HANDLER: r5 = 0 FAULT HANDLER: r6 = 0 FAULT HANDLER: r7 = 0xfffffff2 FAULT HANDLER: r8 = 0x1 FAULT HANDLER: r9 = 0 FAULT HANDLER: r10 = 0 FAULT HANDLER: r12 = 0x142caa FAULT HANDLER: r14 = 0x135ac FAULT HANDLER: cpsr = 0x20000050 FAULT HANDLER: memory map: FAULT HANDLER: +-- 0x00143fff -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x00143000 -- FAULT HANDLER: | stack FAULT HANDLER: +-- 0x0013f000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0013e000 -- FAULT HANDLER: | <undescribed> FAULT HANDLER: +-- 0x00137fff -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x00137000 -- FAULT HANDLER: | IPC buffer FAULT HANDLER: +-- 0x00136000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x00135000 -- FAULT HANDLER: | <undescribed> FAULT HANDLER: +-- 0x00131fff -- FAULT HANDLER: | code and data FAULT HANDLER: +-- 0x00010000 -- CPIO: 2 files found. 0) linux 0x00059c70, 16302080 bytes 1) linux-dtb 0x00fe5ce8, 29415 bytes Best Regards -Daniel Wang

1 1

Compilation Error with version
by Thad Seeberger 08 Mar '18

08 Mar '18

Good day. I am getting hung up compiling the CAmkES compiles. I'm getting following error which I believe is because the version.h.d does not exist. Where is the version set? thx [camkes-accelerator] building... -- Configuring done -- Generating done -- Build files have been written to: /home/xxxx/seL4_camkes_x86_64/stage/x86/pc99/accelerator ninja: error: '/home/xxxx/seL4_camkes_x86_64/tools/camkes/tools/accelerator/DEPFILE', needed by '.', missing and no known rule to make it make: *** [/home/xxxx/seL4_camkes_x86_64/stage/x86/pc99/accelerator/camkes-accelerator] Error 1 ive traced it down I think to this block in the Cmakeadd_custom_command( OUTPUT ${CMAKE_CURRENT_BINARY_DIR} OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/include/version.h OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/version.h.d # Build a valid dependency file from the print-deps script, this is a little awkward COMMAND echo "include/version.h: " > "${CMAKE_CURRENT_BINARY_DIR}/version.h.d" COMMAND "${CMAKE_CURRENT_SOURCE_DIR}/print-deps.py" >> "${CMAKE_CURRENT_BINARY_DIR}/version.h.d" COMMAND sed -i "s/$$/\\/" "${CMAKE_CURRENT_BINARY_DIR}/version.h.d" COMMAND COMMAND "${CMAKE_CURRENT_SOURCE_DIR}/mkversion.py" >"${CMAKE_CURRENT_BINARY_DIR}/include/version.h" DEPENDS mkversion.py DEPENDS print-deps.py DEPFILE ${CMAKE_CURRENT_BINARY_DIR}/version.h.d )

4 8

CapDL spec for Camkes-ARM-VM
by Daniel Wang 08 Mar '18

08 Mar '18

Hi all, I’m trying build a PoC system based on the camkes-arm-vm repository. I saw the init process is created using CapDL, but I’m having trouble to find the the CapDL spec file. Could you please point it out for me? Also for the first step, I’m trying to build another app side-by-side with the VMM and guest Linux. I assume I need to modify the CapDL. I’m not exactly the work flow with CapDL can you give me a hint? Thanks. Best Regards -Daniel Wang

2 2

ARM-VM with Linux Distribution
by Daniel Wang 06 Mar '18

06 Mar '18

Hi all, I was able to compile the camkes-arm-vm and run it on a TK1-SOM board. I wonder if it is possible to run a Linux distribution as the guest OS, such as Ubuntu, Fedora, etc.? If so how can we do that? Best Regards -Daniel Wang

2 1

Re: [seL4] seL4 VMM Hangs during loading time
by Daniel Wang 02 Mar '18

02 Mar '18

Hi Kent and Peter, Thank you so much for your response. I do not know what exactly caused the issue. But I upgraded my toolchain and recompiled the image again and it loaded this time. The GCC version is version 7.2.1 (before it was 4.6). Although I still see the misaligned information like this: CACHE: Misaligned operation at range [90000000, 90000014] CACHE: Misaligned operation at range [90001000, 900091c4] CACHE: Misaligned operation at range [900091c4, 900098d8] CACHE: Misaligned operation at range [900198d8, 900198e0] CACHE: Misaligned operation at range [900198e0, 91392ae0] CACHE: Misaligned operation at range [91394000, 913a4820] CACHE: Misaligned operation at range [913a4820, 913a8000] Another thing I found is that U-boot for TK1-SOM cannot detect ethernet, but I was able to copy the image into MMC and load from there. There are two things I want to do with the seL4 ARM VMM platform. First, I want to incorporate the secure boot from U-boot to seL4 and then using seL4 to verified signed Linux. Second, I want to build a PoC native application and allow the communication between the native app to communication with App running in Linux. I’m wondering if anyone did those two things before that can give me some advice? I implemented the the second scenario before using L4re with a paravirtualized L4Linux. But I’m exactly sure how to do it with seL4 yet. Best Regards -Daniel Wang > On Mar 1, 2018, at 8:00 PM, <Kent.Mcleod(a)data61.csiro.au> <Kent.Mcleod(a)data61.csiro.au> wrote: > > Hi Daniel, > > Two things to try: > > First is to confirm that CONFIG_PRINTING is enabled to distinguish if the kernel is successfully starting its init process. > > Second is to check what ${loadaddr} is set to. Yours seems correct, ours seems to be 0x81000000, but that is for the tk1 jetson dev board. > > You could also try editing the elfloader to print out the contents of the kernel entrypoint before it jumps there to confirm that it is the correct instructions in the stage/arm/tk1/kernel.elf binary. > > Below is what I see when I boot the project on our devboard. > > Kind regards, > Kent. > > ---- > U-Boot SPL 2015.10-rc5-00002-gf861f51-dirty (Oct 13 2015 - 13:44:41) > > > U-Boot 2015.10-rc5-00002-gf861f51-dirty (Oct 13 2015 - 13:44:41 +1100) > > TEGRA124 > Model: NVIDIA Jetson TK1 > Board: NVIDIA Jetson TK1 > DRAM: 2 GiB > MMC: Tegra SD/MMC: 0, Tegra SD/MMC: 1 > tegra-pcie: PCI regions: > tegra-pcie: I/O: 0x12000000-0x12010000 > tegra-pcie: non-prefetchable memory: 0x13000000-0x20000000 > tegra-pcie: prefetchable memory: 0x20000000-0x40000000 > tegra-pcie: 2x1, 1x1 configur��K��Ʌ�pcie: probing port 0, using 2 lanes > tegra-pcie: link 0 down, retrying > tegra-pcie: link 0 down, retrying > tegra-pcie: link 0 down, retrying > tegra-pcie: link 0 down, ignoring > tegra-pcie: probing port 1, using 1 lanes > In: serial > Out: serial > Err: serial > Net: RTL8169#0 > Hit any key to stop autoboot: 2 > 0 > Tegra124 (Jetson TK1) # setenv autoload no && dhcp && tftpboot 0x81000000 jetson1/sel4-image > setenv autoload no && dhcp && tftpboot 0x81000000 jetson1/sel4-image > BOOTP broadcast 1 > BOOTP broadcast 2 > BOOTP broadcast 3 > BOOTP broadcast 4 > DHCP client bound to address 10.13.1.172 (2929 ms) > Using RTL8169#0 device > TFTP from server 10.13.0.130; our IP address is 10.13.1.172 > Filename 'jetson1/sel4-image'. > Load address: 0x81000000 > Loading: ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################ > 3.8 MiB/s > done > Bytes transferred = 20493516 (138b4cc hex) > Tegra124 (Jetson TK1) # bootelf 0x81000000 > bootelf 0x81000000 > ## Starting application at 0x90000000 ... > ELF loader: monitor mode init done > Copy monitor mode vector from 90001000 to a7f00000 size 50 > Number of IRQs: 192 > Load seL4 in nonsecure HYP mode 600001da > ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3 > paddr=[90000000..9139ffff] > ELF-loading image 'kernel' > paddr=[80000000..8003cfff] > vaddr=[e0000000..e003cfff] > virt_entry=e0000000 > ELF-loading image 'capdl-loader-experimental' > paddr=[8003d000..8158dfff] > vaddr=[10000..1560fff] > virt_entry=18484 > Enabling hypervisor MMU and paging > Jumping to kernel-image entry point... > > Bootstrapping kernel > Total 28 IOASID set up > Region [c to 28) for SMMU caps > Booting all finished, dropped to user space > > > > From: Devel <devel-bounces(a)sel4.systems> on behalf of Daniel Wang <danielwang.ksu(a)gmail.com> > Sent: Friday, March 2, 2018 7:47 AM > To: devel(a)sel4.systems > Subject: [seL4] seL4 VMM Hangs during loading time > > Hi all, > > I’m trying to run seL as a microvisor following the CAMKES-ARM-VM. My development board is TK1-SOM from ColoradoEngineering. I was able to flash the U-boot to to load seL4 HYP mode. However when I try to load the kernel. The system just hangs. I got stuck here any help would be appreciated thank you! > > I built the capdl-loader-experimental-image-arm-tk1 > and can copied it to the TK1 MMC storage, then I followed the wiki to setup env bootm_boot_mode to nonsec. Attachment is the printout: > > ------------------------------------------------------------------------------------------- > U-Boot 2018.03-rc3-00090-g3990c9d (Mar 01 2018 - 14:33:40 -0500) > > TEGRA124 > Model: Colorado Engineering TK1-SOM > Board: CEI tk1-som > DRAM: 2 GiB > MMC: sdhci@700b0400: 1, sdhci@700b0600: 0 > Loading Environment from MMC... OK > In: > serial > Out: serial > Err: serial > Net: No ethernet found. > Hit any key to stop autoboot: 0 > Tegra124 (TK1-SOM) # setenv bootm_boot_mode nonsec > Tegra124 (TK1-SOM) # saveenv > Saving Environment to MMC... Writing to MMC(0)... OK > Tegra124 (TK1-SOM) # ext2ls mmc 0 > <DIR> > 4096 . > <DIR> > 4096 .. > <DIR> > 16384 lost+found > <DIR> > 4096 boot > <DIR> > 4096 bin > <DIR> > 4096 dev > <DIR> > 12288 etc > <DIR> > 4096 home > <DIR> > 4096 lib > <DIR> > 4096 media > <DIR> > 4096 mnt > <DIR> > 4096 opt > <DIR> > 4096 proc > > 62 README.txt > <DIR> > 4096 root > <DIR> > 4096 run > <DIR> > 12288 sbin > <DIR> > 4096 srv > <DIR> > 4096 sys > <DIR> > 4096 tmp > <DIR> > 4096 usr > <DIR> > 4096 var > > 150994944 testfile > > 20524388 capdl-loader-experimental-image-arm-tk1 > Tegra124 (TK1-SOM) # ext2load mmc 0 ${loadaddr} capdl-loader-experimental-image-arm-tk1 > 20524388 bytes read in 593 ms (33 MiB/s) > Tegra124 (TK1-SOM) # bootelf ${loadaddr} > CACHE: Misaligned operation at range [90000000, 90000014] > CACHE: Misaligned operation at range [90001000, 900091c4] > CACHE: Misaligned operation at range [900091c4, 900098d8] > CACHE: Misaligned operation at range [900198d8, 900198e0] > CACHE: Misaligned operation at range [900198e0, 91392ae0] > CACHE: Misaligned operation at range [91394000, 913a4820] > CACHE: Misaligned operation at range [913a4820, 913a8000] > ## Starting application at 0x90000000 ... > ELF loader: monitor mode init done > Copy monitor mode vector from 90001000 to a7f00000 size 50 > Number of IRQs: 192 > Load seL4 in nonsecure HYP mode 600001da > ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3 > paddr=[90000000..913a7fff] > ELF-loading image 'kernel' > paddr=[60000000..6003cfff] > vaddr=[e0000000..e003cfff] > virt_entry=e0000000 > > ------------------------------------------------------------------------------------------- > > Best Regards > -Daniel Wang > > > >

1 0

seL4 VMM Hangs during loading time
by Daniel Wang 02 Mar '18

02 Mar '18

Hi all, I’m trying to run seL as a microvisor following the CAMKES-ARM-VM. My development board is TK1-SOM from ColoradoEngineering. I was able to flash the U-boot to to load seL4 HYP mode. However when I try to load the kernel. The system just hangs. I got stuck here any help would be appreciated thank you! I built the capdl-loader-experimental-image-arm-tk1 and can copied it to the TK1 MMC storage, then I followed the wiki to setup env bootm_boot_mode to nonsec. Attachment is the printout: ------------------------------------------------------------------------------------------- U-Boot 2018.03-rc3-00090-g3990c9d (Mar 01 2018 - 14:33:40 -0500) TEGRA124 Model: Colorado Engineering TK1-SOM Board: CEI tk1-som DRAM: 2 GiB MMC: sdhci@700b0400: 1, sdhci@700b0600: 0 Loading Environment from MMC... OK In: serial Out: serial Err: serial Net: No ethernet found. Hit any key to stop autoboot: 0 Tegra124 (TK1-SOM) # setenv bootm_boot_mode nonsec Tegra124 (TK1-SOM) # saveenv Saving Environment to MMC... Writing to MMC(0)... OK Tegra124 (TK1-SOM) # ext2ls mmc 0 <DIR> 4096 . <DIR> 4096 .. <DIR> 16384 lost+found <DIR> 4096 boot <DIR> 4096 bin <DIR> 4096 dev <DIR> 12288 etc <DIR> 4096 home <DIR> 4096 lib <DIR> 4096 media <DIR> 4096 mnt <DIR> 4096 opt <DIR> 4096 proc 62 README.txt <DIR> 4096 root <DIR> 4096 run <DIR> 12288 sbin <DIR> 4096 srv <DIR> 4096 sys <DIR> 4096 tmp <DIR> 4096 usr <DIR> 4096 var 150994944 testfile 20524388 capdl-loader-experimental-image-arm-tk1 Tegra124 (TK1-SOM) # ext2load mmc 0 ${loadaddr} capdl-loader-experimental-image-arm-tk1 20524388 bytes read in 593 ms (33 MiB/s) Tegra124 (TK1-SOM) # bootelf ${loadaddr} CACHE: Misaligned operation at range [90000000, 90000014] CACHE: Misaligned operation at range [90001000, 900091c4] CACHE: Misaligned operation at range [900091c4, 900098d8] CACHE: Misaligned operation at range [900198d8, 900198e0] CACHE: Misaligned operation at range [900198e0, 91392ae0] CACHE: Misaligned operation at range [91394000, 913a4820] CACHE: Misaligned operation at range [913a4820, 913a8000] ## Starting application at 0x90000000 ... ELF loader: monitor mode init done Copy monitor mode vector from 90001000 to a7f00000 size 50 Number of IRQs: 192 Load seL4 in nonsecure HYP mode 600001da ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3 paddr=[90000000..913a7fff] ELF-loading image 'kernel' paddr=[60000000..6003cfff] vaddr=[e0000000..e003cfff] virt_entry=e0000000 ------------------------------------------------------------------------------------------- Best Regards -Daniel Wang

3 2

How to avoid timeout exceptions in non-buggy server code
by Kelly Dean 02 Mar '18

02 Mar '18

The article “Mixed-criticality support in seL4” at https://lwn.net/Articles/745946/ says seL4's solution to the problem of CPU budget exhaustion while in a non-reentrant shared data-structure server is timeout exceptions. The server might time out by chance, through no fault of its own. A more robust solution is to simply disallow calling any such server that advertises a WCET longer than the client's per-period CPU budget, and when a call is made, have the kernel check whether the client's remaining CPU budget ≥ server's WCET. If it is, then proceed with the call as normal. If it isn't, then verify that the client's per-period CPU budget ≥ server's WCET. If that verification succeeds, then terminate the budget for the client's current period early, and actually enter the server at the beginning of the client's _next_ period. (If the verification fails, then the kernel tells the client that the call is disallowed.) If the server fails to return before exhausting the client's CPU budget, then the server has violated its own WCET, which is a bug. Thus, a non-buggy server will never time out, so timeout exception handlers handle only bugs, not routine system operation. If the server's actual WCET is W, then from the client's point of view, the server's apparent WCET is almost 2W, because the client might make the call with remaining CPU budget X such that X is just barely less than W, in which case the kernel will terminate the client's current budget early (so the client loses X) and enter the server at the beginning of the next period, and the server might then take W to return, making the client wait X+W altogether (plus, of course, the remainder of the period, during which other VMs run). But with seL4's current solution, the server's apparent WCET is even longer than 2W, because the server could run for X, time out, be restarted (taking time R), then run for W, making the client wait X+R+W altogether.

2 5

Camkes limitations
by Sam Chenoweth 01 Mar '18

01 Mar '18

Hi, I like the Camkes (3) tool and believe it is essential for making seL4 accessible for developers. However, I have noticed some unexpected limitations that I believe are either bugs or incomplete features. Issue A: A hierarchical component cannot have a dataport with a custom data type. (However, a non-hierarchical component can have a dataport with a custom data type. Also, a hierarchical component can have a dataport with a built-in data type such as Buf.) Issue B: A dataport provided by a sub-component cannot be exported as a dataport belonging to the hierarchical component that contains it. (However, the export of event notifications from sub-components works just fine.) Attached is the relevant code that demonstrates both issues, which is a contrived example to highlight the issues without other stuff getting in the way. Please note that the code as is compiles just fine, however if you comment and uncomment a few lines of code (as instructed in Duck.camkes, Duckherd.camkes and Duckling.camkes), the issues can be demonstrated (separately) as compile failures. There may be other issues with hierarchical components that I am not yet aware of, as the above issues (unfortunately) have prevented me from experimenting with them further. Could you please acknowledge if these are issues that you are aware of, and if there is likely to be a fix in a future Camkes 4 release? Regards, Dr Samuel Chenoweth Cyber Security Researcher DST Group Note: I would have sent this email from my work email address ( samuel.chenoweth(a)dst.defence.gov.au) however I sent it from my personal address instead because of issues to do with our email gateway. All the contents of this email are UNCLASSIFIED and non-sensitive.

2 1

seL4 in an SGX enclave?
by Corey Richardson 28 Feb '18

28 Feb '18

This is email is me being kinda lazy. Does anyone know how challenging this would actually be to pull off? I'm interested in looking into it, but can't for a while. I feel like it makes sense to bootload some little stub that sets up seL4 as the only enclave in the system. I don't see any reason to have multiple enclaves when using seL4. But, from this, it should be possible to get a good static root of trust remote attestation on Google Cloud. (And also, can finally implement https://www.blackhat.com/docs/us-17/thursday/us-17-Swami-SGX-Remote-Attesta…) -- cmr http://octayn.net/ +16038524272

4 4

Fwd: CamkesVM CMA34CR_centos app
by Michal Podhradsky 21 Feb '18

21 Feb '18

Hi Kent, I did a fresh *repo init -u https://github.com/seL4/camkes-vm-manifest <https://github.com/seL4/camkes-vm-manifest> * so I am using the latest default.xml Now I can get a bit further - although still not all the way - here is the full output: https://gist.github.com/podhrmic/bc86178e60fad64ab870ff1fa19992 e3 and then the system as far as I can tell hangs - no serial or VGA output. What could be the cause? Regards M On Mon, Feb 19, 2018 at 4:07 PM, <Kent.Mcleod(a)data61.csiro.au> wrote: > Hi Michal, > > > Which revision of default.xml are you using? Adrian thinks it could be > potentially related to, and fixed by, this commit[1] if you don't have it > yet. > > > Kent > > > [1] https://github.com/seL4/seL4/commit/3d6f4f9bb7bfe42628df > a555601401fa4efcdf2d > > > > ------------------------------ > *From:* Devel <devel-bounces(a)sel4.systems> on behalf of Michal Podhradsky > <mpodhradsky(a)galois.com> > *Sent:* Tuesday, February 20, 2018 9:37 AM > *To:* devel(a)sel4.systems > *Subject:* [seL4] CamkesVM CMA34CR_centos app > > Hi all, > > I have a CM34CR CPU module <https://wiki.sel4.systems/CMA34DBMC> and I am > trying to run the related camkes app on it. > > I choose the centos app: https://github.com/seL4/camkes > -vm/blob/master/apps/vm/cma34cr_centos.camkes > > I am using default camkes vm manifest from https://github.com/seL4/camkes > -vm-manifest. > > Compile with: > > *make clean * > > *make cma34cr_centos_defcondig * > > *make silentoldconfig * > *make* > > And then I create a bootable USB following instructions here > <https://wiki.sel4.systems/Hardware/IA32>. > > Then after I load the kernel and capdl image, I get the following output > on serial: > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > *Boot config: parsing cmdline 'sel4kernel' Boot config: console_port = > 0x3f8 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false > Detected 1 boot module(s): module #0: start=0xd34000 end=0x3b387e8 > size=0x2e047e8 name='rootserver' Parsing GRUB physical memory map > Physical Memory Region from 0 size 9d400 type 1 Physical Memory Region > from 9d400 size 2c00 type 2 Physical Memory Region from e0000 size > 20000 type 2 Physical Memory Region from 100000 size 1ff00000 type 1 > Adding physical memory region 0x100000-0x20000000 Physical Memory > Region from 20000000 size 200000 type 2 Physical Memory Region from > 20200000 size 1fe04000 type 1 Adding physical memory region > 0x20200000-0x40004000 Physical Memory Region from 40004000 size 1000 > type 2 Physical Memory Region from 40005000 size 64bab000 type 1 Adding > physical memory region 0x40005000-0xa4bb0000 Physical Memory Region > from a4bb0000 size 1400000 type 2 Physical Memory Region from a5fb0000 > size 4a0f000 type 1 Adding physical memory region 0xa5fb0000-0xaa9bf000 > Physical Memory Region from aa9bf000 size 500000 type 2 Physical Memory > Region from aaebf000 size 100000 type 4 Physical Memory Region from > aafbf000 size 40000 type 3 Physical Memory Region from aafff000 size > 1000 type 1 Adding physical memory region 0xaafff000-0xab000000 > Physical Memory Region from ab000000 size 4a00000 type 2 Physical > Memory Region from f0000000 size 4000000 type 2 Physical Memory Region > from feb00000 size 4000 type 2 Physical Memory Region from fec00000 > size 1000 type 2 Physical Memory Region from fed10000 size a000 type 2 > Physical Memory Region from fed1c000 size 4000 type 2 Physical > Memory Region from fee00000 size 1000 type 2 Physical Memory Region > from ffc00000 size 400000 type 2 Physical Memory Region from 100000000 > size 14f600000 type 1 Adding physical memory region 0x100000000-0x24f600000 > Got VBE info in multiboot. Current video mode is 16767 ACPI: RSDP > paddr=0xfe020 ACPI: RSDP vaddr=0xfe020 ACPI: RSDT paddr=0xaafda0c4 ACPI: > RSDT vaddr=0xaafda0c4 Kernel loaded to: start=0x100000 end=0xc17000 > size=0xb17000 entry=0x101269 ACPI: RSDT paddr=0xaafda0c4 ACPI: RSDT > vaddr=0xaafda0c4 ACPI: FADT paddr=0xaaffb000 ACPI: FADT vaddr=0xaaffb000 > ACPI: FADT flags=0x3c6a5 ACPI: DMAR paddr=0xaafde000 ACPI: DMAR > vaddr=0xaafde000 ACPI: IOMMU host address width: 36 ACPI: registering > RMRR entry for region for device: bus=0x0 dev=0x1d fun=0x0 ACPI: > registering RMRR entry for region for device: bus=0x0 dev=0x1a fun=0x0 > ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x14 > fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 > dev=0x2 fun=0x0 ACPI: 2 IOMMUs detected ACPI: MADT paddr=0xaaff9000 ACPI: > MADT vaddr=0xaaff9000 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 > ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_APIC apic_id=0x1 ACPI: MADT_APIC > apic_id=0x2 ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC > apic_id=0x3 ACPI: Not recording this APIC, only support 2 ACPI: MADT_IOAPIC > ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 > gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: 2 > CPU(s) detected ELF-loading userland images from boot modules: > size=0x41fc000 v_entry=0x409000 v_start=0x400000 v_end=0x45fc000 > p_start=0x3b39000 p_end=0x7d35000 Moving loaded userland images to final > location: from=0x3b39000 to=0xc17000 size=0x41fc000 Starting node #0 with > APIC ID 0 Mapping kernel window is done ========== KERNEL EXCEPTION > ========== Vector: 0xd ErrCode: 0x0 IP: 0xffffffff80115c04 SP: > 0xffffffff80a0bfa0 FLAGS: 0x10046 CR0: 0x80010013 CR2: 0x0 > (page-fault address) CR3: 0xa12000 (page-directory physical address) > CR4: 0x110668 Stack Dump: *0xffffffff80a0bfa0 == 0x0 > *0xffffffff80a0bfa8 == 0x0 *0xffffffff80a0bfb0 == 0x3b39000 > *0xffffffff80a0bfb8 == 0xffffffff80116b80 *0xffffffff80a0bfc0 == 0x0 > *0xffffffff80a0bfc8 == 0x22a8 *0xffffffff80a0bfd0 == 0x0 > *0xffffffff80a0bfd8 == 0x0 *0xffffffff80a0bfe0 == 0xffffffff80000000 > *0xffffffff80a0bfe8 == 0x7e000 *0xffffffff80a0bff0 == 0xaa24c70c > *0xffffffff80a0bff8 == 0x1f *0xffffffff80a0c000 == 0xfffffffff000ba86 > *0xffffffff80a0c008 == 0xffffffff8081f0c0 *0xffffffff80a0c010 == 0x0 > *0xffffffff80a0c018 == 0x0 *0xffffffff80a0c020 == 0x0 *0xffffffff80a0c028 > == 0x0 *0xffffffff80a0c030 == 0x0 *0xffffffff80a0c038 == 0x0 Halting... > halting... Kernel entry via Interrupt, irq 0 * > > Any pointers at what is the cause of error here? The machien runs normally > with vanilla CentOS so I don't think it is a hardware issue. Also, I am > assuming the CMA34CR is identical to the one you have on your side (at > least checking the lspci output against the camkes description the memory > regions etc seem to match). > > Thanks in advance. > M >

3 3

split.c bootstrap.c failure?
by Richard Clark 21 Feb '18

21 Feb '18

Hi! What is this error and how might I go about tracking down the cause? <<seL4(CPU 0) [decodeUntypedInvocation/167 T0xe0792100 "csm-threads" @3a98c]: Untyped Retype: Slot #15 in destination window non-empty.>> _refill_pool@split.c:177 Failed to retype untyped, error 8 vka_alloc_object_at_maybe_dev@object.h:59 Failed to allocate object of size 4096, error 1 alloc_and_map@bootstrap.c:103 Failed to allocate bootstrap frame, error: 1 What I've done, is taken over the usual sel4test process and turned it into a little process that starts a few others. This error occurs at near the beginning of the main process, after it has allocated some untyped space for a secondary process, and just started it running. There is tons of memory available everywhere, and I do not understand why this is failing.... clues? Thanks! Richard H. Clark ________________________________ 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.

2 1

CamkesVM CMA34CR_centos app
by Michal Podhradsky 21 Feb '18

21 Feb '18

Hi all, I have a CM34CR CPU module <https://wiki.sel4.systems/CMA34DBMC> and I am trying to run the related camkes app on it. I choose the centos app: https://github.com/seL4/camkes-vm/blob/master/apps/vm/cma34cr_centos.camkes I am using default camkes vm manifest from https://github.com/seL4/camkes-vm-manifest. Compile with: *make clean* *make cma34cr_centos_defcondig* *make silentoldconfig* *make* And then I create a bootable USB following instructions here <https://wiki.sel4.systems/Hardware/IA32>. Then after I load the kernel and capdl image, I get the following output on serial: *Boot config: parsing cmdline 'sel4kernel'Boot config: console_port = 0x3f8Boot config: debug_port = 0x3f8Boot config: disable_iommu = falseDetected 1 boot module(s): module #0: start=0xd34000 end=0x3b387e8 size=0x2e047e8 name='rootserver'Parsing GRUB physical memory map Physical Memory Region from 0 size 9d400 type 1 Physical Memory Region from 9d400 size 2c00 type 2 Physical Memory Region from e0000 size 20000 type 2 Physical Memory Region from 100000 size 1ff00000 type 1Adding physical memory region 0x100000-0x20000000 Physical Memory Region from 20000000 size 200000 type 2 Physical Memory Region from 20200000 size 1fe04000 type 1Adding physical memory region 0x20200000-0x40004000 Physical Memory Region from 40004000 size 1000 type 2 Physical Memory Region from 40005000 size 64bab000 type 1Adding physical memory region 0x40005000-0xa4bb0000 Physical Memory Region from a4bb0000 size 1400000 type 2 Physical Memory Region from a5fb0000 size 4a0f000 type 1Adding physical memory region 0xa5fb0000-0xaa9bf000 Physical Memory Region from aa9bf000 size 500000 type 2 Physical Memory Region from aaebf000 size 100000 type 4 Physical Memory Region from aafbf000 size 40000 type 3 Physical Memory Region from aafff000 size 1000 type 1Adding physical memory region 0xaafff000-0xab000000 Physical Memory Region from ab000000 size 4a00000 type 2 Physical Memory Region from f0000000 size 4000000 type 2 Physical Memory Region from feb00000 size 4000 type 2 Physical Memory Region from fec00000 size 1000 type 2 Physical Memory Region from fed10000 size a000 type 2 Physical Memory Region from fed1c000 size 4000 type 2 Physical Memory Region from fee00000 size 1000 type 2 Physical Memory Region from ffc00000 size 400000 type 2 Physical Memory Region from 100000000 size 14f600000 type 1Adding physical memory region 0x100000000-0x24f600000Got VBE info in multiboot. Current video mode is 16767ACPI: RSDP paddr=0xfe020ACPI: RSDP vaddr=0xfe020ACPI: RSDT paddr=0xaafda0c4ACPI: RSDT vaddr=0xaafda0c4Kernel loaded to: start=0x100000 end=0xc17000 size=0xb17000 entry=0x101269ACPI: RSDT paddr=0xaafda0c4ACPI: RSDT vaddr=0xaafda0c4ACPI: FADT paddr=0xaaffb000ACPI: FADT vaddr=0xaaffb000ACPI: FADT flags=0x3c6a5ACPI: DMAR paddr=0xaafde000ACPI: DMAR vaddr=0xaafde000ACPI: IOMMU host address width: 36 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1d fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1a fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x14 fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x2 fun=0x0ACPI: 2 IOMMUs detectedACPI: MADT paddr=0xaaff9000ACPI: MADT vaddr=0xaaff9000ACPI: MADT apic_addr=0xfee00000ACPI: MADT flags=0x1ACPI: MADT_APIC apic_id=0x0ACPI: MADT_APIC apic_id=0x1ACPI: MADT_APIC apic_id=0x2ACPI: Not recording this APIC, only support 2ACPI: MADT_APIC apic_id=0x3ACPI: Not recording this APIC, only support 2ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xdACPI: 2 CPU(s) detectedELF-loading userland images from boot modules:size=0x41fc000 v_entry=0x409000 v_start=0x400000 v_end=0x45fc000 p_start=0x3b39000 p_end=0x7d35000Moving loaded userland images to final location: from=0x3b39000 to=0xc17000 size=0x41fc000Starting node #0 with APIC ID 0Mapping kernel window is done========== KERNEL EXCEPTION ==========Vector: 0xdErrCode: 0x0IP: 0xffffffff80115c04SP: 0xffffffff80a0bfa0FLAGS: 0x10046CR0: 0x80010013CR2: 0x0 (page-fault address)CR3: 0xa12000 (page-directory physical address)CR4: 0x110668Stack Dump:*0xffffffff80a0bfa0 == 0x0*0xffffffff80a0bfa8 == 0x0*0xffffffff80a0bfb0 == 0x3b39000*0xffffffff80a0bfb8 == 0xffffffff80116b80*0xffffffff80a0bfc0 == 0x0*0xffffffff80a0bfc8 == 0x22a8*0xffffffff80a0bfd0 == 0x0*0xffffffff80a0bfd8 == 0x0*0xffffffff80a0bfe0 == 0xffffffff80000000*0xffffffff80a0bfe8 == 0x7e000*0xffffffff80a0bff0 == 0xaa24c70c*0xffffffff80a0bff8 == 0x1f*0xffffffff80a0c000 == 0xfffffffff000ba86*0xffffffff80a0c008 == 0xffffffff8081f0c0*0xffffffff80a0c010 == 0x0*0xffffffff80a0c018 == 0x0*0xffffffff80a0c020 == 0x0*0xffffffff80a0c028 == 0x0*0xffffffff80a0c030 == 0x0*0xffffffff80a0c038 == 0x0Halting...halting...Kernel entry via Interrupt, irq 0* Any pointers at what is the cause of error here? The machien runs normally with vanilla CentOS so I don't think it is a hardware issue. Also, I am assuming the CMA34CR is identical to the one you have on your side (at least checking the lspci output against the camkes description the memory regions etc seem to match). Thanks in advance. M

2 2

CamkesVM: EthDriver and Firewall
by Michal Podhradsky 16 Feb '18

16 Feb '18

Hi all, I have some clarifying questions about the Ethernet driver <https://github.com/seL4/camkes-vm/tree/master/components/Ethdriver> and the Firewall <https://github.com/seL4/camkes-vm/tree/master/components/Firewall> components. 1. Does the ethernet driver return a raw ethernet frame and the consumer of the data has to strip the MAC header etc or does the driver return only payload (IP, ARP etc data)? 2. has the Firewall component been tested and does it work? (I know it is a part of CMA34_centos_defconfig but I don't have a way to test it right now) Thanks for the info. M

2 1

Idris now working on seL4
by jonas.cl＠protonmail.com 13 Feb '18

13 Feb '18

Hi, I am interested in both seL4 and Idris (https://www.idris-lang.org/ a dependently typed pure functional language), so I have written an seL4 project that compiles an "hello world" Idris application. My intention is to eventually write the seL4 tutorials using Idris. Any help, comments or contributions to the repositories is appreciated, especially to the idris-libsel4-ffi repo that currently is very limited. The following repositories are created to accomplish this: The project configuration https://github.com/mokshasoft/sel4-idris-manifest The app itself https://github.com/mokshasoft/sel4-idris-apps The Idris RTS (ported and built for seL4) https://github.com/mokshasoft/libsel4-idris-rts The libsel4 FFI (very limited implementation so far) https://github.com/mokshasoft/idris-libsel4-ffi Regards Jonas Sent from [ProtonMail](https://protonmail.com), Swiss-based encrypted email.

1 0

Re: [seL4] RefOS Building and Execution Error
by ALVI Aslam (MORPHO) 13 Feb '18

13 Feb '18

Hello Peter, Thank you for your support, I will try to run RefOS as per your instructions. I have also updated the RefOS at my local repo to make it runnable with default.xml And it working fine. If you want I can push my changes to you. Thanks & Regards, Aslam

2 1

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

Strange Behevior with cma34cr.
by Dan DaCosta 08 Feb '18

08 Feb '18

To Whom It May Concern: My name is Dan DaCosta and I am working with Rockwell on a smaccms transition project referred to as HTA. The manifest associated with this project can be found here: https://github.com/smaccm/hta This manifest is mostly concerned with targeting the cma34cr board. When building images using a Fedora 26 based OS that relies on gcc 7 the following fault occurs: FAULT HANDLER: data fault from vm.ethdriver.control (ID 0x202) on address > 0x1076878, pc = 0x4070d5, fsr = 0x6 > FAULT HANDLER: rip = 0x4070d5 > FAULT HANDLER: rsp = 0x1076880 > FAULT HANDLER: rax = 0 > FAULT HANDLER: rbx = 0xe68000 > FAULT HANDLER: rcx = 0x8 > FAULT HANDLER: rdx = 0x5 > FAULT HANDLER: rsi = 0xe61000 > FAULT HANDLER: rdi = 0xc > FAULT HANDLER: r8 = 0 > FAULT HANDLER: r9 = 0 > FAULT HANDLER: r10 = 0x16997e000 > FAULT HANDLER: r11 = 0x246 > FAULT HANDLER: r12 = 0 > FAULT HANDLER: r13 = 0x404a70 > FAULT HANDLER: r14 = 0 > FAULT HANDLER: r15 = 0 > FAULT HANDLER: rflags = 0x10246 > FAULT HANDLER: tls_base = 0 > FAULT HANDLER: memory map: > FAULT HANDLER: +-- 0x0000000001081fff -- > FAULT HANDLER: | guard page > FAULT HANDLER: +-- 0x0000000001081000 -- > FAULT HANDLER: | stack > FAULT HANDLER: +-- 0x000000000107d000 -- > FAULT HANDLER: | guard page > FAULT HANDLER: +-- 0x000000000107c000 -- > FAULT HANDLER: | <undescribed> > FAULT HANDLER: +-- 0x0000000001069fff -- > FAULT HANDLER: | guard page > FAULT HANDLER: +-- 0x0000000001069000 -- > FAULT HANDLER: | IPC buffer > FAULT HANDLER: +-- 0x0000000001068000 -- > FAULT HANDLER: | guard page > FAULT HANDLER: +-- 0x0000000001067000 -- > FAULT HANDLER: | <undescribed> > FAULT HANDLER: +-- 0x000000000105dfff -- > FAULT HANDLER: | code and data > FAULT HANDLER: +-- 0x0000000000400000 -- > The config I am primarily interested in is named "cma34cr_centos_defconfig" but I seem to have similar problems for all the cma34cr defconfigs. I was successful at building working images when I switched to building on Ubuntu 16.04 LTS. This distribution version uses gcc 5.4. Thanks! Dan DaCosta

2 1

OS Engineers Wanted!
by Gernot.Heiser＠data61.csiro.au 31 Jan '18

31 Jan '18

Would you like to get paid for making the world more secure with seL4? I'm in charge of directing OS development for the newly-founded company Hensoldt Cyber. We will develop an integrated, highly-secure hardware-software solution, combined with secure production, aimed at changing the game in securing real-world embedded/cyber-physical systems. Needless to say, there will be close collaboration with the Data61 Trustworthy Systems team. We're now hiring engineers who will help us getting there. Specifically, we're looking for strongly-motivated people with practical experience in OS development, although there is flexibility with the degree of experience. Actual experience with seL4 (or even lesser microkernels ;-) would be awesome. Place of work will be Munich (no remote work possible, sorry). You'll have to be prepared to obtain a German government security clearance (German citizenship is not a requirement for this). Interested? Please send me your CV. Gernot

1 0

seL4 as TEE OS in TrustZone
by Daniel (Xiaolong) Wang 30 Jan '18

30 Jan '18

Hi all, I’m exploring for possible ways to run seL4 as a secure TEE kernel in TrustZone. I found an old discussion thread back in 2016 and corresponding from Gernot: I’m very new to TrustZone technology. I wonder has anyone done that before using seL4? Is there any public available resources for reference? Also on which development board did Data61 run seL4 in the secure world? Thanks -Dan FYI Is it possible to run sel4 as a secure world OS in TrustZone? Has anyone successfully done that before? I believe we have done that in the past (with platforms where we could just ignore the secure/normal split and ran everything in secure mode). There is no reason why it wouldn’t work, it just comes down to initialising the platform correctly. https://sel4.systems/pipermail/devel/2016-March/000750.html <https://sel4.systems/pipermail/devel/2016-March/000750.html> Thanks -Dan

4 7

seL4 as a hypervisor running a linux guest and a RToS(or native sel4 applications) on ARM
by Joel Svensson 29 Jan '18

29 Jan '18

Hello, I'm trying to form an understanding of what one can do with seL4 and how much work is involved in doing it. I am currently under the impression that seL4 could act as a hypervisor and run a linux guest. But I have not found easily accessible instructions for how to do this (ARM targets are most interesting, the Raspberry Pi preferably as it is cheap and ubiquitously available). Did anyone here set up such a seL4 as hypervisor for linux guest and document the procedure? I would be very thankful for links. If such a setup is doable, can you still run some native seL4 code on the "hypervisor" then? Thank you very much /JS

2 2

python-capdl sets incorrect permissions on elf setions
by Joseph Takagi 29 Jan '18

29 Jan '18

Hi I believe the capdl python tool does not correctly set permissions on data loaded from component ELF files. I am wondering if this is a known issue with a fix or whether I'm best off diving in and attempting to fix it myself. Im running on a 32-bit ARM platform The camkes generated linker scripts result in several ELF sections (including .rodata .text and .bss) being lumped together in a single ELF segment. The permissions on this segment in the ELF segment header are RWE. This can be seen from the example output below. readelf -l foo_group_bin Elf file type is EXEC (Executable file) Entry point 0x107b64 There are 4 program headers, starting at offset 52 Program Headers: Type Offset VirtAddr PhysAddr FileSiz MemSiz Flg Align EXIDX 0x021ad8 0x00111ad8 0x00111ad8 0x00008 0x00008 R 0x4 LOAD 0x010000 0x00100000 0x00100000 0x12178 0xd9000 RWE 0x10000 <-- .bss .text .rodata etc. are here with RWE permissions LOAD 0x030000 0x00200000 0x00200000 0x00000 0x01000 RW 0x10000 GNU_STACK 0x000000 0x00000000 0x00000000 0x00000 0x00000 RWE 0x10 Section to Segment mapping: Segment Sections... 00 .ARM.exidx 01 .text .init .fini .rodata .eh_frame .ARM.exidx .data .init_array .fini_array .jcr __vsyscall .bss guarded 02 ignore_fooregs 03 The individual sections are given more sensible permissions via their respective section headers, as can be seen below: .text has permissions 'AE' for alloc and execute, .rodata has 'A' and .bss has 'AW', etc. readelf -S ./foo_group_bin There are 28 section headers, starting at offset 0x8524c: Section Headers: [Nr] Name Type Addr Off Size ES Flg Lk Inf Al [ 0] NULL 00000000 000000 000000 00 0 0 0 [ 1] .text PROGBITS 00100000 010000 00eb68 00 AX 0 0 4096 <-- .text can't be written [ 2] .init PROGBITS 0010eb68 01eb68 000014 00 AX 0 0 4 [ 3] .fini PROGBITS 0010eb7c 01eb7c 000014 00 AX 0 0 4 [ 4] .rodata PROGBITS 0010f000 01f000 002ad4 00 A 0 0 4096 <-- .rodata is read-only [ 5] .eh_frame PROGBITS 00111ad4 021ad4 000004 00 A 0 0 4 [ 6] .ARM.exidx ARM_EXIDX 00111ad8 021ad8 000008 00 AL 1 0 4 [ 7] .data PROGBITS 00112000 022000 000168 00 WA 0 0 4096 [ 8] .init_array INIT_ARRAY 00112168 022168 000004 00 WA 0 0 4 [ 9] .fini_array FINI_ARRAY 0011216c 02216c 000004 00 WA 0 0 4 [10] .jcr PROGBITS 00112170 022170 000004 00 WA 0 0 4 [11] __vsyscall PROGBITS 00112174 022174 000004 00 WA 0 0 4 [12] .bss NOBITS 00112178 022178 000b08 00 WA 0 0 8 [13] guarded NOBITS 00113000 022178 0c6000 00 WA 0 0 4096 [14] ignore_fooregs NOBITS 00200000 030000 001000 00 WA 0 0 1048576 [15] .debug_info PROGBITS 00000000 022178 027a60 00 0 0 1 [16] .debug_abbrev PROGBITS 00000000 049bd8 00a4d4 00 0 0 1 [17] .debug_loc PROGBITS 00000000 0540ac 0113f1 00 0 0 1 [18] .debug_aranges PROGBITS 00000000 0654a0 000ef8 00 0 0 8 [19] .debug_line PROGBITS 00000000 066398 00c5ff 00 0 0 1 [20] .debug_str PROGBITS 00000000 072997 0060c1 01 MS 0 0 1 [21] .comment PROGBITS 00000000 078a58 000038 01 MS 0 0 1 [22] .ARM.attributes ARM_ATTRIBUTES 00000000 078a90 000039 00 0 0 1 [23] .debug_frame PROGBITS 00000000 078acc 002638 00 0 0 4 [24] .debug_ranges PROGBITS 00000000 07b108 002238 00 0 0 8 [25] .shstrtab STRTAB 00000000 085137 000114 00 0 0 1 [26] .symtab SYMTAB 00000000 07d340 005230 10 27 1269 4 [27] .strtab STRTAB 00000000 082570 002bc7 00 0 0 1 Key to Flags: W (write), A (alloc), X (execute), M (merge), S (strings) I (info), L (link order), G (group), T (TLS), E (exclude), x (unknown) O (extra OS processing required) o (OS specific), p (processor specific) The ELF.py code from python-capdl applies the segment permissions to the entire segment so disregards the permissions in the ELF section headers. As a result, data which shouldn't be writable or executable are so. I can confirm this through analysis of the capdl output which shows the entire segment being mapped as 64KB pages with RWE permissions set. Any advice on this would be appreciated. Joe Takagi

2 1

Fileserver connection error in RefOS
by ALVI Aslam (MORPHO) 24 Jan '18

24 Jan '18

Hello All, Greetings, I was trying to run RefOs for ia32_defconfig. Found some error while building but after removing all of them I was able to run it. But now I have an error while selfLoader is trying to laod Terminal or Timer_Server. [00.0] SELFLOADER | main(): --- Starting RefOS process selfloader --- [00.1] SELFLOADER | main(): Connect to the server for [/fileserv/terminal] ERROR main(): Error while connecting to file server. [00.84] PROCSERV | proc_exit_handler(): Process PID 2043 exiting with status 0 !!! [00.85] PROCSERV | proc_syscall_postaction(): Releasing process 2043 [/fileserv/terminal]... [00.0] SELFLOADER | main(): --- Starting RefOS process selfloader --- [00.1] SELFLOADER | main(): Connect to the server for [fileserv/timer_server] ERROR main(): Error while connecting to file server. I have also attached the full log of execution. I have also debugged it and found that while resolving the serverPath its get failed. Please help me out to resolve this issue. Thank You in advance Regards, Aslam

1 0

Hyperkernel paper
by Jeff Waugh 23 Jan '18

23 Jan '18

Hi seL4 friends, Any thoughts and/or feelings about the Hyperkernel paper from SOSP'17? This paper describes an approach to designing, implementing, and formally > verifying the functional correctness of an OS kernel, named Hyperkernel, > with a high degree of proof automation and low proof burden. https://homes.cs.washington.edu/~helgi/papers/hyperkernel.pdf Thanks, Jeff

2 1

Userspace Debugging for ia32
by ALVI Aslam (MORPHO) 23 Jan '18

23 Jan '18

Hello Team, I need some help to start a userspace debugging for ia32. Since as per the instruction mention in the link https://wiki.sel4.systems/Debugging%20guide I was able to use GDB for kzm based defconig. But how can I start userspace debugging for ia32 based defconig? Thank You & Regards, Aslam

2 1

seL4 vs. Integrity-178B
by Baconicsynergy 22 Jan '18

22 Jan '18

Hello friends :) First off, congratulations on being the new primary microkernel of choice for the Genode Operating System Framework! I'm very excited. Now to my questions - how does the formal verification of seL4 compare with the Integrity-178B security guarantees? Also, how do two structurally compare with each other in terms of design principles and implementation? Best regards, Joel Desermeau seL4

2 1

seL4 8.0.0 and CAmkES camkes-3.2.0 release
by Kent.Mcleod＠data61.csiro.au 18 Jan '18

18 Jan '18

seL4 8.0.0 and CAmkES camkes-3.2.0 release = seL4 8.0.0 = Note: Meltdown and Spectre patches are not included in this release and will be included in a forthcoming release once they have been verified. Once they are merged they will still be accessible through the master branch of seL4 on github. Release notes: https://wiki.sel4.systems/seL4%208.0.0 CHANGES file in https://github.com/seL4/seL4/tree/8.0.0 = CAmkES camkes-3.2.0 = Release notes: https://wiki.sel4.systems/camkes-3.2.0 CHANGES file in https://github.com/seL4/camkes-tool/tree/camkes-3.2.0 = Miscellaneous updates = == CMake build system == Replacing the current kbuild build system with a new CMake build system is still in progress. The kernel only CMake build is now used by l4v. Initial CMake versions for sel4test, sel4bench and our CAmkES projects are still being developed. We intend to do a release that contains the Kbuild and CMake scripts working side by side, and will then start to remove the Kbuild scripts after that. == Changes to manifests for our projects == Each project that we maintain now has a default.xml and master.xml manifest file. master.xml is used to specify the branch tips of the upstream git repositories that a project uses. default.xml now pins all of the repositories to revisions that last passed our regression tests. For this current release and future releases a release tag will be created on each manifest repo specifying the revision of default.xml that uses the released revisions of all the repositories. The seL4 and camkes-tool repos will still be tagged on each release, and all other repositories will have versioned branches created the same as before. We have only just finished testing this change and the various documentation will be updated over the coming days. == Meltdown and Spectre == As mentioned above, Meltdown and Spectre related patches are not present in this release and will be merged into the kernel once verification is complete. There will likely be a blog post accompanying their release. ?

1 0

Re: [seL4] x86 kernel address space side channels
by Jeroen "Slim" van Gelderen 05 Jan '18

05 Jan '18

Thanks for clarifying that. Do you have any information on whether AMD is wrong claiming that their architecture is not vulnerable? On Thu, Jan 4, 2018 at 11:29 AM, Alex Elsayed <eternaleye(a)gmail.com> wrote: > > On Jan 4, 2018 07:37, "Jeroen "Slim" van Gelderen" <askslim(a)gmail.com> > wrote: > > On Wed, Jan 3, 2018 at 4:37 PM, Alex Elsayed <eternaleye(a)gmail.com> wrote: > >> In addition, Intel has published a press release, claiming that this >> issue (counter to some claims elsewhere) does in fact affect other >> vendors and architectures: >> >> https://newsroom.intel.com/news/intel-responds-to-security-r >> esearch-findings/ > > > Contrary to the PR, Intel CPUs do indeed have a design flaw aka bug which > makes them vulnerable to Meltdown. Meltdown has not been reproduced on ARM > or AMD and AMD thinks Meltdown is not applicable to their chips due to > architectural differences. > > The Spectre attack is the attack that is applicable across the board. > > As far as Linux is concerned only Intel machines will be hit with the > KPI-related slowdown (5%-30%) since KPI will be disabled on AMD CPUs. (And > I assume this goes for Windows too.) This looks bad for Intel, hence the > FUD. > > > It's a bit more nuanced than that. First of all, section 6.4 of the > Meltdown paper is quite clear: non-Intel CPUs _do_ still perform the > problematic access; it's the particular covert channel they use to extract > the information from it that does not port over. Many expect this to > change; the authors themselves see that whether AMD or ARM are affected is > _unknown-_, not that they are unaffected. > > Second, the patch from AMD to disable KPTI has not been accepted AFAIK, > and AArch64 is adding KPTI. > > Third, Meltdown is a _less severe_ attack by far compared to Spectre. > Meltdown can be addressed by KPTI, but some forms of Spectre use little > besides the BTB, which is known[1] to be infeasible to flush in software. > > Fourth, Intel (and I) posted that link _prior_ to the release of the > papers, at a time when all that was known to the public was "very serious > vulnerability in speculative execution" - its claims should be read in that > context. > > [1]: https://arxiv.org/abs/1612.04474 > > > -- Jeroen "Slim" van Gelderen

1 0

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