5 Aug
2014
5 Aug
'14
11:17 a.m.
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(a)lorquet.fr>
An: mark.neuhaus(a)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(a)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.