- Devel - lists.sel4.systems

New to seL4
by Andrew Mine 21 Aug '16

21 Aug '16

Hi I have just started looking at seL4 and I was wondering where can I find some documentation explaining the features and difference between seL4 and other kernels. I have gone through the manual and tutorial documents but nothing majorly explains how seL4 is different and its features. Any guidance towards any documentation will be helpful. Thanks Andrew

2 1

next seL4 developers day on Sep 6?
by Gerwin.Klein＠data61.csiro.au 16 Aug '16

16 Aug '16

We’re contemplating running a seL4 developers day in conjunction with the DARPA HACMS PI meeting in Pittsburgh on Tue, Sep 6 2016. If you would be interested in attending, please drop me a short email by Thursday night of your local time zone. If enough people register interest we will try to organise one. Cheers, Gerwin -- Prof Gerwin Klein, Research Group Leader, Trustworthy Systems DATA61 | CSIRO gerwin.klein(a)data61.csiro.au T +61 2 8306 0578 http://data61.csiro.au NICTA and CSIRO’s Digital Productivity business unit have joined forces to create the digital powerhouse Data61

1 0

Interrupt in seL4
by Norrathep Rattanavipanon 14 Aug '16

14 Aug '16

I have a few questions about how interrupts work in seL4. 1) Is it possible to enable/disable interrupt (i.e. __enable_irq or __disable_irq for ARM) in the userspace code of sel4? We want to make sure that the execution of the code in the initial process does not get interrupt. 2) My understanding is that the scheduling mechanism in seL4 is priority-based first and round-robin if two processes/threads have the same priority. Assume process A is the initial process spawned by kernel. 2.0) is my understanding about sel4 scheduling correct? 2.1) Is the initial process guaranteed to have the maximum priority in seL4? 2.2) If another process, say process B, is created by process A with lower priority. Is it possible for process B to interrupt process A and execute code in B instead while A is executing? Thanks, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

4 6

up-to-date formal verification
by Horace Blanc 09 Aug '16

09 Aug '16

Hi, I would like to know if the verification of the seL4 is up-to-date with the newest version of the sel4 microkernel (3.2.0). If so, how do I access it? When I run make ASpec in l4v, I get a pdf with the Abstract Formal Specification in version 1.3. Does it refer to the seL4 microkernel version 1.3 or has the Abstract Formal Specification its own versions? Also, what is the best way to explore this specification in Isabelle/jedit? thanks in advance Horace Blanc

2 1

on Zynq
by Neelesh Vemula 08 Aug '16

08 Aug '16

Hi all, I am completely new with seL4, embedded systems as well as the fpga world. I am working on installing seL4 on Zynq fpga and use it. I have successfully able to boot up a "hello world" application using uboot(sd card bootup) on the zynq device. However, I have no clue as in how to setup communication between the sel4 logic and the PL(fpga fabric). If I am correct some sort of device driver has to be written or is there anything that is inbuilt or someone else who has worked on a similar project. Any guidance in this regard will be utmost helpful. Thanks a ton! Neelesh Vemula

2 1

capDL configuration file
by Norrathep Rattanavipanon 03 Aug '16

03 Aug '16

So I was reading capDL paper and it mentions about having a human-readable XML file for configuration of the initial thread which allows the system initialize into a know state. I assume this is not specific to camkes. so is there any way I can see/get the XML file and the code that generates it in the regular seL4? Thanks, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

memory map/unmap performance
by Yuxin Ren 02 Aug '16

02 Aug '16

Hi all, I am curious memory mapping/unmapping performance. Are there any applications that stress the memory mapping and unmapping utility? Thanks a lot! Yuxin

4 4

beaglebone ethernet support
by Julien Delange 27 Jul '16

27 Jul '16

Hello, I noticed that there is some source code to support the ethernet driver of the beaglebone black. I look especially in projects/seL4_libs/libsel4platsupport/src/plat/am335x/cpsw_beaglebone.c According to https://github.com/seL4/seL4_libs/blob/master/libsel4platsupport/src/plat/a… the file has been introduced by NICTA - I am wondering if there is any existing example/support for it. In a nutshell, I am trying to use the ethernet driver. I started to integrate the startcode from TI on a camkes application before discovering this code. So, is there any sample application to use it? It is supported/working? Thanks for any help, Julien.

1 0

sel4 on Hikey board
by rahul mahadev 26 Jul '16

26 Jul '16

Hi , I'm trying to run sel4 on a hikey board, I'm following this wiki https://wiki.sel4.systems/Hardware/HiKey . I'm having issues as the link to the linaro-edk2 patch does not work(asks for some auth) , can someone provide another link or direct me . Thank you

2 1

Image lies outside of usable physical memory
by Alexander Boettcher 22 Jul '16

22 Jul '16

Hi, I want to boot seL4 (x86) 3.2.0 on a native machine (Lenovo X201) and I get a message like: End of loaded userland image lies outside of usable physical memory seL4 called fail at sel4/src/arch/x86/kernel/boot_sys.c: in function boot_sys, saying "boot_sys failed for some reason :( (Full log below attached) It seems that our used bootloader put the image to high in physical memory for seL4 (the other x86 kernels we use don't complain so far). Is this right that only memory below PPTR_TOP (0x1fc00000 on x86 3.2.0) can be used for the initial boot modules? Can this be changed or should we not try to touch this define (it seems to be derived from various other defines). Is there maybe a description about the required physical memory layout of the kernel and why it has to be as it is? Just in order to understand better the constraints we probably have to apply to our bootloader ;-) Thanks in advance, Alex. Parsing GRUB physical memory map Physical Memory Region from 0 size 89000 type 1 Physical Memory Region from 89000 size 17000 type 2 Physical Memory Region from d2000 size 2000 type 2 Physical Memory Region from dc000 size 24000 type 2 Physical Memory Region from 100000 size bb17c000 type 1 Adding physical memory region 0x100000-0x1fc00000 Physical Memory Region from bb27c000 size 6000 type 2 Physical Memory Region from bb282000 size dd000 type 1 Physical Memory Region from bb35f000 size 12000 type 2 Physical Memory Region from bb371000 size 81000 type 4 Physical Memory Region from bb3f2000 size 1d000 type 2 Physical Memory Region from bb40f000 size 60000 type 1 Physical Memory Region from bb46f000 size 1f9000 type 2 Physical Memory Region from bb668000 size 80000 type 4 Physical Memory Region from bb6e8000 size 27000 type 2 Physical Memory Region from bb70f000 size 8000 type 1 Physical Memory Region from bb717000 size 8000 type 2 Physical Memory Region from bb71f000 size 4c000 type 1 Physical Memory Region from bb76b000 size c000 type 4 Physical Memory Region from bb777000 size 3000 type 3 Physical Memory Region from bb77a000 size 7000 type 4 Physical Memory Region from bb781000 size 1000 type 3 Physical Memory Region from bb782000 size 9000 type 4 Physical Memory Region from bb78b000 size 1000 type 3 Physical Memory Region from bb78c000 size 13000 type 4 Physical Memory Region from bb79f000 size 60000 type 3 Physical Memory Region from bb7ff000 size 1000 type 1 Physical Memory Region from bb800000 size 800000 type 2 Physical Memory Region from bc000000 size 4000000 type 2 Physical Memory Region from e0000000 size 10000000 type 2 Physical Memory Region from feaff000 size 1000 type 2 Physical Memory Region from fec00000 size 10000 type 2 Physical Memory Region from fed00000 size 0 type 2 Physical Memory Region from fed1c000 size 4000 type 2 Physical Memory Region from fed20000 size 70000 type 2 Physical Memory Region from fee00000 size 1000 type 2 Physical Memory Region from ff000000 size 1000000 type 2 Physical Memory Region from 0 size 38000000 type 1 Kernel loaded to: start=0x100000 end=0x147000 size=0x47000 entry=0x10003e ACPI: RSDP paddr=0xf68e0 ACPI: RSDP vaddr=0xdfcf68e0 ACPI: RSDT paddr=0xbb7f07a2 ACPI: RSDT vaddr=0xdfff07a2 ACPI: DMAR paddr=0xbb781000 ACPI: DMAR vaddr=0xdff81000 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=0x2 fun=0x0 ACPI: 3 IOMMUs detected ACPI: MADT paddr=0xbb7feb45 ACPI: MADT vaddr=0xdfffeb45 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=0x4 ACPI: MADT_APIC apic_id=0x5 ACPI: MADT_IOAPIC ioapic_id=1 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: 4 CPU(s) detected Detected 4 CPUs. Only just 1 Detected 1 boot module(s): module #0: start=0x7fc7a000 end=0x7ffff338 size=0x385338 name='/image.elf' ELF-loading userland images from boot modules: size=0x385000 v_entry=0x2000000 v_start=0x2000000 v_end=0x2385000 p_start=0x80000000 p_end=0x80385000

2 1

3.1.0 to 3.2.0 (x86) upgrade issue
by Alexander Boettcher 22 Jul '16

22 Jul '16

Hello, after upgrading the seL4 kernel (x86) from 3.1.0 to 3.2.0 we get for the very first invocation of seL4_X86_Page_Map an errorcode of *3* (seL4_IllegalOperation). We bisected the commits between 3.1.0 and 3.2.0 and [0] is the first bad commit for us. If we use the 3.2.0 release with [0] reverted on top than everything works as before - so no changes to Genode/seL4 as used for the 3.1.0 kernel are necessary. It's a know issue, or maybe something changed which must be adjusted in userland/roottask ? Thanks, Alex. [0] https://github.com/seL4/seL4/commit/c8819792d76ae5aecd89bcff656ca561e62959a5

2 2

Re: [seL4] [sel4utils question] stack size of the second process
by Kofidoku.Atuah＠data61.csiro.au 21 Jul '16

21 Jul '16

Hi, Our malloc currently uses mmap() for large allocations (and therefore the matching munmap() for freeing those large allocations). See https://github.com/seL4/musllibc/blob/sel4/src/malloc/malloc.c#L352. So while the mmap() call is implemented, the munmap() call is not, and this is why you're seeing this issue with "syscall 91" not being successful: https://github.com/seL4/musllibc/blob/sel4/arch/i386/bits/syscall.h#L92 https://github.com/seL4/musllibc/blob/sel4/arch/arm/bits/syscall.h#L67 ? Usually you allocate such a big chunk of memory for private use and management, so free() probably isn't a mission critical thing here (for the tutorials), unless there are factors I can't see -- let me know if this was helpful -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61

1 0

[sel4utils question] stack size of the second process
by Norrathep Rattanavipanon 20 Jul '16

20 Jul '16

Hi, So I followed hello-4 example. I can create a static array inside a second process (hello-4-app) and the second process works fine. However, when I try to increase the size of an array to 80,000 bytes, the second process wont start. I tried to increase ALLOCATOR_VIRTUAL_POOL_SIZE but it still does not work. Any help would be appreciated. Thanks, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

1 1

Re: [seL4] [sel4utils question] stack size of the second process
by Kofidoku.Atuah＠data61.csiro.au 20 Jul '16

20 Jul '16

