Hacker News Reader

Comment by staticassertion | Hacker News Reader

I wouldn't use SEL4 as an argument. It is completely unreasonable to build a production kernel the way they did - it took them ages to get what they had. Google is probably looking to develop features/ move code a lot faster than is possible using their technique.

Good coding practices take no time to implement, you learn it once and you write that way. It is not bullet proof, neither are capabilities. Still, at least they're practical.

View on HN

I think you miss the point of a microkernel! The point is to keep all your "features" outside of it, and to use it only to implement the core set of functionality necessary to have secure shared access to the hardware. The general L4 concept has proven industry use, so there's no reason you can't take advantage of the already accomplished work on seL4 to bootstrap your own secure OS.

It's true that seL4 is not a magic safety or security bullet; in particular, their FAQ says that they haven't completed extending their proofs to DMA safety via VT-d or SystemMMU on ARM, so DMA-accessing services would have to be separately verified. And its particular feature set may not be appropriate for all situations. But if its API does work for you, it would be foolish not to at least consider using it.

It is really unreasonable to dismiss seL4 simply because it took them a lot of effort to create it. That effort is now done and can be re-used and magnified by further effort.

I didn't realize you were recommending to use sel4, I assumed you meant they should have proven theirs using similar methods.

How about Muen separation kernel in SPARK Ada with automated prover eliminating many classes of undefined behavior? Or C with tools like Frama-C and Astree Analyzer (like SPARK for C)? C++ can't reach the safety of its competition due to more complexity and less tooling.

I'm only commenting on seL4's approach not being very viable. I'm not advocating for C++ in the kernel either.

Fair enough.

To be fair, if Frama-C is an option, as someone on the C++ side of the fence (C vs C++) I would advocate High Integrity C++ is also an option. :)

http://www.ldra.com/en/software-quality-test-tools/group/by-...

I thought about it. The reason I left it off is a lack of static analysis, automatic generation of tests, certified compilers, etc. There's tons of FOSS and commercial vendors for doing such things in C with quite a bit for Ada. Whereas, I could find only one or two products for C++ that seemed like it would be really helpful as opposed to just kind of. So, I pivoted my recommendations to go with languages that have huge, tooling ecosystems in academic R&D and commercial. You can certainly use it but might get less value in long term.

Embedded, real-time Java could also be on the list since Java ecosystem has a verification tool for about everything. CompSci loves Java for some reason (probably mandated classes). Yet, verifiable C and SPARK are closer to the metal than embedded Java plus no Oracle risk. So, left off Java as well.

I guess so, I just know it from reading about it, so it might be that when using it won't be as suitable as I think it could be.

On the Java side you can probably check what Aonix used to do, they are now part of PTC.

http://www.ptc.com/developer-tools/perc

Also there are the guys from MicroEJ.

http://www.microej.com/products/device-software-development/...

There is no Oracle risk with Java, when companies play by the rules.

PTC, Aicas, IBM, MicroEJ, Excelcior JET, HP, Cisco, Ricoh, Azul, Red Hat and so many other companies are selling JDKs with their own set of features, without having had any issue with Sun or Oracle.

Only Google has an issue with Oracle, because they decided they were the cool kid better than anyone else whose rules don't apply to.

Reply on news.ycombinator.com