from Hacker News

The Muen Separation Kernel

by englishm on 8/31/15, 12:28 PM with 21 comments

  • by Zuph on 8/31/15, 1:23 PM

    "The Muen Separation Kernel is the world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level."

    This doesn't really jibe with seL4's claim: "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement is now open source." http://sel4.com/

  • by nickpsecurity on 8/31/15, 7:01 PM

    It's interesting work. It's what my niche would call medium assurance software: a regular development approach that selectively uses higher-assurance tech or practices to produce stuff with fewer defects or risks. Aside from issues in x86 or security policy, the other big risks it will face are how it handles error states, how much apps can affect its internals with function calls (static helps), covert channels (esp timing), and what effect compiler has on it. I recall IRONSIDES was "provably immune" to single-packet DOS and correct W.R.T. specification thanks to SPARK... until a compiler bug decided differently. ;) Ada really needs a compiler like CompCert C or FLINT ML for safety/security use-case.

    Good news for people wanting to try it out is that it's been integrated into Genode OS per recent newsbite:

    http://genode.org/documentation/release-notes/15.08#Genode_o...

    They claim it's also ready for day-to-day albeit still early so problems will happen. Patient, early adopters and contributors are target audience. Have fun! :)

  • by minthd on 8/31/15, 12:35 PM

    This relies on Intel's Vt-d , but there are some issues with Vt-d :

    http://invisiblethingslab.com/resources/2011/Software%20Atta...

  • by amluto on 8/31/15, 3:57 PM

    x86 has some really weird ISA quirks that can lead to exceptions and, frequently, security holes. I wonder how good their ISA model is.

  • by vectorEQ on 8/31/15, 2:30 PM

    the site is marked as high risk >.> http://www.mcafee.com/threat-intelligence/domain/default.asp...

    just sayin' :) not trying to imply anythin'. apart from that my gateway doesn't let me on it :P

  • by j2kun on 8/31/15, 2:23 PM

    And here I thought this was going to be a new kernel for machine learning :)