3 ms·

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 Anal

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.

staticassertion 10y ago
I'm only commenting on seL4's approach not being very viable. I'm not advocating for C++ in the kernel either.
- nickpsecurity 10y ago
  Fair enough.
pjmlp 10y ago
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-coding-standard/high-integrity-c http://www.ldra.com/en/software-quality-test-tools/group/by-...
- nickpsecurity 10y ago
  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.
  - pjmlp 10y ago
    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 http://www.ptc.com/developer-tools/perc Also there are the guys from MicroEJ. http://www.microej.com/products/device-software-development/microej-os/ 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.

staticassertion 10y ago

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

nickpsecurity 10y ago
Fair enough.

pjmlp 10y ago

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-coding-standard/high-integrity-c http://www.ldra.com/en/software-quality-test-tools/group/by-...

nickpsecurity 10y ago
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.
- pjmlp 10y ago
  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 http://www.ptc.com/developer-tools/perc Also there are the guys from MicroEJ. http://www.microej.com/products/device-software-development/microej-os/ 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.