Hi, Thanks for popping by! The answer to the question in the subject line of your email (stack size of processes spawned by sel4utils_configure_process()) is that sel4utils_configure_process() calls sel4utils_configure_thread(), which allocates the stack using vspace_new_pages(), found here: (https://github.com/seL4/seL4_libs/blob/master/libsel4vspace/include/vspace/…) The stack size is determined by CONFIG_SEL4UTILS_STACK_SIZE, which can be set in your `make menuconfig` settings. Try: `make menuconfig` -> select "seL4 Libraries" -> "libsel4utils" and change the stack size as desired. That said, > However, when I try to increase the size of an array to 80,000 bytes, the second process wont start. I tried to increase ALLOCATOR_VIRTUAL_POOL_SIZE but it still does not work. Sorry, I'll need to know a bit more about what's going on here: could you post some more detailed output, or maybe a diff, so I can try to aid you? --Yours truly, Kofi

1 0

Cortex-M port?
by Stefan Wallentowitz 18 Jul '16

18 Jul '16

Hi, I was wondering if anyone ever started a port to a v7-M platform? Cheers, Stefan

2 1

3.2.0 release issues?
by Jeff Waugh 18 Jul '16

18 Jul '16

Hey there, I noticed the wiki "latest" links now point to 3.2.0. I haven't seen an announcement for 3.2.0 yet, so perhaps this is all a matter of staging, but the current sel4test manifest points to 3.2.x-compatible tags that don't exist in most of the repos. Just thought I'd mention it as I imagine it's the primary way people acquire new releases. Thanks, Jeff

2 4

RELEASE: seL4 3.2.0 release
by Parthasarathi Susarla 18 Jul '16

18 Jul '16

We are pleased to announce the release of 3.2.0 of seL4. This release contains the following changes: * ARM Hypervisor support. * ARM Jetson-TK1: Cleanup. * Benchmarking now supports tracking of syscalls. * Support for XSAVE feature set for x86 CPUs. * Simplified ARM platform selection during configuration. = ABI Changes = * seL4_BootInfo has a new entry for IOSpace caps for ARM SMMU. The release tarballs can be directly downloaded from: https://github.com/seL4/seL4/archive/3.2.0.tar.gz 7210ecc65f0f8a04490605e92f7b89b4 3.2.0.tar.gz The manual for this release can be downloaded here: http://sel4.systems/Info/Docs/seL4-manual-3.2.0.pdf Please let us know of any issues that you run into by creating an issue in the issue tracker: https://github.com/seL4/seL4/issues -- Partha Susarla <parthasarathi.susarla(a)nicta.com.au> ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

verification requirements
by Gergely Buday 13 Jul '16

13 Jul '16

Hi, what are the requirements for running the whole sel4 verification proof? Is 32G RAM and 20G disk space enough? How about the processor needs? I guess what is enough in batch mode will be enough for interactive development. - Gergely

2 1

Frame buffer
by Rinat Dobrokhotov 09 Jul '16

09 Jul '16

Hello, Could you tell me if framebuffer is released for seL4? -- Best Regards, Rinat Dobrokhotov

6 7

[sel4] persistent storage / file system
by rahul mahadev 06 Jul '16

06 Jul '16

Hi, I wanted to know if persistent storage/ file system have been tried on sel4 before ,if so can I have more details on it. Regards , Rahul S Mahadev

5 5

Capabilities of binary images
by Norrathep Rattanavipanon 06 Jul '16

06 Jul '16

Hi, I need to access the user image from a user application for verifying that the binary is installed correctly. So I found in bootinfo.h that it contains userImageFrames and its supposed to be the one I'm looking for but it gave me an error when I map the frames via vspace_map_pages(vspace, info->userImageFrames.start, ...) at the root task. The error is : ERROR:sel4utils_map_page_pd:223: Error mapping pages, bailing: 2 What am I doing wrong here? Best, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 2

Get real time clock data (and timer) from I.MX6
by Norrathep Rattanavipanon 30 Jun '16

30 Jun '16

Hi, I was wondering if there's any real time clock implementation for I.MX6 in sel4. And if there isnt any, what would be the best way to use a timer in sel4 (since I saw many implementations of those)? through sel4platsupport_get_default_timer? Best, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 5

ARM Hypervisor extensions in master
by Adrian Danis 28 Jun '16

28 Jun '16

The ARM hypervisor extensions are now supported in the master seL4 kernel. This support has existed on a public development branch (arm_hyp) for some time, but this marks the beginning of proper support and a verification target. What is done: * Hypervisor extensions supported on odroid-xu and Jetson TK1 platforms * SystemMMU supported on Jetson TK1 platform Limitations: * Currently any usage of hyp extensions or SystemMMU is *not* verified * SystemMMU contains work around currently for the VMM to map in large amounts of memory (fix for this relies on a kernel change currently being verified) You can use the manifest https://github.com/seL4proj/camkes-arm-vm-manifest to get the project https://github.com/seL4proj/camkes-arm-vm and then use one of the two default configs for the TK1 and odroid-xu platforms. Adrian ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

camkes-VM with QEMU and virutal PCI device
by Samuel Weiser 28 Jun '16

28 Jun '16

Hi again, I'm playing around with camkes-vm in QEMU+KVM. I want to add a virtual PCI device to Linux, which is running as vm0 on top of seL4. However, I got stuck with some errors during system boot. My setup is as follows: QEMU is configured to share a 1MB memory region between the host and the QEMU guest (seL4). Here's what QEMU sets up: (qemu): info mtree ... 00000000fe000000-00000000fe0fffff (prio 1, RW): ivshmem-bar2-container 00000000fe000000-00000000fe0fffff (prio 0, RW): ivshmem.bar2 00000000febf1000-00000000febf10ff (prio 1, RW): ivshmem-mmio ... (qemu): info pci ... Bus 0, device 4, function 0: RAM controller: PCI device 1af4:1110 IRQ 11. BAR0: 32 bit memory at 0xfebf1000 [0xfebf10ff]. BAR2: 64 bit prefetchable memory at 0xfe000000 [0xfe0fffff]. id "" ... I adapted a previously working configuration (optiplex9020.camkes) accordingly with what I thought should be correct. Especially, I added vm0_config.pci_devices_iospace and vm0_config.pci_devices as well as the PCI irq. Here's the configuration: configuration { VM_CONFIGURATION_DEF() VM_PER_VM_CONFIG_DEF(0, 2) vm0.simple_untyped24_pool = 12; vm0.heap_size = 0; vm0.guest_ram_mb = 1536; vm0.kernel_cmdline = VM_GUEST_CMDLINE; vm0.kernel_image = C162_KERNEL_IMAGE; vm0.kernel_relocs = C162_KERNEL_IMAGE; vm0.initrd_image = C162_ROOTFS; vm0.iospace_domain = 0x00; vm0_config.ram = [ [ 0x20800000, 23 ], [ 0x21000000, 24 ], [ 0x22000000, 25 ], [ 0x24000000, 26], [ 0x28000000, 27], [0x30000000, 28], [0x40000000, 29] , [0x60000000, 30], [0xa0000000, 28]]; vm0_config.ioports = [ {"start":0x2f8, "end":0x2ff, "pci_device":0, "name":"COM2 Serial Port"}, {"start":0x2e8, "end":0x2ef, "pci_device":0, "name":"COM4 Serial Port"} ]; vm0_config.irqs = [ {"name":"Serial", "source":3, "level_trig":0, "active_low":0, "dest":3}, {"name":"PCI", "source":11, "level_trig":1, "active_low":1, "dest":11} ]; vm0_config.pci_devices_iospace = 1; vm0_config.pci_devices = [ {"name":"PCI", "bus":0, "dev":0x04, "fun":0, "irq":"PCI", "memory":[ {"paddr":0xfe000000, "size":0x100000, "page_bits":12}, ], }, ]; } However, after creating the MMIO frames and doing some other stuff, the boot process fails, as shown below. The error also occurs if I change or completely remove just the "memory" definition of my PCI device. I also tried different values for "iospace_domain" (QEMU should use 0 as default PCI domain). Thanks in advance for any hints and ideas! Best, Sammey Starting Loader... Parsing bootinfo... 1041793 free cap slots, from 6783 to 1048576 Untyped memory (24) 0x0000000000100000 - 0x0000000000108000 0x0000000000108000 - 0x0000000000109000 0x0000000003000000 - 0x0000000004000000 0x0000000004000000 - 0x0000000008000000 0x0000000008000000 - 0x0000000010000000 0x0000000010000000 - 0x0000000018000000 0x0000000018000000 - 0x000000001c000000 0x000000001c000000 - 0x000000001e000000 0x000000001e000000 - 0x000000001f000000 0x000000001f000000 - 0x000000001f800000 0x000000001f800000 - 0x000000001fc00000 0x0000000001b6b000 - 0x0000000001b6c000 0x0000000001b6c000 - 0x0000000001b70000 0x0000000001b70000 - 0x0000000001b80000 0x0000000001b80000 - 0x0000000001c00000 0x0000000001c00000 - 0x0000000001e00000 0x0000000001e00000 - 0x0000000001f00000 0x0000000001f00000 - 0x0000000001f80000 0x0000000001f80000 - 0x0000000001fc0000 0x0000000001fc0000 - 0x0000000001fe0000 0x0000000001fe0000 - 0x0000000001ff0000 0x0000000001ff0000 - 0x0000000001ff2000 0x0000000001ff2000 - 0x0000000001ff3000 0x0000000001ff3000 - 0x0000000001ff3800 Loader is running in domain 0 Device untyped memory (30) 0x0000000000001000 - 0x0000000000002000 0x0000000000002000 - 0x0000000000004000 0x0000000000004000 - 0x0000000000008000 0x0000000000008000 - 0x0000000000010000 0x0000000000010000 - 0x0000000000020000 0x0000000000020000 - 0x0000000000040000 0x0000000000040000 - 0x0000000000080000 0x0000000000080000 - 0x0000000000100000 0x000000001fc00000 - 0x0000000020000000 0x0000000020001000 - 0x0000000020002000 0x0000000020002000 - 0x0000000020004000 0x0000000020004000 - 0x0000000020008000 0x0000000020008000 - 0x0000000020010000 0x0000000020010000 - 0x0000000020020000 0x0000000020020000 - 0x0000000020040000 0x0000000020040000 - 0x0000000020080000 0x0000000020080000 - 0x0000000020100000 0x0000000020100000 - 0x0000000020200000 0x0000000020200000 - 0x0000000020400000 0x0000000020400000 - 0x0000000020800000 0x0000000020800000 - 0x0000000021000000 0x0000000021000000 - 0x0000000022000000 0x0000000022000000 - 0x0000000024000000 0x0000000024000000 - 0x0000000028000000 0x0000000028000000 - 0x0000000030000000 0x0000000030000000 - 0x0000000040000000 0x0000000040000000 - 0x0000000060000000 0x0000000060000000 - 0x00000000a0000000 0x00000000a0000000 - 0x00000000e0000000 0x00000000e0000000 - 0x0000000000000000 Sorting untypeds... Untyped 0 (cptr=1a39) is of size 15. Placing in slot 17... Untyped 1 (cptr=1a3a) is of size 12. Placing in slot 20... Untyped 2 (cptr=1a3b) is of size 24. Placing in slot 5... Untyped 3 (cptr=1a3c) is of size 26. Placing in slot 2... Untyped 4 (cptr=1a3d) is of size 27. Placing in slot 0... Untyped 5 (cptr=1a3e) is of size 27. Placing in slot 1... Untyped 6 (cptr=1a3f) is of size 26. Placing in slot 3... Untyped 7 (cptr=1a40) is of size 25. Placing in slot 4... Untyped 8 (cptr=1a41) is of size 24. Placing in slot 6... Untyped 9 (cptr=1a42) is of size 23. Placing in slot 7... Untyped 10 (cptr=1a43) is of size 22. Placing in slot 8... Untyped 11 (cptr=1a44) is of size 12. Placing in slot 21... Untyped 12 (cptr=1a45) is of size 14. Placing in slot 18... Untyped 13 (cptr=1a46) is of size 16. Placing in slot 15... Untyped 14 (cptr=1a47) is of size 19. Placing in slot 11... Untyped 15 (cptr=1a48) is of size 21. Placing in slot 9... Untyped 16 (cptr=1a49) is of size 20. Placing in slot 10... Untyped 17 (cptr=1a4a) is of size 19. Placing in slot 12... Untyped 18 (cptr=1a4b) is of size 18. Placing in slot 13... Untyped 19 (cptr=1a4c) is of size 17. Placing in slot 14... Untyped 20 (cptr=1a4d) is of size 16. Placing in slot 16... Untyped 21 (cptr=1a4e) is of size 13. Placing in slot 19... Untyped 22 (cptr=1a4f) is of size 12. Placing in slot 22... Untyped 23 (cptr=1a50) is of size 11. Placing in slot 23... Creating objects... ... Creating object conn1_mmio_frame_4261412864 in slot 6808, from untyped 1a3c... device frame, paddr = 0xfe000000, size = 12 bits Creating object conn1_mmio_frame_4261416960 in slot 6809, from untyped 1a3c... device frame, paddr = 0xfe001000, size = 12 bits Creating object conn1_mmio_frame_4261421056 in slot 6810, from untyped 1a3c... device frame, paddr = 0xfe002000, size = 12 bits ... Creating object vm_vm0_pre_init_ep in slot 10275, from untyped 1a3c... Creating object conn1_iospace_32 in slot 10276, from untyped 1a3c... <=== This is ignored! Creating object conn4_iport_760_767 in slot 10276, from untyped 1a3c... ... Populating slot 21 with cap to conn1_iospace_32... minting (with badge/guard 0x20)... <<seL4 [decodeCNodeInvocation/107 T0xe1ff3900 "rootserver" @804a911]: CNode Copy/Mint/Move/Mutate: Source slot invalid or empty.>> capDL-loader :: << Error: init_cnode_slot:1689: seL4_FailedLookup >>

2 1

Autocorres Error.
by Dan DaCosta 24 Jun '16

24 Jun '16

seL4 Developers: I apologize in advance if this is not the correct place for this email. I am experimenting with Autocorres as an intern at Rockwell Collin's Advanced Technology Center in Minnesota. My latest experiment is in building a small verified library for manipulation and analysis of adjacency lists. My initial work towards this end generated the following error: exception CTERM raised (line 948 of "~/development/rockwellcollins/verification/l4v/tools/autocorres/utils.ML"): autocorres: Internal var uu_::"int" is exposed. Please notify the AutoCorres maintainers of this failure. In the meantime, use "autocorres [keep_going]" to ignore the failure. I am using the latest version of Autocorres and Isabelle. The c and theory file that generated this error can be found here: https://github.com/chaosape/autocorresexperiments/tree/master/graph Thanks! Dan DaCosta

3 3

Resolving issue using camkes-vm with qemu
by Samuel Weiser 20 Jun '16

20 Jun '16

Hi, I just want to share some information which I needed to run camkes-vm with qemu, especially addressing one issue which prevented the guest vm to boot. I basically follow the recommendations of Adrian in [1] and only focus on the simple case without vt-d. 1. use the 'optiplex9020_onevm' configuration as it basically just specifies physical RAM. 2. enable nested KVM [2,3] 3. run QEMU with enough RAM: qemu-system-i386 -nographic \ -m 3GB \ -enable-kvm \ -cpu host \ -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99 Following the above steps gives you a booting camkes vmm, however it fails to eventually activate Intel vt-x, needed to run the guest vm. The reason for that is that the seL4 kernel requires the IA32_FEATURE_CONTROL MSR to have VMXON enabled (bit 2) and locked (bit 0) (i.e. a value of 5). Normally, it's the job of the BIOS to do so, however I couldn't find an appropriate QEMU BIOS ROM which does so. The quick workaround is to enable VMXON within the seL4 kernel itself. The corresponding diff is attached. With this minor change, the recompiled kernel works like a charm. PS: One could consider making a separate option in Kconfig for that purpose. Best, Sammey [1] https://sel4.systems/pipermail/devel/2016-March/000717.html [2] http://www.rdoxenham.com/?p=275 [3] https://wiki.archlinux.org/index.php/QEMU#Enabling_KVM

2 1

Rust application support
by Kent.Mcleod＠data61.csiro.au 20 Jun '16

20 Jun '16

Using rust (https://www.rust-lang.org) in user applications on top of seL4 with existing C libaries and apps now has limited support. See here for more information: https://wiki.sel4.systems/Rust What you can do: + Build system support for using a rust cargo project as a library or app on seL4 + Use most core libraries (core, alloc, collections, rustc_unicode, and a limited std) + Use rust dependencies from crates.io on seL4 + Use rust to implement camkes components + Using rust's FFI support it is possible to call rust from C and C from rust. Two sample apps are located here: https://github.com/SEL4PROJ/rust-camkes-samples Instructions for building and running are on the wiki page. Has been tested on x86 i386 and arm kzm both in qemu and hardware. Caveats: + Rust's libstd functionality is limited by which muslc syscalls are supported on seL4. + Rust's libstd requires muslc thread local storage support which is not currently available on seL4. We currently use a muslc branch called rust that uses a global TLS struct. Kent McLeod Kernel engineer / Thesis Student DATA61 | CSIRO

1 0

WIll seL4 support any Unikernel
by XilongPei 16 Jun '16

16 Jun '16

Hi, According to wikipedia.org, Unikernels are specialised, single address space machine images constructed by using library operating systems. A developer selects, from a modular stack, the minimal set of libraries which correspond to the OS constructs required for their application to run. These libraries are then compiled with the application and configuration code to build sealed, fixed-purpose images (unikernels) which run directly on a hypervisor or hardware without an intervening OS such as Linux or Windows. Will seL4 support any unikernel, such as Drawbridge or MirageOS, in the future? Xilong Pei Tongji University Shanghai, China 2016/6/13

3 2

Beaglebone black/CAmkES issue
by Julien Delange 15 Jun '16

15 Jun '16

I am using the second serial interface of the beaglebone black. According to the source code (in libsel4platsupport/plat_include/am335x/sel4platsupport/plat/hw/soc_AM335x.h), the address is 0x48022000). The following line is found in the source #define SOC_UART_1_REGS (0x48022000) So, in CAmkES, I configure the hardware component that represents the serial hardware component with the following attributes: drv.mem_attributes = "0x48022000:0x1000"; The application compiles fine. However, when launching the image on the target, I have the following issue. Any idea about how to solve this? Does anybody successfully used UART1 on the beaglebone black? Or have any idea/suggestion to investigate? Thanks. Julien. Creating object conn1_frame__timer_0 in slot 728, from untyped 29b... device frame, paddr = 0x48040000, size = 12 bits Creating object conn2_frame__Cons_PingMe_0 in slot 729, from untyped 29b... device frame, paddr = 0x48022000, size = 12 bits capDL-loader :: << Error: Failed to find device frame at paddr = 0x48022000 >> Ignoring call to sys_rt_sigprocmask Ignoring call to sys_gettid sys_tkill assuming self kill

4 8

Tidying and real-time
by Jeff Waugh 15 Jun '16

15 Jun '16

This commit… https://github.com/seL4/seL4/commit/c5b6a6a58aae75129cdf5a83f861bdacddbf51d6 … is pleasing. As is the RT API. Passive servers! A seemingly viable and sensible approach to user-space scheduling! Just a quick thumbs up for recent progress. :-)

1 0

CAmkES parsing issue
by Julien Delange 10 Jun '16

10 Jun '16

Hi, I am trying to build a camked application with a UART driver. When trying to build the application, I got the following error: While rendering uart_mem.from.source: 'drv' However, the component is well define. How can I try to get more information/debug of the camkes assembly and find out what is wrong? Thanks! Note: the project can be found there: https://drive.google.com/file/d/0Bxl72qH3r6BjRGxYSXd2LUllcDQ/view?usp=shari…

3 6

camkes arm vm I/0 devices
by Josh Tuttle 08 Jun '16

08 Jun '16

Hey, We have been playing around with the busybox for tk1 that was included in the build. While trying to verify all the I/0 devices, we noticed that the Ethernet device would not come up. Looking though dmesg, it seems to load a driver but never initializes a device. Ifconfig just errors when trying to bring up eth0. Has anyone verified the I/0 devices on tk1 using this build? Not being familiar with busybox, can we follow this: http://elinux.org/Jetson/Busybox_RootFS guide to building a busybox image to include all appropriate drivers? Thanks, Josh

2 1

seL4 benchmarks available
by Anna Lyons 07 Jun '16

07 Jun '16

Hi all, I've just finished pushing the seL4 benchmarking suite out to github. Get it: * manifest: https://github.com/seL4/sel4bench-manifest * explore the applications: https://github.com/seL4/sel4bench. Cheers, -- Anna Lyons Kernel engineer / PhD Student DATA61 | CSIRO E anna.lyons(a)nicta.com.au<mailto:anna.lyons@nicta.com.au> www.data61.csiro.au<http://www.data61.csiro.au> CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

Unable to build camkes-vm
by Samuel Weiser 07 Jun '16

07 Jun '16

Hello, didn't manage to build camkes-vm. Is there any working setup available or did I make something wrong? 1.) I tried to build c162_twovm_defconfig with the "default.xml" manifest 1a.) I get compile errors regarding some definitions of seL4_X86.... It seems that seL4_libs (March 2016) are inconsistent with the kernel version (Dec 2015). Updating to a newer kernel, i.e. 3.1.0 solves this issue but creates new ones: 1b.) The bootinfo struct is too big to fit one page. I get the error: compile_assert(bi_size, sizeof(seL4_BootInfo) <= BIT(BI_FRAME_SIZE_BITS)) So I reduced the max. no of bootinfo untyped caps from 800 to 167 1c.) Error: No rule to make target 'libsel4simple-default', needed by 'libsel4platsupport-y' Since the kernel is not stable, it falls back to default but does not manage to correctly reference the default lib. First, I added the missing symlink in libs. Then, I added the default lib to the main Kconfig and the apps/c162_twovm/Kbuild. 1d.) The next error is: x86/pc99/include/vmm/guest_state.h:60:44: error: unknown type name ‘seL4_VCPUContext’ ... 2.) I also tried building with the "working.xml" manifest, which already failed to fetch the correct revisions 2a.) In the working.xml, I fixed the seL4_libs upstream to 'master' Also, the kernel revision is broken, seL4.git points to an experimental commit, which couldn't be fetched. I changed it to kernel 3.1.0. 2b.) The same error as in 1d) appears. This is where I gave up. Any hints? Thanks in advance, Sammey

