- Devel - lists.sel4.systems

Trustworthy and mixed critical
by Jonathan C Day 14 Jun '17

14 Jun '17

Dear all, The first of these terms has an... interesting history. In a nutshell, it's not always used appropriately. Clearly that's not going to be the case with SEL4, but what exactly is meant? Mixed critical is another term that I'm cautious over. It's not completely clear to me if the mixing refers to relaxed constraints for utilisation reasons or something else. (Correct me if I'm mistaken, but I don't think SEL4 implements FLASK, which would be the obvious way to provide differing constraints, relaxed constraints within the trusted computing model. It's totally the wrong level.) I have absolutely no doubt SEL4 will retain all the provable integrity ever claimed (by anyone involved), but this experimental-proto-main branch confuses me on what fundamentally changes. Jonathan Day

2 1

Compilation of seL4 kernel 5.2.0
by Alexander Boettcher 14 Jun '17

14 Jun '17

Hello, I want to compile just the seL4 kernel (5.2.0) and tried it by invoking: alex@max:~/sel4.git$ ARCH=x86 PLAT=pc99 SEL4_ARCH=ia32 make but the compile fails (attached below). Do I need to setup/configure something beforehand ? It seems some defines are not set. The host is a 64bit Ubuntu 16.04 LTS. Thanks, Alex. alex@max:~/sel4.git$ git log commit 3695232f9603af60d56f97072082d90f30e98b0e Author: Kent McLeod <Kent.Mcleod(a)data61.csiro.au> Date: Wed May 31 17:21:29 2017 +1000 update VERSION file to 5.2.0 alex@max:~/sel4.git$ ARCH=x86 PLAT=pc99 SEL4_ARCH=ia32 make [MKDIR] arch/object [PBF_GEN] arch/object/structures.pbf [PBF_GEN] plat/32/plat_mode/machine/hardware.pbf [PBF_GEN] 32/mode/api/shared_types.pbf [BF_GEN] arch/object/structures_gen.h [BF_GEN] plat/32/plat_mode/machine/hardware_gen.h [BF_GEN] 32/mode/api/shared_types_gen.h [CPP] src/arch/x86/32/machine_asm.s_pp [AS] src/arch/x86/32/machine_asm.o [CPP] src/arch/x86/32/traps.s_pp [AS] src/arch/x86/32/traps.o [CPP] src/arch/x86/32/head.s_pp [AS] src/arch/x86/32/head.o [CPP] src/arch/x86/multiboot.s_pp [AS] src/arch/x86/multiboot.o [TOUCH] sources_list_updated [CPP_GEN] kernel_all.c [CPP] kernel_all.c_pp In file included from ./include/arch/x86/arch/fastpath/fastpath.h:14:0, from src/arch/x86/32/c_traps.c:15: ./include/arch/x86/arch/32/mode/fastpath/fastpath.h:137:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ ./include/arch/x86/arch/32/mode/fastpath/fastpath.h:168:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ src/arch/x86/32/c_traps.c:198:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ src/arch/x86/32/c_traps.c:238:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ Makefile:729: recipe for target 'kernel_all.c_pp' failed make: *** [kernel_all.c_pp] Error 1 rm plat/32/plat_mode/machine/hardware_gen.h 32/mode/api/shared_types_gen.h src/arch/x86/32/machine_asm.s_pp src/arch/x86/32/traps.s_pp src/arch/x86/multiboot.s_pp arch/object/structures_gen.h src/arch/x86/32/head.s_pp -- 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 2

seL4-test on Beaglebone black
by Fabrizio Bertocci 14 Jun '17

14 Jun '17

Hi, I am posting this email as reference to anyone who want/need to run seL4 on a BeagleBone Black (BBB). The post at https://wiki.sel4.systems/Hardware/Beaglebone is great, unfortunately even if I followed exactly those instructions, I ended up hitting some walls here and there. I eventually managed to solve those issues and run successfully seL4test on my BBB. First of all the build system. I have tried unsuccessfully to find arm-linux-eabi for CentOS 7 (my preferred distribution for building on Linux), but apparently is an easy-to-find only on Ubuntu... so I ended up creating a VM with Ubuntu 16.04. If someone knows how to get arm-linux-eabi on CentOS please let me know... Unfortunately even with Ubuntu not everything went as smooth as I hoped. It appears that Python "past" module is no longer available for 16.04, so build fails on kernel/tools/lex.py. According to the comment right before the failing import statement, it appears this module is just declared but not used, so commenting it out (or removing it entirely) would fix this issue: #from past.builtins import cmp One more issue: when using either one of the following configurations as start point: - bamboo_bbone_black_debug_xml_defconfig - bbone_black_debug_xml_defconfig The build system will end up producing a binary image and not an ELF image. Producing an ELF image can be more useful if you want to use objdump to get a disassembly (for debugging later). So I changed the configuration with: make menuconfig Navigate to: Tools -> Build elfloader -> Boot image type and select "ELF Boot Image" instead of "Binary Boot Image" Save your configuration then build: make Now manually convert the produced ELF image in a binary: arm-linux-gnueabi-objcopy --output-target binary images/sel4test-driver-image-arm-am335x sel4test.bin then copy the file 'sel4test.bin' onto the SD card formatted as FAT32 Now, in my BBB (rev A5A) if I try to follow the instructions from the wiki page previously mentioned, I get a crash right away (illegal instruction). The problem is that in my BBB the uBoot environment variable ${loadaddr} is set to 0x80200000 and not 0x82000000 (the start address of the produced image). BBB have RAM mapped from address 0x80000000 to 0x9FFFFFFF (512Mb), so running from 0x82000000 is ok. So to load and run, use instead: fatload mmc 0 0x82000000 sel4test.bin go 0x82000000 That's it. Test should load and run successfully: Test suite passed. 220 tests passed. 220/220 tests passed. All is well in the universe. Hope this help saving some time... Regards, Fabrizio

1 0

Important note for CAmkES users
by Stephen.Sherratt＠data61.csiro.au 13 Jun '17

13 Jun '17

We've just released CAmkES 3.0.0 (release notes<https://wiki.sel4.systems/CAmkES%203.0.0>), and with it, all changes staged on our development branch, CAmkES Next, have been merged into the "master" branch of the camkes-tool repo (https://github.com/seL4/camkes-tool) We'll be continuing to develop CAmkES on its "master" branch, and cease making new commits to the "next" branch. # What this means for you As CAmkES 3.0.0 is incompatible with older versions of CAmkES, any projects tracking the master branch of camkes-tool will probably not build after this change. Also, as all new development is now being done on the master branch, any projects tracking the next branch of camkes-tool will no longer receive updates. If you're in either category, you'll need to update your project's repo manifest. # Migration Instructions If your project tracks either the "master", or "next" branch of the camkes-tool, you'll need to update your project's manifest. To check if this applies to you, look in your projects repo manifest xml file (typically in .repo/manifest.xml at the top level of your project) for the line: <project name="camkes-tool.git" path="tools/camkes"> (this implicitly tracks "master") OR <project name="camkes-tool.git" path="tools/camkes" revision="master"> OR <project name="camkes-tool.git" path="tools/camkes" revision="next"> If your manifest has either of those lines, take a look at the migration guide in the CAmkES 3.0.0 release notes: https://wiki.sel4.systems/CAmkES%203.0.0#Migrating It covers a range of different scenarios and explains how to change your manifest so your project will continue to work. If the camkes-tool revision in your manifest specifies a particular version of CAmkES (e.g. 'revision="camkes-2.3.1"'), you don't need to migrate.

1 0

Pre-release of mixed criticality seL4 extensions
by Anna.Lyons＠data61.csiro.au 13 Jun '17

13 Jun '17

= seL4-5.2.0-mcs = The first round of mixed-criticality extensions for seL4 are now available for your perusal and usage. This is a prerelease of features that are currently our candidate for verification. They are *not* verified and most likely contain bugs. If you encounter any, please report them ;) We have more features in development coming, but this is the first lot. = Release Notes = Detailed release notes can be found on our wiki: https://wiki.sel4.systems/seL4%205.2.0-mcs = Upgrade Notes = This version is not compatible with seL4 5.2.0, but forks the API based on that kernel version. Branches are available in most of our libraries to use, and CAmkES and capdl already have support for this pre-release on their latest release and master branch. = Major Changes = A summary of major changes can be found at: https://wiki.sel4.systems/seL4%205.2.0-mcs#Highlights A tutorial covering the new features can be found at: https://wiki.sel4.systems/seL4%205.2.0-mcs = Source Code = https://github.com/seL4/seL4/tree/5.2.0-mcs = Full Change Log = Use: git log 5.2.0..5.2.0-mcs

