March 2015 - Devel - lists.sel4.systems

seL4 + Qubes OS Project
by WhonixQubes 21 Mar '15

21 Mar '15

Hello, I am the maintainer of the Qubes + Whonix project... https://www.whonix.org/wiki/Qubes Which is the port of Whonix OS (think a more secure Tor proxied VM) to Qubes OS, which has upstream integration into the Qubes codebase now. I am very interested in secure minimal kernels and hypervisors, and have been discussing these topics publicly and privately with other interested developers and investors recently. And I am also positioning to bring development resources to low-level projects that can achieve a more optimal (and verifiable) secure TCB than bloated Linux-based systems, as Qubes Dom0 is currently based upon. Actually being able to read through and know all the code that is running on a mission critical machine, a novel thought, huh. ;) I am most interested in this Qubes blurb on the seL4 website... https://sel4.systems/GettingStarted "Qubes is an open source operating system designed to provide strong security for desktop computing using virtualisation to provide isolation. Qubes is based on Xen. seL4 is a much better fit for Qubes. The project is to port Qubes to seL4 (or develop an alternative Qubes-like system for seL4)." I absolutely agree with this and would like to know more about what Qubes development project might already underway be in the seL4 community in order to consider the opportunity of providing some real assistance in the future. What's the status of this seL4 Qubes port project and who can I get in touch with to talk more about accomplishing it? Thanks! :) WhonixQubes

7 7

Emit debugging info
by Hesham ALMatary 19 Mar '15

19 Mar '15

Hi all, This is most likely a straight forward question: how can I get debugging symbols for the final image (if possible)? I am configuring/compiling seL4tests for example with "make kzm_simulation_debug_xml_defconfig", etc. And when I try to dump the generated "sel4test-driver-image-arm-imx31" content with "arm-none-eabi-objdump" command, I can't find any debugging symbols (function/variable names) although debugging flags are set. If the previous question is not valid, then how can I debug the generated image using QEMU/gdb if possible? and trace the program execution beginning from _start? Other solutions for debugging are appreciated. Thanks in advance. -- Hesham

2 2

About the latest commit of seL4 kernel
by Jensen Zhang 16 Mar '15

16 Mar '15

Hello, I found there are several little changes on the latest commit of seL4 kernel [1]. And you just changed the define of function "map_it_frame_cap" for arm, but not for ia32. I just wonder whether there are any further considerations, or it's just a mistake :) Thanks, [1] https://github.com/seL4/seL4/commit/4f12acd2703183c9f44fe097589b53eb53c599eb -- Jensen Zhang Tongji University

2 1

refos and sel4-test questions
by Tim Newsham 16 Mar '15

16 Mar '15

Is it possible to build and run sel4-test against the "experimental" kernel tree? if so, whats the process? On RefOS for my port, I'm seeing a weird problem with the timer code. It is mapping in the right phys addr for my timer device, and I can read the right ID register out, so it appears to be mapping the right memory, but the code to do a timer reset, which sets a reset bit then polls for the bit to return to zero, is getting stuck in an infinite loop. I verified that the loop isn't being altered by the compiler, and I verified that the same code runs fine in sel4 test. At this point I suspect one of two things 1) refos is allowing the mapping to happen with caching on (even though I asked it not to) or 2) something is wrong elsewhere with the "experimental" kernel (sel4-test is running on the "master" tree, and refos is using the kernel from the "experimental" tree). is there anything else I could be missing? any thoughts? -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

3 2

Porting seL4 to RISC-V
by Hesham ALMatary 15 Mar '15

15 Mar '15

Hi all, I'm Hesham ALMatary a computer science research student at the University of York. I am considering porting L4 microkernel variants to RISC-V [2] (for both my research and Google Summer of Code), and Fiasco.OC is one of these variants, but I want to extend the options here by asking about seL4. Is this project would be: first applicable, and second of interest to you? And if yes, would you offer some help (guidance)? I am sending this message as suggested here [1] that I should contact you if I'm willing to port seL4 to a new platform. [1] http://sel4.systems/GettingStarted/ [2] http://riscv.org/ Thanks, -- Hesham

4 4

seL4 on Raspberry Pi
by da Tyga 11 Mar '15

11 Mar '15

> > IMHO, the biggest problem with the Raspberry Pi is that most of its I/O > (even the NIC) is connected through USB. A serial port is available > (albeit without level shifters). So, running the seL4test should be > possible without a USB stack, but as soon as you want to access a > keyboard, network or filesystem, you'll need one. You should keep in mind that seL4 is a microkernel. So the USB stack and drivers that depend on that stack should all be implemented as processes/tasks running on top of seL4. I know it is not cool to mention Minix here, but it and Plan9 suggest ideas as to how the layers above seL4 could be structured. As far as I can understand, seL4 is not an operating system, it is a microkernel upon which one or more operating systems could be built. The key reason to use seL4 would be due to it providing capabilities based isolation between the layers that run on top of it and thus preventing rogue processes from interfering with other processes.

3 2

A port to the Raspberry Pi 2?
by Sebastian Lau 10 Mar '15

10 Mar '15

Would a port of seL4 to the raspberry pi 2 be welcome because I'm interested in buying a raspberry pi 2 and building sel4 for it?

5 9

docker compatible? (was Re: MySQL - seL4)
by Raoul Duke 07 Mar '15

07 Mar '15

> wouldn't provide you much. What sel4 could buy > you is isolation between mysql and other applications > if you chose to run several processes on the same > machine. The processes themselves, including mysql, > would still be vulnerable to any internal vulnerabilities > they might have (sel4 is not a magic bullet). There's a lot of noise around Docker. I find it annoying for many reasons, including security -- although I do understand some of the attraction. It would be super keen in my mind if seL4 could offer something in that vein, could present itself as a nice alternative.

5 6

MySQL - seL4
by André Bispo 06 Mar '15

06 Mar '15

Hello guys,Do you think it is feasible to have MySQL running on top of seL4 and take advantage of the isolation mechanisms?I was looking into the microkernel, the CamKES project and the mailinglist, to find some answers but i think it would be very difficult, if not impossible to run MySQL on seL4.I'm trying to explore this possibility and i want to know your opinion before continue. Best regards,André Bispo.

3 2

USB booting problem
by André Bispo 05 Mar '15

05 Mar '15

Hello guys, i'm building myself a system for my thesis and i'm currently testing out the seL4.I was trying to boot the sel4test by USB following the tutorial described in another question on this mailing list.But syslinux seems to load the kernel and the test but nothing appears afterwards.This is the message shown: MBRLoading sel4kernel... okLoading rootserver... ok _ If anyone could help me out i'd be very grateful. Best regards,André Bispo.

3 3