2 1

VM on SeL4 for TK1
by Joshua Tuttle 06 Jun '16

06 Jun '16

Hi, I am working with Peng Xie to run the vm for tk1 code that Adrian gave out a couple of days ago, located at https://github.com/seL4proj/camkes-arm-vm-manifest. We have successfully been able to build and run on our tk1 board, but are met with a buildroot login prompt. What is the username and password, we should be using? Also, is this a para-virtualized or fully-virtualized environment? Thanks, Josh Tuttle Research Engineer Intelligent Automation, Inc. 15400 Calhoun Dr., Suite 109 Rockville, MD 20855 Ph: (301) 795-2706 jtuttle(a)i-a-i.com<mailto:jtuttle@i-a-i.com> ________________________________ 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

Latest experimental RT kernel released
by Anna Lyons 03 Jun '16

03 Jun '16

= Latest experimental RT kernel released = The RT kernel provides + periodic scheduling, + temporal isolation, + support for criticality and criticality mode changes, + temporal exceptions, .. and more. == Caveats == The RT kernel does not compile or run on all platforms, we currently support: + x86: ia32 platforms with TSC_DEADLINE mode + ARM: Sabre lite, Beagle board, and Odroid-xu (all armv7-a). The RT kernel is not verified, and as such we provide no guarantees, and there's likely still some bugs hiding in there. The other platforms require driver work at user level and in the kernel. If you are keen to get a certain platform working, contributions are welcome! == Available == + *Kernel branch* on github: https://github.com/seL4/seL4/tree/rt + *Release notes* (detailed API changes from current seL4 latest release): https://wiki.sel4.systems/seL4%201.0.0-rt-dev + *RT kernel manual* http://sel4.systems/Info/Docs/seL4-manual-1.0.0-rt-dev.pdf + *whitepaper* http://arxiv.org/abs/1606.00111 == Try it == Check out the rt branch of sel4test-manifest with repo: $ repo init -u https://github.com/seL4/sel4test-manifest.git -b rt Feedback on the API would be *extremely* valued. Enjoy! -- Anna Lyons Kernel engineer / PhD Student DATA61 | CSIRO E anna.lyons(a)nicta.com.au<mailto:anna.lyons@nicta.com.au> www.data61.csiro.au<http://www.data61.csiro.au> CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

3 3

Memory allocation & threads
by Доброхотов Ринат 03 Jun '16

03 Jun '16

Hello, I don't understand how static and virtual pool's size related to thread's available working space. I got the example app from the sel4-tutorials project with process creation (app-4). A static pool and a virtual pool are created in this app. I have done experiments with size of this pools and size of arrays in the second thread. For example I set size of virtual pool to zero, as I understand this pool need to create kernel objects. Also I define the test array size of (1 << 23)~8,3Mb. If test array is static, static pool size must be equal to ((1 << seL4_PageBits) * 100) ~0,4Mb. If test array is no static, static pool size not limited. Why is it so? -- Best Regards, Rinat Dobrokhotov

4 4

Will the codes in branch rt be merged into master
by XilongPei 01 Jun '16

01 Jun '16

Hi, I got information from https://wiki.sel4.systems/seL4%201.0.0-rt-dev , the development branch for the seL4 realtime extensions. My question is that will the codes in branch rt be merged into master, and add some build option. If a working tree always not in the master branch, it will be very difficult to be managed. Xilong Pei Tongji University 2016/6/1

2 1

RT branch questions
by Julien Delange 26 May '16

26 May '16

I am currently trying the RT branch and have some questions: 1. What emulator to use in order to try the examples? I am trying to use x86 with qemu but it seems that it does not work. I got the following trace at execution Starting node #0 APIC: unsupported platform, TSC-deadline mode is not supported seL4 called fail at /home/sel4/camkes-sc-tests/kernel/src/arch/x86/kernel/boot_sys.c:451 in function boot_sys, saying "boot_sys failed for some reason :( So, is there an emulator (for any supported platform) to try it? 2. In the RT-camkes extensions, I have the following new attributes: _period _budget _priority What is the semantics of these attributes? Any information about them? How they are supposed to be isolated from each other then? How to define the scheduling plan for the system then? Also, how these attributes apply to all thread: a thread is created for each interface of the component, so, how can we then define the priority/budget of each thread? Do these attributes apply to all the components of the thread? Thanks for any help/clarification. Julien. assembly { composition { component Client client1; component Client client2; } configuration { client1._priority = 100; client1._period = 10000; client1._budget = 7500; client2._priority = 50; client2._period = 10000; client2._budget = 7500; } }

