<div dir="ltr">Hi,<div><br></div><div>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.</div><div><br></div><div>Is it a practical kernel capable of replacing existing kernels? Time will tell.</div><div><br></div><div>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.</div><div><br></div><div>Interestingly, there is a kernel which is currently being developed by Google called <a href="https://en.wikipedia.org/wiki/Google_Fuchsia">Fuchsia</a> which, according to some rumours, will replace the Linux kernel in Android one day. Will this happen? Only time will tell again :-)</div><div><br></div><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div><i>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."</i></div></blockquote><div><br></div><div>The thing is that, all over the world, researchers are doing research!!! Guess they are having a lot of fun too :-)</div><div><br></div><div>Avinash</div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 24 January 2018 at 22:02, Jheengut Pritvi <span dir="ltr"><<a href="mailto:z.coldplayer@gmail.com" target="_blank">z.coldplayer@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Any thoughts for this toy kernel!!<br>
<br>
---------- Forwarded message ----------<br>
From: Jeff Waugh <<a href="mailto:jdub@bethesignal.org">jdub@bethesignal.org</a>><br>
Date: 23 January 2018 at 04:38<br>
Subject: [seL4] Hyperkernel paper<br>
To: devel@sel4.systems<br>
<br>
<br>
Hi seL4 friends,<br>
<br>
Any thoughts and/or feelings about the Hyperkernel paper from SOSP'17?<br>
<br>
> 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.<br>
<br>
<br>
<a href="https://homes.cs.washington.edu/~helgi/papers/hyperkernel.pdf" rel="noreferrer" target="_blank">https://homes.cs.washington.<wbr>edu/~helgi/papers/hyperkernel.<wbr>pdf</a><br>
<br>
Thanks,<br>
Jeff<br>
<br>
______________________________<wbr>_________________<br>
Devel mailing list<br>
Devel@sel4.systems<br>
<a href="https://sel4.systems/lists/listinfo/devel" rel="noreferrer" target="_blank">https://sel4.systems/lists/<wbr>listinfo/devel</a><br>
<br>
______________________________<wbr>____________________________<br>
Linux User Group of Mauritius (LUGM) Discuss mailing list<br>
Website: <a href="http://lugm.org" rel="noreferrer" target="_blank">http://lugm.org</a><br>
Mailing list archive: <a href="http://discuss.lugm.org/pipermail/discuss_discuss.lugm.org/" rel="noreferrer" target="_blank">http://discuss.lugm.org/<wbr>pipermail/discuss_discuss.<wbr>lugm.org/</a><br>
Forum: <a href="http://lugm.org/forum/" rel="noreferrer" target="_blank">http://lugm.org/forum/</a><br>
IRC: #<a href="http://linux.mu" rel="noreferrer" target="_blank">linux.mu</a> on Freenode<br>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr" style="font-size:12.8px"><div dir="ltr" style="font-size:12.8px"><div dir="ltr" style="font-size:12.8px"><div dir="ltr" style="font-size:12.8px"><div dir="ltr" style="font-size:12.8px"><font size="2" style="font-family:arial,helvetica,sans-serif"><font size="4"><b>Avinash Meetoo</b></font><b><br></b><b>Husband and dad in the Noulakaz family</b></font></div><div dir="ltr" style="font-size:12.8px"><font face="arial, helvetica, sans-serif" size="2"><b><br></b></font></div><div dir="ltr" style="font-size:12.8px"><font face="arial, helvetica, sans-serif" size="2"><b><a href="https://www.linkedin.com/in/avinashmeetoo" target="_blank">LinkedIn</a> | <a href="https://twitter.com/AvinashMeetoo" target="_blank">Twitter</a> | <a href="https://www.facebook.com/avinashmeetoo" target="_blank">Facebook</a> | <a href="https://plus.google.com/+AvinashMeetoo" target="_blank">Google+</a> | <a href="https://www.youtube.com/user/avinashmeetoo" target="_blank">YouTube</a><br></b></font><br style="font-size:12.8px"><div><font face="arial, helvetica, sans-serif">37D Bernardin de St Pierre Avenue, 72350 Quatre-Bornes, Mauritius</font></div><div dir="ltr"><font face="arial, helvetica, sans-serif">Mobile : <a href="tel:+23054939394" target="_blank">+230 5493-9394</a> | Home : <a href="tel:+2304245883" target="_blank">+230 424-5883</a></font></div><div dir="ltr"><font face="arial, helvetica, sans-serif">Email : <a href="mailto:avinash@noulakaz.net" target="_blank">avinash@noulakaz.net</a> | Web : <a href="http://www.noulakaz.net/" target="_blank">www.noulakaz.net</a></font></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
</div>