Devel

devel@sel4.systems

9 participants
1391 discussions

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

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel