Hello,
we are proud to announce that the just released version 16.08 of the
Genode OS Framework brings vastly extended seL4 support, which allows
interactive and dynamic system scenarios to run directly on the x86
version of the seL4 kernel. With the new version, users of seL4 can
compose dynamic operating systems from a plethora of ready-to-use Genode
components.
First, there are our time-tested device drivers and protocol stacks:
- VESA driver (based on x86emu of XOrg)
- Intel graphics driver (based on Linux 4.4.3), e.g., to drive external
connectors
- Intel wireless stack (based on Linux 4.4.3) including WPA supplicant
- Network driver (based on iPXE)
- AHCI, PS/2, PIT, ACPI driver
- Audio driver (ported from OpenBSD 5.9)
- USB driver (based on Linux 4.4.3) with hot-plug support
- lwIP - light weight TCP/IP stack
- Linux TCP/IP Stack (ported from Linux 4.4.3)
- File-system support, e.g., ext2 based on Rump kernels
Also, Genode includes a range of low-complexity resource multiplexers:
- Secure GUI multiplexer - Nitpicker
- Highly configurable and dynamical window manager
- Audio mixer
- Virtual networking components
- Virtual file-system support
For application development, there are several runtime environments and
high-level libraries:
- Noux - UNIX-like subsystem to run command-line-based GNU software
like bash, vim, coreutils, gcc/g++, ...
- Environments for the Rust, Python, and Lua programming languages
- Base libraries like libc, standard C++ library, pthreads, OpenSSL,
Readline etc.
- Qt5 libraries and applications, including Webkit
There's a lot more to explore and - in the pure microkernel way - each
of these components are executed in user mode as separate protection
domains on seL4.
More details about version 16.08 can be found in the extensive release
documentation:
https://genode.org/documentation/release-notes/16.08
and, for the impatient, a life demo scenario of Genode on seL4 can be
downloaded:
https://www.genode.org/documentation/release-notes/16.08#Try_Genode_seL4_at…
Best regards,
--
Alexander Boettcher
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
Hi,
I am very interested in SEL4, partly because I was assured it was impossible to use Formal Methods in kernel development, partly because it's a fascinating project in its own right, but right now because there are some embedded applications that could do with the high level of reliability and security that provable correctness implies.
Unfortunately, said applications need a comprehensive network stack and a powerful packet filtering/mangling engine.
The latter could imaginably be done in the kernel, as it's deterministic, but I don't see any obvious value. Nonetheless, if someone has coded such a system as a third-party add-on, I would be very interested.
There are good arguments for why the former can't be done, in a way that can be proven, and I really want the correctness.
In terms of userspace, I believe I could use something like L4Linux (as long as it is still maintained), and I think there's one supplied, but are there other options? Has anyone ported OpenBSD to it?
To be honest, I'm not sure I need a multitasking userspace, but I do absolutely need the network stack and packet filter. Everything else can be ported, albeit with difficulty. However, network operating systems are thin on the ground and tend to be proprietary, exactly what I don't want.
For those curious, I'm looking to end up with a system with strong bounds on robustness and security, and that can handle things like multipath TCP, network failover, QoS and OpenFlow. However, all of these requirements boil down to a sequential process. Unnecessary complexity is where you end up with problems.
If current wisdom says that there's nothing suitable in userspace, then does anyone know if there are there any existing Coloured Petri Nets that I could use to build what I need into the kernel? Even if I can't get better than a quasi-guarantee, it would be something.
>
> Re:
>
> ------------------------------
> Date: Mon, 29 Aug 2016 23:01:45 +0000
> From: <Gernot.Heiser(a)data61.csiro.au>
> <snip>
> You may *think* that the manufacturers don?t make changes to the more
> conventional bits of the hardware, and thus they are ?correct", but that
> isn?t true, of course. And on top of that we know that there are
> intentional backdoors in commercial hardware.
> The only way around this is high-assurance hardware, and this doesn?t come
> at an affordable cost.
>
> I think it?s an illusion to think one can partition hardware into trusted
> and untrusted bits. In the end, the OS is at the mercy of the hardware, if
> it?s faulty then you lose, there?s no way around it.
A key attraction of seL4 is the trustworthiness of the microkernel.
Running it on hardware with known bugs or features (e.g. recent Intel CPUs)
that compromise the kernel's trustworthiness counteracts the perceived
advantages.
Perhaps, it would be possible to list CPUs (and possibly boards) that are
recognised for being free of known potential attack vectors.
I would certainly not want to invest time and effort into making seL4 run
on hardware that could have be reasonably known to be of low assurance.
Dear seL4 developers,
first, I'd like to thank you for publishing seL4 under GPL. I am very
happy that I can finally get my hands dirty with working with the kernel
of your group. :-) Currently, I am taking the first baby steps to bring
the Genode OS framework (http://genode.org) to seL4. For reference, I am
using the experimental branch.
The first smallish issue I stumbled upon stems from the fact that Genode
is written in C++. By compiling the seL4 syscall bindings with a C++
compiler, I got the following error:
error: inconsistent operand constraints in an ‘asm’
It can be reproduced by putting the following code snippet into a cc
file and compiling it with 'g++ -m32 -c' (tested with the Genode tool
chain as well as with GCC 4.8.1):
typedef enum {
seL4_SysDebugPutChar = -9,
_enum_pad_seL4_Syscall_ID = (1U << ((sizeof(int)*8) - 1))
} seL4_Syscall_ID;
void
seL4_DebugPutChar(char c)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysDebugPutChar),
"b" (c)
: "%ecx", "%edx", "%esi", "%edi", "memory"
);
}
When compiling the same code snippet with 'gcc' instead of 'g++',
everything is fine. It turns out that the C++ compiler does not like the
enum value to be specified as input argument. I found the following ways
to circumvent this problem:
* Changing the enum value 'SysDebugPutChar' to a positive value,
* Removing the definition of '_enum_pad_seL4_Syscall_ID',
* Casting 'seL4_SysDebugPutChar' to an integer:
: "a" ((int)seL4_SysDebugPutChar),
In any case, I seem to have to change the bindings. Do you see a way
around it? If not, would you consider one of the solutions above for the
seL4 headers?
On another note, I noticed that the bindings use the EBX register.
Unfortunately, this makes it impossible to compile seL4 userland
software as position-independent code (PIC). E.g., when compiling the
above code snippet via 'g++ -m32 -fPIC -c', the following error occurs:
error: inconsistent operand constraints in an ‘asm’
However, PIC is required in order to use shared libraries. The solution
would be to not use EBX to pass arguments to the 'asm' statements, save
EBX on the stack prior moving the respective kernel argument to the
register, and, of course, restoring it after sysenter returns.
Before I start changing the bindings, I'd like to know: is there anyone
else working on the same problem? Would you be open to accept a change
of the bindings to become PIC compliant on the costs of a few added
instructions? Or do you have another suggestion how I should go about it?
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
Greetings.
I am working on MIPS port of seL4. Now I can run very simple hello world application which reads and dumps bootinfo page. In other words, I modified elfloader, added platform and architecture support to the kernel, add _sel4_start for mips in libsel4platsupport, adopted mips support of libmuslc to work with __sysinfo in mips and more. Now I have some questions.
I see that for different ‘syscalls' muslc uses different routes but with the same end. For example, SYS_ioctl from __stdout_write uses __syscall, provided by libmuslc/arch/<arch>/syscall_arch.h (implemented as CALL_SYSINFO). In the same time, syscall_cp function from __stdio_write is implemented inside libmuslc/src/internal/<arch>/syscall.s which uses __sysinfo in turn. So, that question is why?
The second question is about the kernel. Now I am using static configuration of TLB in kerne: I have one region for rootserver aligned to 2MB, and one region for boot info page (also aligned). Thus, I do not have tlb traps since everything is in the TLB. In future, of course, I should add a processing of TLB misses somewhere in the plat/arch part of kernel. I am not familiar with memory support in seL4 yet, is there any syscall for delivery tlb traps? (I see nothing similar) Is there any check inside, for example, SEND call, about a presence of page in TLB?
thank you.
--
Vasily A. Sartakov
sartakov(a)ksyslabs.org
Hi,
Google has announced a new operating system fuchsia, https://github.com/fuchsia-mirror Its kernel is called Magenta, Magenta has a capability-based security model, this is very similar to seL4.
Does anyone pay attention to Google's new operating system fuchsia?
Xilong Pei
Tongji University
Shanghai, China
2016/8/24
Hi,
we are using as user level timer driver the PIT on Genode/seL4 and
experience situations that the driver does not get IRQs after a while.
It happens on Qemu as also on native x86 hardware.
We tracked down the problem to the masking of edge-triggered IRQs on the
I/O APIC in the seL4 kernel. According to Intel, [0] chapter 3.2.4
"Interrupt Mask R/W", edge interrupts on a masked interrupt pin gets
ignored and are not held pending. On [2] there are also some discussion
about this topic too.
We solved/workaround the issue by this patch [1]. I looked additionally
into two other microkernels using the I/O APIC and they don't mask edge
level triggered I/O APIC interrupts. I wonder if anybody already
stumbled about the issue on seL4/x86? If not, please take the patch or
give advices to adapt the patch so that it may get upstream.
Thanks,
Alexander Boettcher.
[0] http://www.intel.com/design/chipsets/datashts/29056601.pdf
[1]
https://github.com/genodelabs/genode/blob/master/repos/base-sel4/patches/io…
[2] http://yarchive.net/comp/linux/edge_triggered_interrupts.html
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
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
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