The kernel comes with a hypervisor (under BSD on Githu, too) and you can run Linux in one virtual environment (see http://l4linux.org/) 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@lorquet.fr An: mark.neuhaus@email.de Betreff: Re: Aw: Re: Re: Re: seL4 is open source now

Hello,

Reading through the se4l FAQ at http://sel4.systems/FAQ/ , 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@email.de 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.