Aw: Re: Re: Re: Re: seL4 is open source now
mark.neuhaus at email.de
mark.neuhaus at email.de
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 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 at lorquet.fr>
> An: mark.neuhaus at email.de
> Betreff: Re: Aw: Re: Re: Re: seL4 is open source now
> 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 at 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.
More information about the baseband-devel