- Devel - lists.sel4.systems

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