- Devel - lists.sel4.systems

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