[lugm.org] Fwd: [seL4] Hyperkernel paper

[Avinash Meetoo]

Hi,

I have not read the paper entirely but the kernel used is not a toy kernel
as far as I can see. Rather, it is a new kernel, inspired by Unix, but
which, because of the way it is built, has been formally verified to
contain no bug.

Is it a practical kernel capable of replacing existing kernels? Time will
tell.

Is formal verification something desirable? You bet, with our over reliance
on technology. But real kernels (e.g. Linux, XNU, NT kernel, etc.) have not
been built to satisfy the requirements of formal verification.

Interestingly, there is a kernel which is currently being developed by
Google called Fuchsia <https://en.wikipedia.org/wiki/Google_Fuchsia> which,
according to some rumours, will replace the Linux kernel in Android one
day. Will this happen? Only time will tell again :-)

*Dave Burke, Google's VP of Android engineering, told Android Police about
Fuchsia in May 2017: "Fuchsia is an early-stage experimental project. We,
you know, we actually have lots of cool early projects at Google. I think
what’s interesting here is its open source, so people can see it and
comment on it. Like lots of early-stage projects, it’s gonna probably pivot
and morph."*


The thing is that, all over the world, researchers are doing research!!!
Guess they are having a lot of fun too :-)

Avinash



On 24 January 2018 at 22:02, Jheengut Pritvi <z.coldplayer at gmail.com> wrote:

> Any thoughts for this toy  kernel!!
>
> ---------- Forwarded message ----------
> From: Jeff Waugh <jdub at bethesignal.org>
> Date: 23 January 2018 at 04:38
> Subject: [seL4] Hyperkernel paper
> To: devel at sel4.systems
>
>
> Hi seL4 friends,
>
> Any thoughts and/or feelings about the Hyperkernel paper from SOSP'17?
>
> > This paper describes an approach to designing, implementing, and
> formally verifying the functional correctness of an OS kernel, named
> Hyperkernel, with a high degree of proof automation and low proof burden.
>
>
> https://homes.cs.washington.edu/~helgi/papers/hyperkernel.pdf
>
> Thanks,
> Jeff
>
> _______________________________________________
> Devel mailing list
> Devel at sel4.systems
> https://sel4.systems/lists/listinfo/devel
>
> __________________________________________________________
> Linux User Group of Mauritius (LUGM) Discuss mailing list
> Website: http://lugm.org
> Mailing list archive: http://discuss.lugm.org/pipermail/discuss_discuss.
> lugm.org/
> Forum: http://lugm.org/forum/
> IRC: #linux.mu on Freenode
>



-- 
*Avinash Meetoo*
*Husband and dad in the Noulakaz family*


*LinkedIn <https://www.linkedin.com/in/avinashmeetoo> | Twitter
<https://twitter.com/AvinashMeetoo> | Facebook
<https://www.facebook.com/avinashmeetoo> | Google+
<https://plus.google.com/+AvinashMeetoo> | YouTube
<https://www.youtube.com/user/avinashmeetoo>*
37D Bernardin de St Pierre Avenue, 72350 Quatre-Bornes, Mauritius
Mobile : +230 5493-9394 <+23054939394>  |  Home : +230 424-5883
<+2304245883>
Email : avinash at noulakaz.net  |  Web : www.noulakaz.net
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://discuss.lugm.org/pipermail/discuss_discuss.lugm.org/attachments/20180126/e4fc0a17/attachment.html>