- Devel - lists.sel4.systems

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