Progress of bringing Genode to seL4
Hello, I have written up the first of a series of articles about using seL4 as base platform for the Genode OS framework: http://genode.org/documentation/articles/sel4_part_1 I hope that it contains useful bits of information for novices of seL4 and Genode alike. Even though the article outlines a few hurdles, the overall experience of using the kernel had been overly positive so far. For those of you interested in tracking the progress of the ongoing work, here is the corresponding topic branch: https://github.com/nfeske/genode/commits/sel4 Cheers 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
Hello, I went a bit further with bringing seL4 and Genode together. The following article describes a series of small experiments with the kernel's IPC mechanism and the management of virtual memory. http://genode.org/documentation/articles/sel4_part_2 The steps described in the article can be reproduced via my corresponding topic branch, which I have just rebased on top of Genode's master branch: https://github.com/nfeske/genode/commits/sel4 Cheers Norman On 10/30/2014 01:26 PM, Norman Feske wrote:
-- 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
Your article says: "Second, the mapping database keeps records about how mappings got established. Thereby, the memory required for storing this information in the kernel depends on the behaviour of the user land. As a consequence, a malicious user-level program is able to provoke a high consumption of kernel memory by establishing mappings. Eventually, this represents an attack vector for denial-of-service attacks onto the kernel." Is this right? I thought that the callers have to provide the resources that get consumed by the kernel to perform system calls. Is this not the case in this situation? On Tue, Mar 10, 2015 at 2:20 AM, Norman Feske <norman.feske@genode-labs.com> wrote:
-- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com
"Is this right? I thought that the callers have to provide the resources that get consumed by the kernel to perform system calls. Is this not the case in this situation?" ahh, you answered this later in the article.. I should have finished reading before asking the question :) On Tue, Mar 10, 2015 at 7:02 AM, Tim Newsham <tim.newsham@gmail.com> wrote:
-- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com
Tim already found it, but just for those on the list who haven’t read the article: this paragraph is about how traditional L4 kernels did this, as opposed to seL4, which doesn’t have the problem (nor a mapping database). Cheers, Gerwin
________________________________ 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.
On 11/03/15 04:02, Tim Newsham wrote:
As Gerwin says, this paragraph applies to traditional L4 kernels, not seL4. Indeed, it would not only allow denial-of-service attacks, but also trivial covert storage channels that make it impossible for the kernel to enforce confidentiality. seL4's proof of confidentiality (information flow enforcement) rules out such channels [1], and would have been a lot more difficult without seL4's memory management model that deviates from traditional L4. Note that recently work on Fiasco.OC has demonstrated how to exploit these kinds of covert channels to break confidentiality [2], so this is by no means just an academic curiosity. Cheers Toby [1] https://www.nicta.com.au/pub-download/full/6464/ [2] https://eprint.iacr.org/2014/984.pdf ________________________________ 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.
Hello, my work on bringing Genode to seL4 has reached a point where simple Genode system scenarios can be executed on the seL4 kernel. The development steps and the rationale behind the taken design decisions are documented in the following article: http://genode.org/documentation/articles/sel4_part_3 The individual steps can be examined as separate commits on my topic branch cited in my previous email. Even though the current version is still at a proof-of-concept stage, we plan to feature it in the upcoming Genode release 15.05. Cheers Norman On 03/10/2015 01:20 PM, Norman Feske wrote:
-- 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
Hello, following-up my last posting, Genode 15.05 was released earlier today. As promised, it comes with principle support for seL4. A quick summary of the current release: - Comprehensive architectural documentation - Feature completion of the our custom kernel - Kernel-protected capabilities - Principal support for the 64-bit x86 - Dynamic thread weights - Revised device-driver infrastructure - Device drivers - New AHCI driver - Multi-touch support - Audio drivers ported from OpenBSD - SD-card drivers for i.MX53 and Raspberry Pi - Board support for i.MX6-based Wandboard - Support for GPT partitions - Proof-of-concept support for the seL4 kernel - NOVA kernel mechanism for signals - Tool chain updated to GCC 4.9.2 and binutils 2.25 Besides seL4 support, the most prominent addition is a completely new documentation in the form of the book "Genode Foundations": http://genode.org/documentation/genode-foundations-15-05.pdf These and many more topics of the release are covered in the release documentation: http://genode.org/documentation/release-notes/15.05 Best regards Norman On 05/18/2015 04:06 PM, Norman Feske wrote:
-- 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
participants (4)
-
Gerwin Klein -
Norman Feske -
Tim Newsham -
Toby Murray