3 6

Advice on camkes and regular seL4 for driver components
by Norrathep Rattanavipanon 26 May '16

26 May '16

Hello, I currently had codes, implemented as regular seL4, since camkes does not support some features (i.e. transferring capabilities or accessing address space outside the process), Everything is fine up to this point but now I want to create several drivers. And I found that the best and easiest way to do that is to use camkes. So is it possible to use existing regular codes in conjunction with camkes? Or would the best way be to implement drivers as regular seL4 codes? Thanks, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

building VMM on Jetson TK1 board
by PX 26 May '16

26 May '16

Hi, all we want to build the seL4-based VMM from https://github.com/smaccm/sel4arm-vmm.git on Jetson TK1 board. However, the seL4 kernel in that project does not support TK1 board. We want to use the new version seL4 version (arm_hyp) at https://github.com/seL4/seL4.git. My questions are: 1) It is feasible to do that? 2) If so, what are the correct steps to do that? 3) we try to compile these source code, but failed. We do the following modifications: A) we add TK1 source codes (i.e. TK1 folders from https://github.com/seL4/seL4.git) to the corresponding libraries in the VMM source code from https://github.com/smaccm/sel4arm-vmm.git; and B) we add relevant config definitions to the VMM code. Currently, we can successfully compile the seL4 kernel code, but have trouble to compile the VMM libraries. Do we miss something here? thanks Peng

2 1

Availability of RT branch?
by Julien Delange 24 May '16

24 May '16

Hi all, Follow-up on our recent discussions on the RT branch: is the RT branch now available? How could I get it and access the related documentation? If not available, is there any idea of when it will be available? Thanks. Julien.

1 0

Getting timer info from seL4 kernel
by Will Klieber 18 May '16

18 May '16

Hi, Is there any way of obtaining the number of elapsed timer ticks from the seL4 kernel (using ARM / BeagleBoard platform)? I know the kernel uses this information internally for the scheduler, but I couldn't find any way of accessing it from userland. Specifically, my usage scenario is as follows. Two mutually distrustful programs are running, and each wants to run an action periodically. We want to temporally isolate the two programs using seL4 time domains. In this case, interacting with the hardware timer in userland seems difficult, since we want to get the updated time whenever a new timer tick arrives, but the userland device driver for the timer can only operate in exactly one of the seL4 time domains. Please let me know if I am misunderstanding something or if there might be a better way to approach this situation. Thanks, Will

5 6

Hello. I'm Kihyun-seo in South Korea.
by 서기현 17 May '16

17 May '16

Hello, I am a student of the Hanseo University in Korea. I want to create a UAV(drone) that uses Odroid XU4 Odroid XU4's Detailed Specifications = http://www.hardkernel.com/main/products/prdt_info.php?g_code=G143452239825 I want to install seL4 on the board for the security of the drones. The board has “ubuntu-15.04-robotics-odroid-xu4-201” 32bit linux version. I have two questions. First, I understood that after installing the seL4 first, and installing the linux later after seeing the 1.jpg. However, in the “https://wiki.sel4.systems/Getting%20started”. “Setting up your machine - These instructions are for Ubuntu. They assume you already know the basics of using the command line, compilers and GNU Make.” So then, Should I install the Linux(ubuntu) first, and install the seL4 later? I wonder what is correct. and I need more detailed explanation. Second, An error occurred during install the seL4 like 2.jpg. (command = "make menuconfig" in "Build ia32" part.) I need a solution about the error. Please answer my two questions.

3 2

multi-core support
by PX 16 May '16

16 May '16

Hi, Just want to double check if the seL4 under link https://github.com/seL4/sel4test supports multi-core? If so, the multi-core support is configured by default? If the sel4 does not support multi core, where can we get the experimental version supporting multi core? thanks Peng

2 1

Trusted Execution Environment on seL4
by rahul mahadev 11 May '16

11 May '16

