Aw: Re: Re: Re: Re: seL4 is open source now

mark.neuhaus at mark.neuhaus at
Tue Aug 5 09:17:21 UTC 2014

The kernel comes with a hypervisor (under BSD on Githu, too) 
and you can run Linux in one virtual environment 
(see and for example an GSM stack in 
another virtual environment. So you can think of that kernel
as a kind of virtual machine that seperates the hardware  

This way all virtual systems are prooven separated and I think 
that is what the merkel-phone does.

owever NICTA is actually going much further. Thei are working 
on a zero-bug (verified file system) and much more.

This kind of programming is entirely different from common
way to write a program. (YOU don't write the program, but you
write a proof in Coq or ISABEL ect and from this proof a 
programm can be derived automatically)  


> Gesendet: Dienstag, 05. August 2014 um 10:50 Uhr
> Von: "Sebastien Lorquet" <sebastien at>
> An: mark.neuhaus at
> Betreff: Re: Aw: Re:  Re:  Re: seL4 is open source now
> Hello,
> Reading through the se4l FAQ at , I'm reading this:
> Unique about seL4 is its unprecedented degree of assurance, achieved through
> formal verification. Specifically, the ARM version of seL4 is the first (and
> still only) general-purpose OS kernel with a full code-level functional
> correctness proof, meaning a mathematical proof that the implementation (written
> in C) adheres to its specification. In short, the implementation is proved to be
> bug-free (see below). This also implies a number of other properties, such as
> freedom from buffer overflows, null pointer exceptions, use-after-free, etc.
> Okay with that. But also:
> There is a further proof that the binary code which executes on the hardware is
> a correct translation of the C code. This means that the compiler does not have
> to be trusted, and extends the functional correctness property to the binary.
> So that is very cool, even the binary result is proved, not only the source code !
> The only thing that bothers me is: what can I do with this cool software? It
> seems that little can be done without a set of userspace servers, so I guess we
> have to wait until some open source community provides useful software to run
> with this microkernel.
> Best regards,
> Sébastien Lorquet
> Le 02/08/2014 12:49, mark.neuhaus at a écrit :
> > 
> >> My idea is that at some point, the developers working at xda-developers
> >> (android phone hackers) will get enough knowledge of their baseband
> >> chips so that something can be done with osmocom. But this is only my
> >> opinion!
> > 
> > Yes lets hope. The calypso is just to outdated to be interesting
> > for anything 'useable' beyond pure hacking-fun.
> > 

More information about the baseband-devel mailing list