1 0

Announcing CAmkES 3.0.0
by Stephen.Sherratt＠data61.csiro.au 13 Jun '17

13 Jun '17

We're pleased to announce the release of CAmkES 3.0.0. This is a major release, which contains all work from our development branch, also known as CAmkES Next. Future development on CAmkES will occur on the "master" branch. Importantly, this means no further commits will be made to the "next" branch, so users will need to update their manifests to point at the "master" branch, or alternatively, the "camkes-3.0.0" tag created with this release. = Release Notes = Detailed release notes can be found on our wiki: https://wiki.sel4.systems/CAmkES%203.0.0 = Upgrade Notes = Dependencies for running CAmkES have changed since the previous release. Instructions for installing dependencies on several linux distros can be found here: https://wiki.sel4.systems/CAmkES#Build_dependencies If you were tracking the master branch of the camkes-tool in your project, you'll need to modify your project's manifest for it to continue to work. Migration instructions for a variety of situations can be found at: https://wiki.sel4.systems/CAmkES%203.0.0#Migrating = Major Changes = A summary of major changes can be found at: https://wiki.sel4.systems/CAmkES%203.0.0#New_Features = Examples = mkdir camkes-examples && cd camkes-examples repo init -u https://github.com/seL4/camkes-manifest.git -m default-3.0.x.xml repo sync tests/x86-simple.tcl # builds and runs simple example = Source Code = https://github.com/seL4/camkes-tool/ = Full Change Log = Use: git log camkes-3.0.0...$(git merge-base camkes-2.3.1 camkes-3.0.0) = More Details = Manual: https://github.com/seL4/camkes-tool/blob/camkes-3.0.0/docs/index.md Wiki: https://wiki.sel4.systems/CAmkES Enjoy!

