6 ms·
I've been waiting for this to be released. I suppose everyone has been. Capabilities. Like fine grain locks, these are very powerful and very hard to get right
by CalChris 10y ago
I've been waiting for this to be released. I suppose everyone has been.
Capabilities. Like fine grain locks, these are very powerful and very hard to get right. That's the lesson from Hydra, the 432, .... No, it's not a hard mechanism for the microkernel to get right; it's a hard policy for the application programmer to get right. However, that's probably more of an opportunity rather than meant as a criticism. Our tools are massively more evolved than they were in the 70s. It'll be interesting to see what happens with capabilities.
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.
Provably secure. They did this with the SEL4 microkernel so this is a doable thing. If they're going to hang their hat on security (capabilities, microkernel, ...) there's no excuse for not having done this already and delivered a provably secure microkernel out of the box.
- 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 agoShared_ptr is slow. It has an atomic variable for reference counter - it is supposed to be thread safe...
- CalChris 10y agoYes, 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 agoI 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 agoHow 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 agoI'm only commenting on seL4's approach not being very viable. I'm not advocating for C++ in the kernel either.
- nickpsecurity 10y ago
- int_handler 10y agoTo be fair, this is not the entirety of C++ but C++ following the Google C++ Style Guide, which limits use to a more manageable subset of the language. For instance, exceptions, which can be especially hairy in a language with manual memory management, is prohibited. Take a look at the Fuchsia codebase. The code is really quite clean and readable.
- throwayedidqo 10y agoRandom muse, but God damn I love Google's code quality. Compared to the midnight bamboo forest my company built. A challenging codebase, not by its merits but because you need to be clever just to find your way through. Anyone know if Google is hiring webforms developers?
- andrewflnr 10y agoWhy do you want to implement something small with something that is large? Consider the size and amount of equipment involved in making watches. Or microchips, for that matter.
- paulddraper 10y agoDo you carry that watch-making equipment on your wrist along with your watch?
- andrewflnr 10y agoOf course not. I only need them in my workshop/foundry/dev machine.