- Devel - lists.sel4.systems

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

am335x - configs and refos
by Tim Newsham 04 Mar '15

04 Mar '15

Attached are some patches for am335x support. I've started to play with refos, and can build it for am335x and run some of the startup (with release mode) but it hangs at some point.. still a work in progress. Also there's a few minor proofread tweaks on the refos doc. By the way, sel4test runs pretty well now in debug and release modes. Instructions are pretty straightforward: - build the project using the debug or release config - use objcopy to extract a raw binary from the ELF image - load the binary with uboot (I use "tftp", it defaults to the proper load address) - run it in uboot with "go 82000000" Tim

2 1

Joint a formally verified C compiler with seL4?
by Grissiom 02 Mar '15

02 Mar '15

Hi all, I've heard a formally verified optimizing C compiler: CompCert recently: http://www.absint.com/compcert/ HN: https://news.ycombinator.com/item?id=9130934 . So what benefit will there be if some one use CompCert as the compiler for seL4? -- Cheers, Grissiom

3 2

Re: [seL4] How are capabilities assigned
by Sebastian Lau 02 Mar '15

02 Mar '15

Hi, sorry if this sounds stupid but are address spaces and threads directly managed by the kernel as in are they allocated and identified by the kernel or is there another that helps the kernel?

2 2