4 ms·

>C++. Oh lord. Why are you writing a microkernel in C++? If there was anything they learned from L4 (Xen, Linux, ...) it is that C is sufficient. Why do you wan

by pikzen 10y ago

>C++. Oh lord. Why are you writing a microkernel in C++? If there was anything they learned from L4 (Xen, Linux, ...) it is that C is sufficient. Why do you want to implement something small with something that is large? This one is a real head scratcher. Because if there was anything proven from years and years of using C, it's that it is woefully insecure and should not be trusted to write a kernel with. You can still fuck up with C++, sure, but std::shared_ptr offers more guarantees than *. EDIT: HN stop eating my stars

ndesaulniers 10y ago
"folks it's ok, we're using shared_ptr's. We're safe. Problem solved."
- MichaelMoser123 10y ago
  Shared_ptr is slow. It has an atomic variable for reference counter - it is supposed to be thread safe...
CalChris 10y ago
Yes, we know that C is not secure. We also know that C++ is not secure and moreover it definitely isn't C, now with security. It's just more bigger C. So use your phrase, you can still fuck up with C++. You can just do it in more clever and insidious ways. seL4, a third-generation microkernel is 8,700 lines of C code and 600 lines of assembler. http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.... So we also empirically know that you can formally verify a microkernel written in C. Now if the Fuchsia folks had gone ahead and formally verified their microkernel, this issue would be moot. But they haven't. So we are instead left with std::shared_ptr offers more guarantees than *. While this isn't nothing, it isn't much either.
- staticassertion 10y ago
  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.
  - nickpsecurity 10y ago
    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.

by pikzen 10y ago

ndesaulniers 10y ago

"folks it's ok, we're using shared_ptr's. We're safe. Problem solved."

MichaelMoser123 10y ago
Shared_ptr is slow. It has an atomic variable for reference counter - it is supposed to be thread safe...

CalChris 10y ago

Yes, we know that C is not secure. We also know that C++ is not secure and moreover it definitely isn't C, now with security. It's just more bigger C. So use your phrase, you can still fuck up with C++. You can just do it in more clever and insidious ways. seL4, a third-generation microkernel is 8,700 lines of C code and 600 lines of assembler. http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.... So we also empirically know that you can formally verify a microkernel written in C. Now if the Fuchsia folks had gone ahead and formally verified their microkernel, this issue would be moot. But they haven't. So we are instead left with std::shared_ptr offers more guarantees than *. While this isn't nothing, it isn't much either.

staticassertion 10y ago
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.
- nickpsecurity 10y ago
  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.