- Devel - lists.sel4.systems

Cannot run on more than 1 domian?
by Kun Cheng 26 Mar '15

26 Mar '15

Hey guys, It seems that sel4test can only run on 1 domian (with CONFIG_NUM_DOMAINS=1 in .config), I tried to set it to 4 or a larger one (<=16) but when I ran the image with qemu it gave me an error "seL4 failed assertion '_ndks_end - _ndks_start <= NDKS_SIZE' at /home/kenneth/sel4/sel4current/kernel/src/arch/ia32/kernel/boot_sys.c:447 in function try_boot_sys". Is there any other configurations or code that I have to change? PS: I've been suffering a problem that I can only receive devel digests recently but none of your emails could reach me. This is weird because I set no filter in gmail. Best regards, Kun Cheng

1 0

Getting Started
by Fred 24 Mar '15

24 Mar '15

>From the main page. "If you would like to learn how to build a system on seL4, you might want to follow the lectures and especially the seL4-based project of UNSW's Advanced Operating Systems course <http://cs9242.web.cse.unsw.edu.au/>." Request: Is it possible to obtain access to the recorded lectures as well as the notes? Also assignment templates appear to be only available to enrolled students. I understand that publicly posting solutions to the assignments may be a problem. e.g. git clone ssh:// YOURLOGIN@login.cse.unsw.edu.au//home/cs9242/public_html/current/project/files/aos-2014 Background: Our project is in the internally funded phase of an open-source platform for medical simulation and training (similar to SimMan). The system consists of intercommunicating modules where each module runs a minimal OS. Thanks

4 5

beagle bone docs on page?
by Tim Newsham 21 Mar '15

21 Mar '15

Now that sel4, sel4test and refos work on beaglebone, perhaps it could be mentioned on the sel4 web page? If there's anything I can do to help make that happen, please let me know. Tim

2 1

seL4 + Qubes OS Project
by WhonixQubes 20 Mar '15

20 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 18 Mar '15

18 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 15 Mar '15

15 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 15 Mar '15

15 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 14 Mar '15

14 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 10 Mar '15

10 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