[hga]

As I was told in a HN discussion that non-educational "for GPL" version doesn't supply the same runtime, and the run time supplied is not very good. Maybe it's OK, but with all those restrictions and limitations it just didn't sound like an ecosystem I want to mess with. Plus I prefer to be able to develop and release software with less restrictive open source licenses.

WRT seL4 vs. Muen, I wouldn't be surprised if seL4 does less for you, it's only 9,000 lines of C code, and some of it is artifacts from the manual Haskell -> C translation.

[nickpsecurity]

Ahhhhhh. Wasn't aware of that. Will have to check with them. Muen uses the zero-runtime profile. Not sure about IRONSIDES. Far as those using a runtime, if that's the case, I'd recommend some FOSS people create an alternative one that is good. Then they get the language, toolset, etc benefits without that issue. Recreating those will be much more difficult.

"WRT seL4 vs. Muen, I wouldn't be surprised if seL4 does less for you, it's only 9,000 lines of C code, and some of it is artifacts from the manual Haskell -> C translation."

That's not what I meant. seL4 is a separation kernel: they're supposed to do almost nothing. The thing is that once a modification occurs, it can invalidate the whole security claim. So, the person modifying it needs to be able to correctly use whatever its assurance depended on. That will be much easier for Muen given a domain expert only needs to learn Ada/SPARK vs all that went into seL4.

Now, Muen certainly has less assurance in that it doesn't have formal models of design, security policy, etc. Most FOSS types won't do all that, though. So, just requiring a language that knocks out errors and maybe learning Design-by-Contract is a nice alternative that might get more people involved. That it's Ada... might get less people involved. Who knows. (shrugs)