1 0

Missing pico_device.h
by Michal Podhradsky 09 Jun '17

09 Jun '17

Hello, the recent commits in broke the build of util_libs <https://github.com/seL4/util_libs/commits/master> broke the build of camkes- <https://github.com/seL4/camkes-vm>vm <https://github.com/seL4/camkes-vm>. To recreate the error, do: mkdir test_defaultcd test_defaultrepo init -u https://github.com/seL4/camkes-vm-manifest.gitrepo sync make cleanmake optiplex9020_defconfigmake silentoldconfigmake You will get: *In file included from /test_default/libs/libethdrivers/src/pico_dev_eth.c:15:0:/test_default/stage/x86/pc99/include/ethdrivers/pico_dev_eth.h:16:26: fatal error: pico_device.h: No such file or directorycompilation terminated.* Regards Michal

1 0

Temporally disable write-access on memory pages
by Norrathep Rattanavipanon 09 Jun '17

09 Jun '17

Hello, I have a question regarding the best way to temporally disable write-access on memory pages. Suppose in the user-space, there are two processes: initial user-space process and process A, which is created by the initial process. Process A has its own virtual memory space. Now we want to find a way to enforce the memory inside process A to be temporally R/O to process A (since we want to have the initial process compute a function on that memory snapshot.) Currently, what we are doing now is to lock all memory pages of process A by calling the "remap" function inside the initial process. But then we realize that doing that does not help much. Since process A owns capabilities to its memory pages, process A also can call "remap" function to unlock the locked memory pages (please correct me if it's wrong). This will cause the memory to be inconsistent when computing a function on that memory. My question is is there anyway to enforce how a page locking (make it R/O) works in seL4 so that ONLY the entity that locked the page can unlock it? For example, in this case, we want to make sure that only the initial process can unlock the pages that he locked earlier. Thank you, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 2

Fwd: k_vmm_manager: failed on sel4 hypervisor connection
by Michal Podhradsky 08 Jun '17

08 Jun '17

Hello all, I am running camkes-vm on x86 architecture, following the example on wiki https://wiki.sel4.systems/CAmkESVM#Cross_VM_Connectors with the exception that I want to invoke the stringReverse component <https://github.com/podhrmic/camkes-vm/tree/master/components/StringReverse> . I am running the optiplex9020_defconfig example with only one VM, and when I start booting the guest linux system, I see the following error: *[ 1.282326] dataport: loading out-of-tree module taints kernel.* *[ 1.290615] dataport: module license 'unspecified' taints kernel.* *[ 1.306854] Disabling lock debugging due to kernel taint* *[ 1.319664] dataport initialized with major number 247* *vmm_vmcall_handler:55 | Failed to find handler for token:2* *[ 1.325411] incorrect event context magic number (expected 42, got -677408512)insmod: can't insert '/lib/modules/4.8.16/kernel/drivers/vmm/consumes_event.ko': Operation not ermitted* *[ 1.337441] emits_event initialized with major number 245* *[ 1.356391] k_vmm_manager: failed on sel4 hypervisor connection |-1|* Then when I log into linux and call `string_reverse <https://github.com/podhrmic/camkes-vm/tree/master/linux/pkg/string_reverse>` program, I get the following error: *# string_reverse * *[ 8.360164] BUG: unable to handle kernel paging request at d881f2c0* *[ 8.360164] IP: [<d00a69f0>] chrdev_open+0xab/0x100* *[ 8.360164] *pde = 17867067 *pte = 00000000 * *[ 8.360164] Oops: 0000 [#1]* *[ 8.360164] Modules linked in: emits_event(PO) dataport(PO)* *[ 8.360164] CPU: 0 PID: 691 Comm: string_reverse Tainted: P O 4.8.16 #1* *[ 8.360164] task: d79c9740 task.stack: d6ae0000* *[ 8.360164] EIP: 0060:[<d00a69f0>] EFLAGS: 00010286 CPU: 0* *[ 8.360164] EIP is at chrdev_open+0xab/0x100* *[ 8.360164] EAX: d881f2c0 EBX: 00000000 ECX: d79b0d00 EDX: 00000000* *[ 8.360164] ESI: d79b0d00 EDI: d6add808 EBP: d6ae1e10 ESP: d6ae1df8* *[ 8.360164] DS: 007b ES: 007b FS: 0000 GS: 0033 SS: 0068* *[ 8.360164] CR0: 80050033 CR2: d881f2c0 CR3: 16ad9000 CR4: 00102690* *[ 8.360164] DR0: 00000000 DR1: 00000000 DR2: 00000000 DR3: 00000000* *[ 8.360164] DR6: fffe0ff0 DR7: 00000400* *[ 8.360164] Stack:* *[ 8.360164] d7ac9be0 d7ac9be0 00000001 d7ac9be0 d6add808 00000000 d6ae1e30 d00a2370* *[ 8.360164] d6ae1e28 d7ac9be8 d00a6945 d7ac9be0 d69db010 d7462d80 d6ae1e4c d00a2cf8* *[ 8.360164] d79c2b80 d79c2b80 00000000 d6ae1ebc d7462d80 d6ae1eb0 d00ae159 d6ae1e64* *[ 8.360164] Call Trace:* *[ 8.360164] [<d00a2370>] do_dentry_open+0x197/0x216* *[ 8.360164] [<d00a6945>] ? cdev_put+0x1a/0x1a* *[ 8.360164] [<d00a2cf8>] vfs_open+0x45/0x4e* *[ 8.360164] [<d00ae159>] path_openat+0x822/0x970* *[ 8.360164] [<d007a468>] ? __alloc_pages_nodemask+0x11c/0x770* *[ 8.360164] [<d00ae2d8>] do_filp_open+0x31/0x77* *[ 8.360164] [<d00b6293>] ? __alloc_fd+0xbb/0xfe* *[ 8.360164] [<d00a2e56>] do_sys_open+0x54/0xc7* *[ 8.360164] [<d00a2ee1>] SyS_open+0x18/0x1a* *[ 8.360164] [<d0000ee1>] do_fast_syscall_32+0x7a/0xb8* *[ 8.360164] [<d047831f>] sysenter_past_esp+0x40/0x6a* *[ 8.360164] Code: 11 89 f0 e8 e1 fa ff ff 83 f8 01 19 db 31 d2 83 e3 fa 89 d0 e8 4d ff ff ff 85 db 75 59 8b 46 28 85 c0 75 0c* *[ 8.360164] EIP: [<d00a69f0>] chrdev_open+0xab/0x100 SS:ESP 0068:d6ae1df8* *[ 8.360164] CR2: 00000000d881f2c0* *[ 8.360164] ---[ end trace 46873a57a343e435 ]---* *[ 8.376285] string_reverse (691) used greatest stack depth: 6496 bytes left* *Killed* which seems like the program is trying to access memory that it is not supposed to. If I follow the example from wiki (here https://wiki.sel4. systems/CAmkESVM#Cross_VM_Connectors ) I get the same error, but triggered by `print_client` program. Have you seen a problem like this before? How do I correctly load the kernel module? Regards Michal

2 5

Using linux-tk1-debian on camkes-arm-vm
by Mike Clark 05 Jun '17

05 Jun '17

I have seL4 running on a TK1 using linux-tk1-initrd. I'd like to get the linux-tk1-debian version running to load the userspace off of the emmc drive of the TK1. FWIW, I did flash the TK1 to the latest verison, R21.5. The default DTS has root=/dev/mmcblk0p2 in the bootargs. When booting with this, I get a kernel panic. I also tried changing that to root=/dev/mmcblk0p1 (since that partition was the larger one on the emmc). It also gives a kernel panic, albeit a different message. With mmcblk0p1, the message I get is: [ 10.092841] EXT2-fs (mmcblk0p1): error: couldn't mount because of unsupported optional features (240) [ 10.102749] EXT4-fs (mmcblk0p1): couldn't mount as ext3 due to feature incompatibilities [ 10.137427] EXT4-fs (mmcblk0p1): mounted filesystem with ordered data mode. Opts: (null) [ 10.145696] VFS: Mounted root (ext4 filesystem) on device 179:1. [ 10.162679] devtmpfs: mounted [ 10.165845] Freeing unused kernel memory: 252K (c0aa9000 - c0ae8000) [ 10.224352] Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 [ 10.224352] [ 10.233480] CPU: 0 PID: 1 Comm: init Tainted: G W 4.3.0-rc5 #1 [ 10.240429] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree) [ 10.246713] [<c0015d30>] (unwind_backtrace) from [<c0012b74>] (show_stack+0x10/0x14) [ 10.254457] [<c0012b74>] (show_stack) from [<c009247c>] (panic+0xa0/0x214) [ 10.261330] [<c009247c>] (panic) from [<c002566c>] (complete_and_exit+0x0/0x1c) [ 10.268627] [<c002566c>] (complete_and_exit) from [<00000000>] ( (null)) [ 10.275408] ---[ end Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 With mmcblk0p2, the message I get is: [ 10.095124] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.102907] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.111127] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.118994] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.126711] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.134472] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.142167] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.149983] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.159891] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.167669] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.175842] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.183743] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.191391] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.199146] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.206813] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.214653] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.222551] Kernel panic - not syncing: VFS: Unable to mount root fs on unknown-block(179,2) [ 10.230976] CPU: 0 PID: 1 Comm: swapper Tainted: G W 4.3.0-rc5 #1 [ 10.238184] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree) [ 10.244462] [<c0015d30>] (unwind_backtrace) from [<c0012b74>] (show_stack+0x10/0x14) [ 10.252205] [<c0012b74>] (show_stack) from [<c009247c>] (panic+0xa0/0x214) [ 10.259079] [<c009247c>] (panic) from [<c0aaa238>] (mount_block_root+0x21c/0x230) [ 10.266554] [<c0aaa238>] (mount_block_root) from [<c0aaa368>] (mount_root+0x11c/0x124) [ 10.274459] [<c0aaa368>] (mount_root) from [<c0aaa4bc>] (prepare_namespace+0x14c/0x194) [ 10.282451] [<c0aaa4bc>] (prepare_namespace) from [<c0aa9dec>] (kernel_init_freeable+0x1c0/0x1d0) [ 10.291315] [<c0aa9dec>] (kernel_init_freeable) from [<c07c4b20>] (kernel_init+0x8/0xe8) [ 10.299397] [<c07c4b20>] (kernel_init) from [<c000f4d8>] (ret_from_fork+0x14/0x3c) [ 10.306959] ---[ end Kernel panic - not syncing: VFS: Unable to mount root fs on unknown-block(179,2) Is there a guide for how to setup the emmc on the TK1 to boot using linux-tk1-debian? Will an older version of the TK1 image from Nvidia work or do I need to do a custom debian install (like this https://wiki.debian.org/InstallingDebianOn/NVIDIA/Jetson-TK1)?

2 3