4 ms·

I am exceptionally sceptical that "specialised" and "secure" are anything but opposites. "One hundred novel implementations of /dev/random" is a security night

I am exceptionally sceptical that "specialised" and "secure" are anything but opposites. "One hundred novel implementations of /dev/random" is a security nightmare. What you want is one implementation of /dev/random that everybody uses. Like uh, Linux. Same goes for every other element of the kernel. A secure kernel does not come from using (I'm sorry to say) a hipster programming language, it comes from decades of abuse that is thrown at mainstream kernels.

mahyarm 11y ago
It wouldn't be 100 implementations of /dev/random, but one implementation per language. Security with a C / C++ based system that has to be everything to everyone is pretty much intractable. If you have a java unikernel server for example, you only have one programming language which you can understand from top to bottom with a lot of well written open source libraries. Then you have a hypervisor, from what I understand can be far simpler than the linux kernel, POSIX and everything else. You only have two smaller layers to understand, versus the huge unix ecosystem stack to understand. Also changing something inside your unikernel stack would be a git commit & deploy away. Patching a kernel vulnerability which you probably don't understand is a significantly longer undertaking.
- nickpsecurity 11y ago
  "Then you have a hypervisor, from what I understand can be far simpler than the linux kernel, POSIX and everything else. You only have two smaller layers to understand, versus the huge unix ecosystem stack to understand." That's exactly it. It's how it was done in old days for highly assured systems and it still applies. Side advantage is that anything you create that you control you can apply the best software and security engineering methods possible. So, the big messy OS might be hard to hit with static or covert channel analysis but your microkernel/hypervisor/VMM might do fine.
querulous 11y ago
unikernels are only single language now for convenience and research purposes. in the future you'll probably compile to something similar to the llvm ir and generate a unikernel from that. there'll probably be a standard /dev/random, a standard tcp stack, a standard http parser, etc
kasey_junk 11y ago
The point of something like Halvm, the Haskell unikernel, is that can bring to bear a lot of formal methods for proving the components are secure. This sort of thing is untenable in a general purpose OS, but for specialized use case it makes a lot of sense. Here (https://github.com/GaloisInc/haskell-tor https://github.com/GaloisInc/haskell-tor) for instance is a Tor implementation written for HalVM. The surface area for proving this implementation is secure is dramatically smaller than the more general purpose one. That it is more efficient about resources means that you can run more nodes, which in this particular case is very important. The author gave a talk at QCon last week, I can't seem to find video of it just now...
- nickpsecurity 11y ago
  You're right about where it's going on that but wrong about where it is. The reason is the compiler, state of FP security analysis, and overall TCB. So much to prove that's non-trivial and even non-obvious how before we can trust as secure the object code that started as your Haskell program linking to that. I advise safe constructions of simple imperative or functional languages until INFOSEC research in security verification catches up to things like Haskell. That's basically subsets of C, Java, Ada, ML, and LISP with certifying or hand-compilation. I'd love a certified Haskell runtime, though. Tolmach et al were making progress in that direction and might pick it back up eventually.

mahyarm 11y ago

It wouldn't be 100 implementations of /dev/random, but one implementation per language. Security with a C / C++ based system that has to be everything to everyone is pretty much intractable. If you have a java unikernel server for example, you only have one programming language which you can understand from top to bottom with a lot of well written open source libraries. Then you have a hypervisor, from what I understand can be far simpler than the linux kernel, POSIX and everything else. You only have two smaller layers to understand, versus the huge unix ecosystem stack to understand. Also changing something inside your unikernel stack would be a git commit & deploy away. Patching a kernel vulnerability which you probably don't understand is a significantly longer undertaking.

nickpsecurity 11y ago
"Then you have a hypervisor, from what I understand can be far simpler than the linux kernel, POSIX and everything else. You only have two smaller layers to understand, versus the huge unix ecosystem stack to understand." That's exactly it. It's how it was done in old days for highly assured systems and it still applies. Side advantage is that anything you create that you control you can apply the best software and security engineering methods possible. So, the big messy OS might be hard to hit with static or covert channel analysis but your microkernel/hypervisor/VMM might do fine.

querulous 11y ago

unikernels are only single language now for convenience and research purposes. in the future you'll probably compile to something similar to the llvm ir and generate a unikernel from that. there'll probably be a standard /dev/random, a standard tcp stack, a standard http parser, etc

kasey_junk 11y ago

The point of something like Halvm, the Haskell unikernel, is that can bring to bear a lot of formal methods for proving the components are secure. This sort of thing is untenable in a general purpose OS, but for specialized use case it makes a lot of sense. Here (https://github.com/GaloisInc/haskell-tor https://github.com/GaloisInc/haskell-tor) for instance is a Tor implementation written for HalVM. The surface area for proving this implementation is secure is dramatically smaller than the more general purpose one. That it is more efficient about resources means that you can run more nodes, which in this particular case is very important. The author gave a talk at QCon last week, I can't seem to find video of it just now...

nickpsecurity 11y ago
You're right about where it's going on that but wrong about where it is. The reason is the compiler, state of FP security analysis, and overall TCB. So much to prove that's non-trivial and even non-obvious how before we can trust as secure the object code that started as your Haskell program linking to that. I advise safe constructions of simple imperative or functional languages until INFOSEC research in security verification catches up to things like Haskell. That's basically subsets of C, Java, Ada, ML, and LISP with certifying or hand-compilation. I'd love a certified Haskell runtime, though. Tolmach et al were making progress in that direction and might pick it back up eventually.