Hi, I am Rahul Mahadev, I'm currently working on a Google Summer Of Code project with the organization lowRISC. My project is to implement a Trusted Execution Environment for the RISC-V platform. Last year's gsoc had a port of sel4 for RISC-V platform by Hesham Almatery. I plan on using seL4 for the port by either of the two methods. 1. paravirtualize OPTEE(Linaro's TEE) on top of seL4 2. implement an API similar to OPTEE for seL4 I have written a blog post explaining this, I wanted your opinion + ideas regarding this. link: http://mahadevrahul.blogspot.in/2016/05/gsoc-2016-implementing-trusted.html Thank You, Rahul Mahadev

2 1

Is the L4-embedded microkernel here means seL4
by XilongPei 20 Apr '16

20 Apr '16

Dear all, The web page http://ssrg.nicta.com.au/about/#achievements says: !$ All recent Apple iOS devices ship with a <http://www.apple.com/business/docs/iOS_Security_Guide.pdf> security processor controlled by a fork of our L4-embedded microkernel; I wonder whether the L4-embedded microkernel means seL4. thanks Xilong Pei Tongji University 2016/4/14

4 5

Problem porting sel4 into XU4
by Norrathep Rattanavipanon 19 Apr '16

19 Apr '16

Hi, I'm trying to port sel4 into ODROID-XU4 by following the wiki ( https://wiki.sel4.systems/Hardware/odriod-XU) So far I can successfully enable HYP mode as indicated by [ 0.198398] [c0] CPU: All CPU(s) started in HYP mode. [ 0.198433] [c0] CPU: Virtualization extensions available. as well as generate sel4test-driver-image-arm-exynos5 image. However, we cant do fastboot in XU4 since it doesnt have usb otg. Thus, I followed booting from sd card from https://wiki.sel4.systems/Hardware/General-ARM and copied the image into the first partition of sd card and do the following: Exynos5422 # fatload mmc 0 0x48000000 sel4test-driver-image-arm-exynos5 Exynos5422 # bootelf 0x48000000 and here's the output: ## Starting application at 0x41000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A7 r0p3 Switching CPU... ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p3 paddr=[41000000..4126401f] ELF-loading image 'kernel' paddr=[40000000..4002dfff] vaddr=[e0000000..e002dfff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[4002e000..40388fff] vaddr=[8000..362fff] virt_entry=13868 Enabling hypervisor MMU and paging Enabling MMU and paging Jumping to kernel-image entry point... �⧹I�AIq9Fy6 1)�a&I99)�6� Yq��摦P�^б��F��^/A�yyyyyyyyy�Y �)aay��XY�ǡyQ)�q��O�a@ Ia)!Fyaay �)��XY��.6I�)&FvF�6fF��VƑ�y��P�)aay��XY�ǡyQ)�q��O�a@ Ia Is it expected? or am I doing something wrong? Any help would be appreciated. Best, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 6

building VMM on multi-core seL4
by PX 14 Apr '16

14 Apr '16

Dear all, I have some questions about building VMM on top of seL4. I know there is a sel4-based VMM on github (https://github.com/smaccm/sel4arm-vmm-manifest) Gernot also told me that this version of VMM does not support multi core. My questions are: 1) Can this single core version of VMM be run on top of multi-core sel4 just using one core without modification? 2) If not, what supports are missed in the multi-core version of sel4? I assume single-core version applications should be compatible with multi-core micro kernel. 3) If my assumption is wrong, what do we (as VMM developer) need to add to the VMM code to make it workable on the multi-core seL4? thanks Peng

2 1

Re: [seL4] [seL4/seL4] Real performance comparisons (#21)
by Gernot Heiser 11 Apr '16

11 Apr '16

On 11 Apr 2016, at 8:09 , fresheneesz <notifications(a)github.com<mailto:notifications@github.com>> wrote: I imagine this isn't the right place for this, but i can't find a better one. The correct one is this (devel(a)sel4.systems<mailto:devel@sel4.systems>) I see the performance comparisons at http://l4hq.org/docs/performance.php are run on all different processors. In its current form, the performance numbers here are completely useless. It would be very informative to have real performance benchmarks where the exact same processor is used for every OS in comparison. Otherwise, what am I supposed to do with those number? You’re right that comparisons across different processors are of limited power, but they aren’t useless either, especially when expressed in cycles (and ideally coupled with an understanding of the underlying hardware, eg the insane pipeline depth and speculation of the Pentium 4). However, given that these are different implementations spanning 20 years (some written in assembler), it isn’t possible to run them on the same hardware. The key observation is that no-one has ever done better on any of those processors. Gernot ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

i have some questions about domain and thread
by 김은영 04 Apr '16

04 Apr '16

Hi, all first, I do not speak English well. please answer to me easily. i'm studying seL4 kernel source code. i have some questions. 1. What is domain? i read manual but i don't understand well. I hope that you explain to me in detail about the domain. 2. What is the maximum number of threads that can be created in one domain? 3. Usually there is a function to create a new thread in kernel source code. but i can't find the function in seL4 kernel source code. What is the way to create a new user thread in seL4? also, what is the way to exit user thread in seL4? thanks.

2 1

Questions about Kernel Memory Mapping
by Daniel Wang 01 Apr '16

01 Apr '16

Hi all, I’m trying to understand the seL4 kernel source code. I think the memory mapping between physical memory and virtual memory is a key point since it is directly related to how kernel functions and manage badges. I noticed that the kernel turns on the paging very early. Can someone help me or point out some resources how kernel memory is allocated? Especially how during and after the booting what the kernel memory snapshot looks like and things like that. For example, I traced to map_kernel_window() function and even before that there is some pptr to paddr conversion. I would really appreciate the help. Thanks -Dan

3 2

seL4 Documentation/Tutoria
by xurongfeik 31 Mar '16

31 Mar '16

Hi folks Is there any Documentation/Tutorial about execution time for typical invocations of the seL4 system calls? Thanks! -- 许荣飞 Rongfei Xu 北京航空航天大学 Beihang University

2 1

sel4 build tutorial
by Jorge Alberto Garcia 31 Mar '16

31 Mar '16

Hi folks Is there any Documentation/Tutorial about how to do a build to start testing seL4 ? where can I find the current boards/architectures supported? Thanks!

2 2

Network Stack and Driver
by Norrathep Rattanavipanon 31 Mar '16

31 Mar '16

Hello, My name is Oak and I'm working with Prof. Gene Tsudik for remote attestation project using sel4. I know that you guys are not interested in developing network stack and drivers for sel4. But do you happen to know if anyone else has done some work with network stack and Wi-fi, Bluetooth or ethernet driver in sel4? Regards, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

答复:答复: 答复:Re: About the execution time of seL4 API
by xurongfeik 29 Mar '16

29 Mar '16

裴老师：您好！谢谢您的资料。现在我们学校有两个团队在做这方面的工作：其中我们实验室主要在模型层对seL4微内核进行建模仿真，主要是把微内核基本功能机制建模成为一个基本模型，对User Mode扩展部分以策略模型的方式与基本模型进行编织，从而建立一套在设计早期通过模型仿真验证策略的方法。目前，我们正着手建立一个能准确反映真实seL4微内核运行的模型，但是由于仿真时钟的不准确，我们希望在某一硬件环境上把seL4微内核模型下层的系统调用时间统计出来，通过时间累加计算seL4微内核模型上的应用执行过程。但是目前不知道该如何获取这些系统调用的执行时间，不知道裴老师您那边是否有相关的数据？另外一个团队主要是基于seL4微内核的操作系统开发，主要考虑分区、并发的不确定性。目前主要用于航天的应用中。如果裴老师有相关的研究，非常愿意共同合作！祝好！许荣飞在 2016-03-29 14:39:35，"XilongPei" <pei.xilong(a)kortide.com> 写道： XuRongfei: 我是同济大学电信学院老师裴喜龙，我们从事你说的这个方向好几年了。附件文件是我把seL4的说明书翻译成了中文，下面这个链接是我们做的高可用操作系统的项目工程页面。 http://elastos.org/redmine/projects/rt-elastos这个工程的源码在： https://github.com/elastos/HD-Elastos 我们基于AOP思想做的操作系统（正在开发中），官网：http://elastos.org/project-guide/ 源码开源在github: https://github.com/elastos/ElastosRDK5_0它基于AOP思想，提出一种构件技术CAR，并基于这个构件技术，实现了一… 希望国内做相关工作的人能合作，共同做一些大的工程。同济大学裴喜龙 2016年3月29日星期二发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 xurongfeik 发送时间: 2016年3月29日 14:11 收件人: Thomas Sewell <thomas.sewell(a)nicta.com.au> 抄送:devel@sel4.systems 主题: [seL4] 答复:Re: About the execution time of seL4 API Thank you for your reply！ My name is XuRongfei, and I am a PHD student from China,Beijing. Now I focus on RTOS Modeling and Simulation. As we know, an important principle of microkernel design is the separation of mechanism and policy, it is what enables the construction of arbitrary systems on top of a minimal kernel. This separation of mechanism and policy is similar to AOM(Aspect-Oriented Modeling) and we can model the mechanism and policy separately. The biggest advantage is that analysis and verification of the policy applied in the implementation phase will be advanced to the design stage. As seL4 Microkernel is "the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement". So if we want to construct an RTOS on top of seL4 Microkernel, it is necessary to simulate and analyse the policy model on the microkernel model first. To simulate the seL4 Microkernel model accurately and agree with the real situation, the execution time of seL4 typical API (such as send\receive\notify message and Resume\Suspend\Create thread) for certain platform. So how can we get the execution time of this APIs for certain platform? Is it possible? Thank you very much! At 2016-03-29 11:45:42, "Thomas Sewell" <thomas.sewell(a)nicta.com.au> wrote: Hmm, what do you mean by measuring the time? You can measure the typical execution time of various system calls easily enough by checking the CPU cycle counter. There is an internal "sel4bench" project which is similar to "sel4test" but measures timing information of some system calls. My understanding is that this will be released at some point in the near future. It's also possible to calculate the worst-case execution time of the kernel for some platforms. There's been a lot of research work on this http://ssrg.nicta.com.au/projects/TS/realtime.pml by various people at Data61/NICTA. It's probably possible to replicate for some platform of interest, but it might be quite difficult to do. Cheers, Thomas. On 29/03/16 14:06, xurongfeik wrote: Hello，everyone： When given a specific platform， is it possible to measure the execution time of seL4 API？ Anyone who has the relative data please send it to me， many thanks！！ -- 许荣飞 Rongfei Xu 北京航空航天大学 Beihang University _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

2 1

About the execution time of seL4 API
by xurongfeik 29 Mar '16

29 Mar '16

Hello，everyone： When given a specific platform， is it possible to measure the execution time of seL4 API？ Anyone who has the relative data please send it to me， many thanks！！ -- 许荣飞 Rongfei Xu 北京航空航天大学 Beihang University

3 4

Where can I get the information about Linux on seL4
by XilongPei 29 Mar '16

29 Mar '16

Hi Gernot, I found that the footer of http://ssrg.nicta.com.au/ is: Served by Apache on Linux on seL4 Whare can I get more information about Linux on seL4? Xilong Pei Tongji University 2016/3/29

2 1

Status of ARMv8 support for seL4 ?
by karim.allah.ahmed＠gmail.com 28 Mar '16

28 Mar '16

Hello, >From this roadmap [0], I can see that ARMv8 support is underway at the moment. Is this something that's going to be released soon given that the roadmap says Q1-2016 (at least 32-bit) ? [0] https://sel4.systems/Info/Roadmap -- Karim Allah Ahmed.

1 0

Porting Qubes OS to seL4 project
by Paul Vlase 28 Mar '16

28 Mar '16

No answer ... Am I doing something wrong? Beside not have patience. Could anyone tell about the status of the seL4 Qubes port project and who can I get in touch with to talk more about it? On Tue, Mar 22, 2016 at 11:35 PM, Paul Vlase <vlase.paul(a)gmail.com> wrote: > Hello, > > My name is Paul Vlase and I am following a master degree right now. I > am interested in porting the Qubes OS to seL4 project and I saw that > you are working already on it. Is there anything I can help you on > this project? > > Thank you, > Paul Vlase

2 1

sel4 in TrustZone
by Norrathep Rattanavipanon 27 Mar '16

27 Mar '16

Hi again :) Is it possible to run sel4 as a secure world OS in TrustZone? Has anyone successfully done that before? Thank you, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

6 6

(simple?) build error?
by 谢文龙 27 Mar '16

27 Mar '16

I'm getting an error when building from Ubuntu. I'm building from: repo init -u https://github.com/seL4/sel4test-manifest.git I've configured with: make ia32_simulation_release_xml_defconfig and done "make menuconfig" accepting the defaults. Finally I run make and get errors: [KERNEL] [PBF_GEN] arch/object/structures.pbf [PBF_GEN] arch/api/shared_types.pbf [PBF_GEN] plat/machine/hardware.pbf [PBF_GEN] api/types.pbf [BF_GEN] arch/object/structures_gen.h [BF_GEN] arch/api/shared_types_gen.h [BF_GEN] plat/machine/hardware_gen.h [BF_GEN] api/types_gen.h [CPP] src/arch/x86/32/machine_asm.s [AS] src/arch/x86/32/machine_asm.o [CPP] src/arch/x86/32/traps.s [AS] src/arch/x86/32/traps.o [CPP] src/arch/x86/32/head.s [AS] src/arch/x86/32/head.o [CPP] src/arch/x86/halt.s [AS] src/arch/x86/halt.o [CPP] src/arch/x86/idle.s [AS] src/arch/x86/idle.o [TOUCH] sources_list_updated [CPP_GEN] kernel_all.c [CPP] kernel_all.c_pp [CP] kernel_final.c [CC] kernel_final.s [AS] kernel.o [LD] kernel.elf /usr/bin/ld:linker.lds_pp:5: syntax error collect2: error: ld returned 1 exit status make[1]: *** [kernel.elf] Error 1 make: *** [kernel_elf] Error 2 make V=3 mkdir -p /home/talos/seL4test/stage/x86/pc99 mkdir -p /home/talos/seL4test/build/x86/pc99 mkdir -p /home/talos/seL4test/images mkdir -p /home/talos/seL4test/stage/x86/pc99/common cp -R /home/talos/seL4test/tools/common/* /home/talos/seL4test/stage/x86/pc99/common [libs/libsel4] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4 CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4 -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4 SOURCE_DIR=/home/talos/seL4test/libs/libsel4 V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4' [GEN] include/sel4/types_gen.h [GEN] arch_include/x86/sel4/arch/invocation.h [GEN] include/sel4/shared_types_gen.h [GEN] sel4_arch_include/ia32/sel4/sel4_arch/invocation.h [HEADERS] [STAGE] api/* [STAGE] interfaces/* [STAGE] sel4/* [STAGE] interfaces/* [STAGE] sel4/* [STAGE] interfaces/* [STAGE] sel4/* [STAGE] sel4/* [STAGE] interfaces/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4' [libs/libsel4] done. [libs/libmuslc] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libmuslc CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libmuslc -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libmuslc/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libmuslc SOURCE_DIR=/home/talos/seL4test/libs/libmuslc V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libmuslc' make[1]: Nothing to be done for `default'. make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libmuslc' [libs/libmuslc] done. [libs/libcpio] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libcpio CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libcpio -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libcpio/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libcpio SOURCE_DIR=/home/talos/seL4test/libs/libcpio V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libcpio' [HEADERS] [STAGE] cpio/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libcpio' [libs/libcpio] done. [libs/libutils] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libutils CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libutils -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libutils/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libutils SOURCE_DIR=/home/talos/seL4test/libs/libutils V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libutils' [HEADERS] [STAGE] utils/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libutils' [libs/libutils] done. [libs/libsel4vka] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4vka CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4vka -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4vka/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4vka SOURCE_DIR=/home/talos/seL4test/libs/libsel4vka V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4vka' [HEADERS] [STAGE] vka/* [STAGE] vka/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4vka' [libs/libsel4vka] done. [libs/libsel4vspace] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4vspace CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4vspace -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4vspace/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4vspace SOURCE_DIR=/home/talos/seL4test/libs/libsel4vspace V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4vspace' [HEADERS] [STAGE] vspace/* [STAGE] vspace/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4vspace' [libs/libsel4vspace] done. [libs/libplatsupport] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libplatsupport CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libplatsupport -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libplatsupport/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libplatsupport SOURCE_DIR=/home/talos/seL4test/libs/libplatsupport V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libplatsupport' [HEADERS] [STAGE] platsupport/* [STAGE] platsupport/* [STAGE] platsupport/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libplatsupport' [libs/libplatsupport] done. [libs/libsel4simple] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4simple CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4simple -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4simple/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4simple SOURCE_DIR=/home/talos/seL4test/libs/libsel4simple V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4simple' [HEADERS] [STAGE] simple/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4simple' [libs/libsel4simple] done. [libs/libsel4simple-default] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4simple-default CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4simple-default -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4simple-default/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4simple-default SOURCE_DIR=/home/talos/seL4test/libs/libsel4simple-default V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4simple-default' [HEADERS] [STAGE] simple-default/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4simple-default' [libs/libsel4simple-default] done. [libs/libsel4platsupport] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4platsupport CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4platsupport -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4platsupport/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4platsupport SOURCE_DIR=/home/talos/seL4test/libs/libsel4platsupport V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4platsupport' [HEADERS] [STAGE] sel4platsupport/* [STAGE] sel4platsupport/* [STAGE] sel4platsupport/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4platsupport' [libs/libsel4platsupport] done. [libs/libelf] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libelf CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libelf -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libelf/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libelf SOURCE_DIR=/home/talos/seL4test/libs/libelf V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libelf' [HEADERS] [STAGE] elf/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libelf' [libs/libelf] done. [libs/libsel4utils] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4utils CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4utils -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4utils/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4utils SOURCE_DIR=/home/talos/seL4test/libs/libsel4utils V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4utils' [HEADERS] [STAGE] sel4utils/* [STAGE] sel4utils/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4utils' [libs/libsel4utils] done. [libs/libsel4muslcsys] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4muslcsys CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4muslcsys -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4muslcsys/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4muslcsys SOURCE_DIR=/home/talos/seL4test/libs/libsel4muslcsys V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4muslcsys' [HEADERS] [STAGE] arch_stdio.h [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4muslcsys' [libs/libsel4muslcsys] done. [libs/libsel4allocman] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4allocman CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4allocman -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4allocman/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4allocman SOURCE_DIR=/home/talos/seL4test/libs/libsel4allocman V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4allocman' [HEADERS] [STAGE] allocman/* [STAGE] allocman/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4allocman' [libs/libsel4allocman] done. [libs/libsel4test] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4test CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4test -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4test/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4test SOURCE_DIR=/home/talos/seL4test/libs/libsel4test V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4test' [HEADERS] [STAGE] sel4test/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4test' [libs/libsel4test] done. [apps/sel4test-tests] building... mkdir -p /home/talos/seL4test/build/x86/pc99/sel4test-tests CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/sel4test-tests -f /home/talos/seL4test/.config -f /home/talos/seL4test/apps/sel4test-tests/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/sel4test-tests SOURCE_DIR=/home/talos/seL4test/apps/sel4test-tests V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/sel4test-tests' [HEADERS] [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/sel4test-tests' [apps/sel4test-tests] done. [KERNEL] mkdir -p /home/talos/seL4test/build/kernel make -C /home/talos/seL4test/build/kernel -f /home/talos/seL4test/kernel/Makefile \ SOURCE_ROOT=/home/talos/seL4test/kernel O=/home/talos/seL4test/build/kernel V=3 \ TOOLPREFIX= \ CONFIG_DOMAIN_SCHEDULE= \ HAVE_AUTOCONF=1 NO_PRESERVE_TIMESTAMP=1 seL4 build options: =================== ARCH = x86 PLAT = pc99 CPU = TOOLPREFIX = PATH = /home/talos/bin:/home/talos/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games DEBUG = ASSERT = CONFIG_DEFS = CYCLE_COUNTER PERF_COUNTER=CYCLE_COUNTER DANGEROUS_CODE_INJECTION = CC = gcc CC_PATH = CPP = cpp CPP_PATH = AS = as AS_PATH = LD = ld LD_PATH = PARSER = c-parser PARSER_PATH = BF_GEN = bitfield_gen.py BF_GEN_PATH = SYSCALL_ID_GEN = syscall_header_gen.py SYSCALL_ID_GEN_PATH = INVOCATION_ID_GEN = invocation_header_gen.py INVOCATION_ID_GEN_PATH = XMLLINT_PATH = XMLLINT = xmllint.sh CFLAGS = -fno-stack-protector -m32 --std=c99 -nostdlib -nostdinc -ffreestanding -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -Wdeclaration-after-statement "-I/home/talos/seL4test/kernel/include/arch/x86/arch/32" "-I/home/talos/seL4test/kernel/include/plat/pc99/plat/32" -O2 -mno-mmx -mno-sse -mno-sse2 -mno-3dnow -DCYCLE_COUNTER -DPERF_COUNTER=CYCLE_COUNTER -DFASTPATH ASFLAGS = -Wa,--32 "-I/home/talos/seL4test/kernel/include/arch/x86/arch/32" "-I/home/talos/seL4test/kernel/include/plat/pc99/plat/32" CPPFLAGS = -DHAVE_AUTOCONF -I/home/talos/seL4test/include/generated -DARCH_X86 -DIA32 -DARCH_IA32 -D__KERNEL_32__ -DX86_32 -DPLAT_PC99 -DFASTPATH -DCYCLE_COUNTER -DPERF_COUNTER=CYCLE_COUNTER -DFASTPATH "-I/home/talos/seL4test/kernel/include/arch/x86/arch/32" "-I/home/talos/seL4test/kernel/include/plat/pc99/plat/32" LDFLAGS = -Wl,--build-id=none -Wl,-m,elf_i386 -nostdlib -nostdinc -Wl,--build-id=none -O2 make[1]: Entering directory `/home/talos/seL4test/build/kernel' [LD] kernel.elf /home/talos/seL4test/kernel/tools/changed.sh kernel.elf gcc -Wl,--build-id=none -Wl,-m,elf_i386 -nostdlib -nostdinc -Wl,--build-id=none -O2 -Wl,-T -Wl,linker.lds_pp \ -o kernel.elf src/arch/x86/32/machine_asm.o src/arch/x86/32/traps.o src/arch/x86/32/head.o src/arch/x86/halt.o src/arch/x86/idle.o kernel.o /usr/bin/ld:linker.lds_pp:5: syntax error collect2: error: ld returned 1 exit status make[1]: *** [kernel.elf] Error 1 make[1]: Leaving directory `/home/talos/seL4test/build/kernel' make: *** [kernel_elf] Error 2

2 1

sel4 benchmark
by Norrathep Rattanavipanon 24 Mar '16

24 Mar '16

Hello, What's the best way to benchmark my program inside sel4? I saw wiki page about running sel4 bench (https://wiki.sel4.systems/Benchmarking%20guide) but it wasnt filled yet. So I wonder if there's any public guide or tutorial on that? I also found this https://github.com/seL4/libplatsupport/blob/master/arch_include/x86/platsup… and tried both rdtsc_pure and rdtsc_cpuid but neither of them seems to produce reliable results. Best, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

sel4 job offer
by Julien Delange 24 Mar '16

24 Mar '16

For information, we are looking for people to work on sel4. See https://www.appone.com/maininforeq.asp?Ad=250944&R_ID=1243309&Refer=http://… If you have any question, do not hesitate to contact me and/or apply! Julien.

1 0

Porting Qubes OS to seL4 project
by Paul Vlase 22 Mar '16

22 Mar '16

Hello, My name is Paul Vlase and I am following a master degree right now. I am interested in porting the Qubes OS to seL4 project and I saw that you are working already on it. Is there anything I can help you on this project? Thank you, Paul Vlase

1 0

[CAmkES] CAmkES 2.1.0 Release Notes
by Stephen Sherratt 22 Mar '16

22 Mar '16

CAmkES 2.1.0 Release Notes ========================== ## New Features - runner takes an `--architecture` command line argument which selects the target architecture. Valid arguments are: aarch32, arm_hyp, ia32 - added the ability to specify a hardware dataport as cached. Previously all hardware dataports were mapped uncached. This feature is intended to be used on dataports backed by DMA-able memory to improve access times. Functions to flush dataports from the cache are also provided. - support for seL4 3.0.0 ## Removed Features - `--hyp` command line argument is replaced with `--architecture arm_hyp` ## API Removals ### Unmarshalling Helpers These were intended for use in templates, but are no longer used in any internal templates: - `camkes_marshal` - `camkes_marshal_string` - `camkes_unmarshal` - `camkes_unmarshal_string` ### DMA Utilities These had been deprecated for a long period and are now being removed: - `camkes_dma_page_alloc` - `camkes_dma_page_free` You can find it at: https://github.com/seL4/camkes-tool/tree/camkes-2.1.0 A manifest for the 2.1.0 compatible versions of test and example apps: https://github.com/seL4/camkes-manifest/blob/master/default-2.1.x.xml Release notes on the wiki: https://wiki.sel4.systems/CAmkES%202.1.0 Enjoy! ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

What happens to the IPC buffer when you make another process within the same Vspace?
by Qiwei Wen 20 Mar '16

20 Mar '16

Hi, I'm trying to write a multithreaded seL4 application. It's to be made up of sel4util processes with different cspaces and sharing the same Vspace. I managed to achieve this, but what confuses me is that since the processes share the same Vspace, wouldn't GetIPCBuffer() return the same result for each of them? I looked at libsel4/arch_include/arm/sel4/arch/functions.h, and GetIPCBuffer() is simply: return *(seL4_IPCBuffer**)seL4_GlobalsFrame; Since seL4_GlobalsFrame is just a fixed memory location (0xffffc000) in the shared address space, why does seL4_GetIPCBuffer() return different results for different processes? Below is the output: ========================== PARENT: IPCBUFFER: 00273000 CHILD: GlobalsFrame: ffffc000, *GlobalsFrame 10076000 CHILD: setting shared to 97 PARENT: CHILD DIED, shared char: 97, MR16: 00000000 ============================= Is it that the frame ffffc000 mapping is changed on every context switch perhaps? Can I absolutely trust that IPC is still working correctly with this set up? Thanks, David

5 4

Isabelle itself proven?
by Steve VanderLeest 20 Mar '16

20 Mar '16

Since the formal verification of functional correctness of seL4 was performed using the Isabelle theorem prover, could someone tell me if Isabelle itself has been formally verified? If so, could you suggest some good references to that work? Regards, Steve Steven H. VanderLeest, Ph.D. Chief Operating Officer DornerWorks, Ltd. 3445 Lake Eastbrook Grand Rapids, MI 49546 www.dornerworks.com

3 2

Booting process
by Daniel Wang 19 Mar '16

19 Mar '16

Hi all, I’m very new to seL4 development. I’m particularly interested in understanding seL4 kernel source code. Could someone points me out how the seL4 is booted and where should I start learning? Thanks -Dan

3 2

seL4 wiki
by Anna Lyons 18 Mar '16

18 Mar '16

Hi all, We've created a public wiki for seL4 development here: https://wiki.sel4.systems/ The kernel team have put some effort into creating the initial content, but there is much more to be done. Contributions encouraged! New accounts are restricted to avoid spam, but if you have posted on this mailing list your account will be approved quickly. Otherwise contact us. Thanks, Anna Lyons seL4 Kernel Engineer | PhD Student DATA61 | CSIRO E <mailto:Brigitte.Biscotto@data61.csiro.au> Anna.Lyons(a)data61.csiro.au<mailto:Anna.Lyons@data61.csiro.au> Level 3, K17 Building, UNSW Gate 14, Barker Street, Kensington, NSW, 2033 l Locked Bag 6016, Sydney NSW 1466 www.data61.csiro.au<http://www.data61.csiro.au/> CSIRO’s Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 [cid:image001.png@01D0EFD9.052ECFC0] ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

FYI: microkernel.info community site
by Jakub Jermář 14 Mar '16

14 Mar '16

Hello, just FYI, I have set up a simple web page[1] to promote the wider microkernel community and its goals. So far, the page comes with a brief description of the microkernel concept and an incomplete list of microkernel projects with links to each project's web. The description is made out of the first two sentences I found in the "What is XYZ" section or elsewhere on the web of the respective project. I also took the freedom to use the respective project's logo (or what I believed was the project's logo) for promoting it. I hope you will find this small web a good idea. It was inspired by a similar (though a little bit more informative) site set up by the unikernel community [2]. The sources of the [1] web are hosted on Github [3], so feel free to submit issues or PR to make the site better. Please send me a PM if there are any issues pertaining your project's cartouche that cannot be dealt with using Github. Thanks, Jakub [1] http://microkernel.info [2] http://unikernel.org/projects/ [3] https://github.com/jermar/microkernel.info

8 8

Capability faults on seL4_Send and seL4_Call
by Qiwei Wen 12 Mar '16

12 Mar '16

Hi all, I understand that capability faults for seL4_Send and seL4_Call only happen when the look-up fails, and not when illegal operations are attempted, such as calling a null cap or a piece of untyped memory. Is there another way at all, then, that such errors can be handled by user-level code? This is part of a project where the faulting process needs to surrender control to another process whenever it performs a system call on an invalid capability. Is there a way to achieve this given that fault endpoints will not work? Thanks, David

1 0

using camkesvm with qemu
by Julien Delange 10 Mar '16

10 Mar '16

Hi, I am currently trying to use the camkesvm example and run it in qemu. I am currently able to compile the c162_twovm_defconfig application. However, when running, I have the following issue (see below). So, I am wondering what would be the good arguments to start the application in qemu. I noticed that the kernel/initrd image for linux are specific in a header file, I assume this is also included in the image loaded by capdl. Any idea about how to run this example with qemu and/or how to test it? Thanks! Starting node #0 vt-x: not supported <<seL4 [decodeUntypedInvocation/193 T0xe2ff1900 "rootserver" @804afa7]: Untyped Retype: Insufficient memory or offset outside untyped>> Unmasking IOAPIC source 2 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 3 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 4 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 16 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 17 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 18 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 23 on ioapic 0 without ever setting its mode! <<seL4 [decodeCNodeInvocation/107 T0xe2ff1900 "rootserver" @804a4b2]: CNode Copy/Mint/Move/Mutate: Source slot invalid or empty.>> capDL-loader :: << Error: init_cnode_slot:1471: seL4_FailedLookup >> Ignoring call to sys_rt_sigprocmask

3 4

Recovering from cap fault?
by Qiwei Wen 10 Mar '16

10 Mar '16

Hi all, On page 26 of the manual (1.2) there's an instruction on how to restart a thread following a capability fault. The program counter where the faulting thread should pick up execution is said to be message register 0. What I'm trying to do is to restart the execution on the next instruction following the system call instruction so as to skip it. Try as I might, it will not work and the faulting thread is stuck in an endless number of faults. Below is the relevant code: seL4_Word pc = seL4_GetMR(0); printf("cap fault, pc: %08x, on %s\n",pc,seL4_GetMR(2)?"wait":"send"); //assert(!faultnum++); seL4_MessageInfo_t info = seL4_MessageInfo_new (seL4_CapFault,0,0,1); seL4_SetMR(0,pc + 4); seL4_Reply(info); It does restart, but immediately cap-faults again at the very same program counter. Is it supposed to work? What did I do wrong? Cheers, David

2 1

seL4 Tutorial Idea
by da Tyga 09 Mar '16

09 Mar '16

Hi Andrew Jackman! First of all apologies about my assumptions. In my hasty reading of your question I got the impression you were talking about yourself and not the intended audience for your tutorial material proposal. Like yourself, I too would use a practical, tutorial style guide if it were available. So I would like to give my vote for your idea. Unfortunately, I'm a one-man-show and thus not in a position to make a pledge towards a tutorial effort. Perhaps the good folks who are involved with seL4 could suggest how your proposal could come about. Reading these digests, tit would appear that there are quite a few people who are trying to come to grips with seL4. Yes, I was referring to the material that you linked. Cheers, Tyga >>> thread in reverse chrono-order: Andrew Jackman kd7nyq(a)gmail.com On Sun, Mar 6, 2016 at 11:04 AM, Jackman <kd7nyq(a)gmail.com> wrote: > Is anyone interested in tutoring on the topic of sel4? I have two > objectives: > > First, I'm interested in beginning programming, like getting through the > Hello World process. I would hope this eventually includes things like > basic driver development and practical application development. > > Second, I want to understand how virtualization works with sel4 and the > infrastructure behind it. My objective is to be able to stand up my own > virtualization host and guests. > > I'm not sure how payment would work. I'd be interested in turning our > experience into tutorials for community consumption, which may be more > valuable to some of you than the money. > > Thank you. > > Andrew Roy Jackman Hi Andrew, I don't wish to discourage you, but if you are just starting out programming and have limited knowledge of operating systems, etc ... then seL4 might be a very big undertaking to understand and learn from. There are a lot of topics you would need to come up to speed on. I suggest taking a look Gernot's course material at unsw.edu.au. > da Tyga: Thank you for writing back. I totally agree with your assessment. Permit me to elaborate a bit more on my situation. I am a professional software engineer who is primarily dedicated to writing virtualization automation software for sales demonstrations. Naturally, our department is always interested in ways in which we can improve the efficiency of our virtualization environment(s). After reading 'L4 Virtualization and Beyond' (2008, http://os.inf.tu-dresden.de/papers_ps/haertig08_l4_virtualization_and_beyon… ), I became fascinated with L4. I am here talking to you all because of the amount of press that seL4 has gotten as the proofed L4 kernel and because it appears to have the best, most easily understood documentation. Now, that does not mean that I think seL4 is well documented, just that it's the best documented of the L4 projects. The purpose of my original email was to very gently say that the introductory material to seL4 is so bad, that I'm willing to pay someone to either bring it up to date, assist me with it, or both. For example, there is a thread about RefOS, wherein Kevin wrote, "RefOS was a student project that is now no longer actively maintained." Gapry and HyperNewbie, however, provided at least some fixes, but their fixes don't appear to have gotten any attention from upstream. This was on 11 February. Nevertheless, RefOS appears to be the only seL4 project geared towards newcomers on the 'Getting Started' page ( https://sel4.systems/Info/GettingStarted/) You should note that, on that page, there is no indicator that newcomers should, in fact, stay away from that project because it's no longer maintained. I don't think requesting some attention on documentation is a bad or unjust thing. I would hope that lowering the barriers to entry to the seL4 community would increase the flow of developers, users, and sponsors to the seL4 project. In turn, I hope that would be seen as a good thing. I'm offering part-time, albeit unofficial, company sponsored development in exchange for some paid tutoring. I am not asking for a hand-out. If I didn't have to worry about ramp-up time or coming up with deliverables, I wouldn't be bugging you. Now, if you're worried about my qualifications, I'm a university educated computer scientist. While I've spent most of my career on web programming, I've studied operating systems development both at school and on my own. I began a toy kernel with the help of the osdev.org resources, and I'm happy with my progress. When I take inventory, however, I realize I don't have the desire to (re-)write an L4 kernel, nor do I think I can improve upon it. Finally, I think you're referring to Professor Gernot Heiser's page at https://www.cse.unsw.edu.au/~gernot/, and probably more specifically the CS9242 course at http://www.cse.unsw.edu.au/~cs9242/current/. If you're referring to another course, please be more specific. Thank you. Andrew Jackman kd7nyq(a)gmail.com

5 5

Tutor?
by Jackman 09 Mar '16

09 Mar '16

Is anyone interested in tutoring on the topic of sel4? I have two objectives: First, I'm interested in beginning programming, like getting through the Hello World process. I would hope this eventually includes things like basic driver development and practical application development. Second, I want to understand how virtualization works with sel4 and the infrastructure behind it. My objective is to be able to stand up my own virtualization host and guests. I'm not sure how payment would work. I'd be interested in turning our experience into tutorials for community consumption, which may be more valuable to some of you than the money. Thank you. Andrew Roy Jackman

2 2

Performce test for CAMKES or RefOS
by ぷ风过无痕?? 08 Mar '16

08 Mar '16

Hi everyone, I want to measure a variety of important aspects of system performance on CAMKES or RefOS. I know that Lmbench is an extensive suite of micro-benchmarks that give powerful insights into system performance. And lmbench is written in ANSI-C,so it is portable across a wide variety of systems and architectures. Can I measure the system performance on CAMKES or RefOS using Lmbench ? Thank you.

2 1

Re: [seL4] Devel Digest, Vol 22, Issue 1
by da Tyga 08 Mar '16

08 Mar '16

Hi Andrew, I don't wish to discourage you, but if you are just starting out programming and have limited knowledge of operating systems, etc ... then seL4 might be a very big undertaking to understand and learn from. There are a lot of topics you would need to come up to speed on. I suggest taking a look Gernot's course material at unsw.edu.au. On 7 March 2016 at 12:00, <devel-request(a)sel4.systems> wrote: > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. Tutor? (Jackman) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sun, 6 Mar 2016 11:04:25 -0700 > From: Jackman <kd7nyq(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] Tutor? > Message-ID: > < > CAADorGK4z2oW4JoBq+K--72LDGc0d-2-1jTxUu41UxidvwjkHw(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Is anyone interested in tutoring on the topic of sel4? I have two > objectives: > > First, I'm interested in beginning programming, like getting through the > Hello World process. I would hope this eventually includes things like > basic driver development and practical application development. > > Second, I want to understand how virtualization works with sel4 and the > infrastructure behind it. My objective is to be able to stand up my own > virtualization host and guests. > > I'm not sure how payment would work. I'd be interested in turning our > experience into tutorials for community consumption, which may be more > valuable to some of you than the money. > > Thank you. > > Andrew Roy Jackman >

1 0

Can not build RefOS
by Gapry Un 08 Mar '16

08 Mar '16

Dear all, I follow the official step (https://github.com/seL4/refos-manifest) to build RefOS and it occurs the following error message. In file included from /home/chi-wai/Workspaces/microkernel/RefOS/libs/librefos/src/sync.c:16:0: ~/Workspaces/RefOS/stage/arm/imx31/include/refos/refos.h:73:1: *error: unknown type name ‘uint32_t’* ~/Workspaces/RefOS/stage/arm/imx31/include/refos/refos.h:73:23: *error: unknown type name ‘uint32_t’* In file included from /home/chi-wai/Workspaces/microkernel/RefOS/libs/librefos/src/sync.c:18:0: ~/Workspaces/RefOS/stage/arm/imx31/include/refos-util/cspace.h:44:72: *error: unknown type name ‘uint32_t’* ~/Workspaces/RefOS/libs/librefos/src/sync.c: In function ‘sync_create_mutex’: ~/Workspaces/RefOS/libs/librefos/src/sync.c:49:5: *warning*: ‘seL4_Notify’ is deprecated (declared at /home/chi-wai/Workspaces/microkernel/RefOS/stage/arm/imx31/include/sel4/deprecated.h:23): use seL4_Signal [-Wdeprecated-declarations] ~/Workspaces/RefOS/libs/librefos/src/sync.c: In function ‘sync_acquire’: ~/Workspaces/RefOS/libs/librefos/src/sync.c:65:5: *error: invalid initializer* ~/Workspaces/RefOS/libs/librefos/src/sync.c: In function ‘sync_release’: ~/Workspaces/RefOS/libs/librefos/src/sync.c:74:5: *warning*: ‘seL4_Notify’ is deprecated (declared at /home/chi-wai/Workspaces/microkernel/RefOS/stage/arm/imx31/include/sel4/deprecated.h:23): use seL4_Signal [-Wdeprecated-declarations] make[1]: *** [src/sync.o] Error 1 make: *** [librefos] Error 2 Does RefOS use the old seL4 API ? If it is, which version I need to downgrade? Thanks for any help or suggestion, Gapry. https://gapry.wordpress.com/

6 9

Re: [seL4] Devel Digest, Vol 21, Issue 11
by ぷ风过无痕?? 23 Feb '16

23 Feb '16

Hi everyone,I find an interesting problem when I read the code of endpoint(kernel\src\object\endpoint.c). In the sendIPC and receiveIPC functions , I see there are 3 states for an endpoint(Idle , send , receive). Below it is the state machine diagram. sendIPC EPState_Recv ——> EPState_Idle ——>EPState_send receiveIPC EPState_send——> EPState_Idle ——>EPState_Recv But when I add some print infomation, I find the endpoint can never reach the Send state. I think the correct state machine diagram just has two states(idle and receive). sendIPC EPState_Recv ——> EPState_Idle receiveIPC EPState_Idle ——>EPState_Recv Am I right???

2 1

Timer for AM335x
by Julien Delange 17 Feb '16

17 Feb '16

I am trying to develop a camkes application with one component having access to the timer. I got some inspiration from the time server for the kzm machine. Now, I am trying to port that to the am335x machine to execute on a beagleboard black. I dig into the code and found the appropriate platform-specific functions to call. Unfortunately, when trying to compile, it fails (see below). Anybody has an idea why this happens? Also, if you want to look at the camkes application, I put it on github at https://github.com/juli1/sel4-experiments/tree/master/camkes/pingimpl-am335x Thanks for any help! /home/sel4/test/camkes/build/arm/am335x/pingimpl/src/timer/static/components/timer/src/timer.o: In function `irq_callback': /home/sel4/test/camkes/apps/pingimpl/components/timer/src/timer.c:22: undefined reference to `dm_handle_irq' /home/sel4/test/camkes/apps/pingimpl/components/timer/src/timer.c:32: undefined reference to `dm_oneshot_relative' /home/sel4/test/camkes/build/arm/am335x/pingimpl/src/timer/static/components/timer/src/timer.o: In function `run': /home/sel4/test/camkes/apps/pingimpl/components/timer/src/timer.c:58: undefined reference to `dm_oneshot_relative' collect2: error: ld returned 1 exit status

2 2

handling timer with camkes
by Julien Delange 16 Feb '16

16 Feb '16

Dear all, I would like to build a scheduler on top of camkes. I figure that I have to get access to the timer irq and start from there (e.g. then, dispatch other tasks according to the number of elapsed ticks). I did find some relevant examples, especially in the camkes-vm ( https://github.com/seL4/camkes-vm) but nothing I can try. Is there any information about such materials? I tried to reuse the component but always got build error. I was wondering if there was an existing tutorial or an example I could try that will help me. Thanks. Julien.

2 3

Allocation of untyped memory
by Norman Feske 09 Feb '16

09 Feb '16

Hello, while moving Genode's seL4 support to seL4 version 2, I stumbled over the dynamic allocation within untyped memory regions. In the old experimental branch that I used previously, the retype-untyped operation allowed me to manually specify an offset where the new kernel object should be placed within the untyped memory region. So I was able to manage the allocation of untyped memory manually. In short, I added each initial untyped memory region to a roottask-local "phys-mem" allocator. Each time when creating a kernel object, I asked this allocator for a region of the required size and alignment, determined the untyped-memory capability that belongs to the found region, and used this capability to create the kernel object(s) at the calculated offset within the untyped-memory region. This worked very well. After switching to version 2, I found the retype-untyped operation to lack the offset argument (which admittedly was never present in the non-experimental version). Instead of accepting an offset parameter, the kernel maintains a built-in allocator per untyped-memory region. (please correct me if my understanding is wrong) The allocator is basically a simple offset value ("FreeIndex") that is increased with each allocation. Since I no longer have the chance to specify the offset explicitly, I have to rely on the allocation policy of the kernel and hit the following problem: There exists an untyped memory region of size 0x2000. Initially, the FreeIndex is 0. Now, I am creating the following kernel objects within the untyped-memory region: 1. CNode with totalObjectSize 0x400: -> The allocation increases FreeIndex to 0x400. 2. CNode with totalObjectSize 0x800: -> The FreeIndex gets aligned to 0x800 (natural alignment of the to-be-created CNode). This creates a gap between 0x400 and 0x800. -> The allocation increases FreeIndex to 0x1000. 3. seL4_IA32_4K with a totalObjectSize 0x1000: -> The allocation increases FreeIndex to 0x2000. 4. CNode with totalObjectSize 0x400: <<seL4 [decodeUntypedInvocation/209 T0xe3fc9900 "rootserver" @2013228]: Untyped Retype: Insufficient memory (1 * 1024 bytes needed, 0 bytes available).>> Since FreeIndex equals the size of the untyped memory region, the kernel concludes that untypedFreeBytes is 0. Even though there exists a gap of 0x400 within the untyped memory region that satisfies the alignment of the to-be-created kernel object, the kernel won't allow me to use it. In contrast, with the retype-untyped-at-offset operation, such a situation never occurred. Right now, I am a bit puzzled about how to proceed and have the following questions in the back of me head: * What is the rationale behind fixing the allocation policy within untyped memory regions in the kernel. Doesn't this design contradict with the principle of avoiding policy in the kernel? In my specific case, this policy seemingly makes my life much more difficult. To use the kernel in a deterministic way, I would need to model the kernel's allocation behavior in the user land. * From what I gather from the kernel's source code, the built-in allocator would not allow me to reuse parts of untyped memory regions because 'FreeIndex' is always increasing. E.g., after revoking the CNodes of steps 1 and 2, I still cannot create any new kernel objects within the untyped memory region because FreeIndex remains equal the size of the untyped memory region. Is this correct? * Is it possible to give me the retyped-untyped-at-offset operation back? ;-) e.g., in the form of a patch? Or alternatively, are there any best practices that I could follow wrt managing untyped memory? Maybe I'm just approaching the problem from the wrong angle? Best regards Norman -- Dr.-Ing. Norman Feske Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

3 5

Upgrading to Camkes 2.0
by Jeff Hieb 25 Jan '16

25 Jan '16

I was looking to upgrade to CAmkES release 2.0. but can't get an example arm configuration to compile. I did a a fresh clone using https://github.com/seL4/camkes-manifest.git and found the ia32_simple_defconfig compiles fine, but not arm_simple_defconfig make arm_simple_defconfig make [libs/libsel4] building... make[1]: *** No rule to make target `/home/sysjeff/Camkes2/libs/libsel4/sel4_arch_include/arm/interfaces/sel4arch.xml', needed by `include/interfaces/sel4_client.h'. Stop. make: *** [libsel4] Error 2 looks like the arm directory got renamed to aarch32 and part of the build system doesn't know? $ ls /home/sysjeff/Camkes2/libs/libsel4/sel4_arch_include/ aarch32/ ia32/ Is there something simple I am missing? Thanks, Jeff -- Jeffrey L. Hieb Department of Engineering Fundamentals University of Louisville Louisville Kentucky 40292 (502) 852 0465

2 2

Issue with CAmkES tutorial
by James Hasner 21 Jan '16

21 Jan '16

All, Noticed an issue with the tutorial for creating a dataport application with CAmkES components. This issue is on https://wiki.sel4.systems/CAmkES%20Tutorial within the Makefile and Kbuild section. You titled the application "helloevent" instead of hellodataport, causing the newly created application to not be able to access the header files needed. Thanks, James

2 1

Announcing Robigalia, make seL4 applications with Rust!
by Corey Richardson 07 Jan '16

07 Jan '16

Hi all, On behalf of the Robigalia project I am pleased to announce our first public release of the core libraries for using Rust on seL4. Currently, this consists of a raw interface akin to libsel4 and a higher-level "Rustic" interface. Currently, only x86 is supported. An ARM port is in progress. We have a website: https://robigalia.org/ And a mailing list: https://lists.robigalia.org/listinfo/robigalia-dev The goal of the Robigalia project is to promote Rust as a robust choice for application development on seL4 and has the long-term goal of producing Robigo, a POSIX-compatible personality on seL4. We're in the initial stages of development. We are primarily a group of students from Clarkson University, though other contributors are starting to trickle in. Currently in-progress is a port of the tutorial from the sel4-tutorials repositories and examples of doing various things using the libraries we've created. Beyond those, we're also working on x86 platform support, right now virtio and PCI bus management. (I didn't intend on posting this for another week, to finish the tutorial and high-level library, but it was scooped on HN, so I figured I might as well) -- cmr +16032392210 http://octayn.net/

2 1

Hardware Platform for sel4 and running linux as guest os
by Julien Delange 07 Jan '16

07 Jan '16

Dear all, I am looking to purchase a board for a project that will use sel4. I have the following hardware requirements: - serial port - ethernet - potentially usb Then, I want to run linux on top of sel4 and have also some native components. In the linux partition, I would like to control the usb and potentially the ethernet. In the native components, I am planning to use the serial port (communication with other components). I thought the beagleboard black would be a good match. Does anyone tried to run linux as a guest os on this platform? If yes, is there any tutorial/example to set it up? Also, any information about how to use the serial ports and other hardware components? Also, if you have an experience with any other board (x86 or ARM - the platform does not really matter), is it possible to indicate what you would recommend? Thanks for any help or suggestion, Julien.

6 6

CAmkES 2.0.0
by Ihor Kuz 06 Jan '16

06 Jan '16

The Trustworthy Systems Team at Data61 (formerly NICTA) is pleased to announce CAmkES release 2.0.0 The new release updates CAmkES to be compatible with seL4 version 2.0.0. It also marks the transition to more frequent and regular releases, as well as switching our release process to semantic versioning, so it's easy to tell which CAmkES releases are source-compatible, or will require updates to user-level code, and also with which seL4 versions they will be compatible. You can find it at: https://github.com/seL4/camkes-tool/tree/2.0.0 And a manifest for the 2.0.0 compatible versions of the CAmkES test and example apps: https://github.com/seL4/camkes-manifest/blob/master/default-2.0.x.xml Enjoy! ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

Extending errors to always include argument numbers
by Corey Richardson 05 Jan '16

05 Jan '16

For consistency, it seems like it'd beneficial if: seL4_RangeError seL4_AlignmentError seL4_DeleteFirst seL4_FailedLookup seL4_RevokeFirst included an indication of which argument the error applies to. For some of these errors, not every call has a unique argument which can cause the erorr. This seems like a relatively straightforward change for me to get acquainted with the full process of modifying and re-verifying the kernel. Are there tradeoffs hidden here that would make this undesirable? -- cmr +16032392210 http://octayn.net/

3 2

seL4 & camkes questions
by Julien Delange 04 Jan '16

04 Jan '16

Hello, First of all, thanks for the help you provided previously. After downloading the virtual machine, everything was fine and I was able to try seL4 and camkes by using the tutorials. Thanks also for making this documentation available publicly, it definitively helps a lot to learn the principles of this operating system. I still do have some questions regarding sel4 and camkes. - About camkes, what are the thread mapping rules. How a component is transformed into one (or several) sel4 threads? Is there a mapping 1 component = 1 thread or is it possible to have multiple threads per component? - How can I find the code generated by camkes? The idl/adl code is ultimately transformed into C code and I was wondering where I could see the code. - How the real-time requirements are handled in camkes? For example, how can I specify that a component is executed periodically every XXX ms. Does the ADL supports that? - How can we specify the scheduling constraints? Can we have an ARINC653-like scheduling where every process has a fixed time slice to be executed? Since the behavior of the system can be deduced from the execution time, allocated a fixed time slice also avoid some attacks - About scheduling, what are the policies actually supported? - How timing is handled? I tried to use nanosleep() from the libc but it seems the syscall/service is not implemented. I also tried the timer example from the sel4 tutorial but when compiling, there is an error (the function timer_handle_irq needs an IRQ as a parameter). Any idea how to fix the example and more information about how time is handled? - is it possible for the OS to load and launch multiple elf at the same time or other processes must be manually started? - How capabilities and services are associated? From the example hello-2 in the sel4 tutorial, I see that a capability is declared (with vka_alloc_endpoint(&vka, &ep_object)) but I do not understand how this is associated with the message being sent between both tasks. In other words, how is it possible to associated a capability with a service. When sending or receiving a message (for example, by using seL4_SetMR(0, MSG_DATA);), there is no use of the capability. So, how the kernel can check that the thread can effectively send a message? - Is there any efforts to support standards such as ARINC653 or MILS? (even experimental) - Is there any significant/big projects that are available online and you would recommend to learn the OS and its associated libraries? Hope you do not mind such a list of questions! I really enjoy digging into the OS and it seems very interesting. Thanks for any help/comment.

4 4

DMA
by Raymond Jennings 04 Jan '16

04 Jan '16

Is it ever possible for seL4 to run on a conventional machine without an IOMMU if any code that manipulates a DMA capable device is included as trusted or does DMA automatically void any assurance? Reason for question: Running seL4 on a system without an IOMMU.

4 8

Determining when would-have-blocked
by Corey Richardson 04 Jan '16

04 Jan '16

Looking at the manual and the C impl, it seems there is no robust way to determine if a non-blocking send failed. How should an application handle this? NBRecv sets the badge register to zero when the recv "failed" - is it expected that most/all endpoints will be badged? I'm still trying to get a feel for what a system designed for this model would look like. -- cmr +16032392210 http://octayn.net/

3 2

Tutorial error
by Julien Delange 23 Dec '15

23 Dec '15

Hello, I am trying to reproduce the tutorial. I followed the steps from the slides on https://github.com/seL4-projects/sel4-tutorials/blob/master/docs/seL4Tutori… When trying to compile, I got the following error in [1]. It seems to be a warning from the compiler, so, I edit the CFLAGS in the .config and tried to compile but then got the error in [2], which then avoid any potential compilation. Is there any special setup for the compiler? I am currently using gcc 5.2.1. Thanks for any suggestion, Julien. [1] /home/julien/tmp/sel4-tutorials/stage/x86/pc99/include/vka/object.h:286:5: warning: 'seL4_AsyncEndpointObject' is deprecated (declared at /home/julien/tmp/sel4-tutorials/stage/x86/pc99/include/sel4/objecttype.h:23): use seL4_NotificationObject [-Wdeprecated-declarations] [2] /home/julien/tmp/sel4-tutorials/kernel/src/plat/pc99/machine/acpi.c:38:13: error: size of array '__assert_failed_acpi_rsdp_packed' is negative

2 2

Camkes dependencies & development environment
by Julien Delange 23 Dec '15

23 Dec '15

Dear all, First of all, sorry if this question has been asked several times already. I am currently trying to use sel4 & camkes on a debian stable. I installed all the dependencies but I am facing an error message when trying to build the tool (see below). My version of cabal is 1.20, so, version should not be an issue. After searching, it seemed that the version of ghc might be the root cause so I upgraded to testing and/or unstable but faced other issues then. My question is then what is the best development environment to use sel4 and camkes? Any special recommendation? I would like to keep my existing debian/stable as much as possible. Thanks for any help or suggestion, Julien. [parse-capDL] building... export CONFIG_CAPDL_LOADER_MAX_IRQS=256 && cabal configure && cabal build && cp dist/build/parse-capDL/parse-capDL . Resolving dependencies... cabal: The package 'capDL-tool' requires Cabal library version -any && >=1.18 but no suitable version is installed. Makefile:45: recipe for target 'parse-capDL' failed make[1]: *** [parse-capDL] Error 1 Makefile:49: recipe for target '/home/julien/tmp/camkes/stage/arm/imx31/parse-capDL/parse-capDL' failed make: *** [/home/julien/tmp/camkes/stage/arm/imx31/parse-capDL/parse-capDL] Error 2

3 3

domain problems
by ぷ风过无痕?? 23 Dec '15

23 Dec '15

Hi everyone, I'm running the RefOS project on arm kzm board. The config file is kzm_debug_defconfig. I am tring to set two domains in the RefOS by changing the CONFIG_NUM_DOMAIN parameter from 1 to 2 in this file and rebuilt RefOS. When running RefOS it gets stucked and some servers cannot be initialized.How to resolve this bug?

1 0

domain problems
by ぷ风过无痕?? 23 Dec '15

23 Dec '15

Hi everyone, I'm running the RefOS project on arm kzm board. The config file is kzm_debug_defconfig. I am tring to set two domains in the RefOS by changing the CONFIG_NUM_DOMAIN parameter from 1 to 2 in this file and rebuilt RefOS. When running RefOS it gets stucked and some servers cannot be initialized.How to resolve this bug? The full output information is in the adjunct file.

1 0

RTEMS working with seL4
by Hesham Almatary 15 Dec '15

15 Dec '15

Hi all, I got an RTEMS port working for RISC-V architecture along with seL4. This depends on my earlier seL4 port for RISC-V. RTEMS runs with support of seL4 microkernel, and it runs in Supervisor mode (on another core). seL4 application would allocate and map memory for it from its untyped memory (userspace), before off-loading it to another core. seL4 application that loads/runs RTEMS is pretty much the same as SOS. For more details (and instructions) about how to build/run the project, see the github repo of the port [1], and/or this blog post [2] [1] https://github.com/heshamelmatary/rtems-riscv [2] http://heshamelmatary.blogspot.co.uk/2015/12/rtems-port-for-risc-v-withwith… Cheers, -- Hesham

2 2

VSpace translation?
by Ben Karel 14 Dec '15

14 Dec '15

Would any of seL4's guarantees be compromised if a Translate method were added to page directory objects (for mapping a virtual address to the underlying physical address, without exposing the intermediate page capabilities)?

4 4

Capability resolution depth mismatches
by Ben Karel 14 Dec '15

14 Dec '15

Hi all, Some capability resolution, such as for fault handling, winds up calling resolveAddressBits with n_bits = wordBits, and any remaining bits are ignored. In other cases, such as the destination slot for seL4_CNode_Copy, the user provides a resolution depth parameter, and the call to resolveAddressBits is mediated by lookupSlotForCNodeOp, which fails with a depth mismatch if there are any bits remaining. Individually these seem like reasonable choices, but it leads to code like this: seL4_CNode cspace_root = ...; // freshly allocated 256-slot CNode with no guard seL4_CPtr slot_for_copy = 0x23; // arbitrary slot we know is available seL4_CPtr slot_for_tcb = slot_for_copy << 24; seL4_CNode_Copy(cspace_root , endpoint_for_copy, 8, ...); seL4_TCB_Configure(..., endpoint_for_tcb, ...); I found it surprising that two different CPtrs are needed to describe the same slot! Is there a conceptual-model-explanation that doesn't involve appeal to the underlying implementation? Also: my current understanding is that the depth parameter is only needed to disambiguate indirections through CNode-containing slots. What goes wrong if the depth mismatch checks are relaxed?

2 2

Timing side channel via idle thread code?
by Brian Mastenbrook 12 Dec '15

12 Dec '15

While pulling up the Haskell model to respond to the previous question, I noted the following statement: "The idle thread's code is at an arbitrary location in kernel memory. For convenience in the Haskell model, we place it in the globals frame, but there is no need for it to be in user-accessible memory." Given that the globals frame is mapped cacheable, doesn't this lead to a potential timing side channel? Tasks would be able to determine whether the idle thread's code has been evicted from cache, which may or may not reveal something interesting about the state of the system as a whole. -- Brian Mastenbrook CTO Wearable Inc. Makers of AirStash

3 2