- Devel - lists.sel4.systems

Kernel extensions and userspace options
by Jonathan C Day 30 Aug '16

30 Aug '16

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.

3 6

Re: [seL4] Devel Digest, Vol 27, Issue 16 - High Assurance Hardware
by Tyga 30 Aug '16

30 Aug '16

> > 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.

2 1

IA32 syscall bindings
by Norman Feske 26 Aug '16

26 Aug '16

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

4 7

syscalls and tlb
by Vasily A. Sartakov 26 Aug '16

26 Aug '16

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

4 5

Does anyone pay attention to Google's new operating system fuchsia
by XilongPei 24 Aug '16

24 Aug '16

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

3 3

x86: loosing edge triggered interrupts when using I/O APIC
by Alexander Boettcher 24 Aug '16

24 Aug '16

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

2 1

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