5 ms·

They also have http://sel4.com http://sel4.com -- why wouldn't they use the .com as the canonical site instead of a more obscure .systems? (I say this because

by amirmc 11y ago

They also have http://sel4.com http://sel4.com -- why wouldn't they use the .com as the canonical site instead of a more obscure .systems? (I say this because sel4.systems is linked from within the original article). Also, the link http://sel4.systems/FAQ/proof.pml http://sel4.systems/FAQ/proof.pml is a 404 (linked within the article where it says "Last year, Heiser’s team proved mathematically that their kernel is unhackable."). I guess this is meant to link to http://sel4.systems/Info/FAQ/proof.pml http://sel4.systems/Info/FAQ/proof.pml (where the claims are far more measured).

sanxiyn 11y ago
I don't think claims are more measured. It is more detailed, yes, but claims are still extremely strong. "Integrity means that data cannot be changed without permission, and confidentiality means that data cannot be read without permission." seL4 claims both. I think "unhackable" is a good enough summary.
- andrewchambers 11y ago
  Hacking includes guessing credentials. I don't think this protects against bad passwords etc.
- amirmc 11y ago
  I didn't mean to imply that the claims were not strong. Just that they're more careful/specific (which is a good thing for this kind of work). Also, saying a piece of software is "unhackable" is akin to saying a ship is "unsinkable".
  - schoen 11y ago
    It seems like, in light of the mathematical proof, it may be reasonable to say "does not contain exploitable software vulnerabilities". Unfortunately, it's true that might not be enough to prevent attacks in some settings. For example, see Govindavajhala and Appel's "Using Memory Errors to Attack a Virtual Machine". https://www.cs.princeton.edu/~appel/papers/memerr.pdf https://www.cs.princeton.edu/~appel/papers/memerr.pdf In this case, they show that even given correct software safety guarantees, they can write a program which requires only one bit flip in any of a large number of RAM locations in order to achieve privilege escalation or violate the safety guarantees. They can then heat or irradiate the DRAM chips and make such a bit flip likely to occur. Since they can't control which bit will flip, it might sometimes crash the computer, but it's more likely to make their attack succeed. So, one thing to study with systems like this is whether hardware fault injection can compromise the security guarantees in a way that would allow an attack to succeed.
    - nickpsecurity 11y ago
      This is why you address system security holistically. There are countless projects that sprang from the Aegis processor that address the fact that RAM and devices aren't trustworthy. One had the start of an EAL7 argument for security of software from all those attacks via the hardware mechanism without modifying the processor's internal RTL. Another shows security of information flow of a design down to the gates. Others are about just synthesizing correct designs that arbitrary parties can produce for a fab and composing them into a trustworthy system. The problem, if not specific attack, has been known a long time. The Tandem NonStop architecture assumed that its memory, I/O, and key components could fail. So, they designed system to work correctly regardless plus linear scaling of resources. My proposal was to integrate above technologies with older, non-patented version of NonStop for high security and availability.
technion 11y ago
It looks like their website has been changed. I started writing a Pull Request to fix the README links for the FAQ and Contribution guidelines, but actually printing, signing and scanning a CLA put me off.

by amirmc 11y ago

sanxiyn 11y ago

I don't think claims are more measured. It is more detailed, yes, but claims are still extremely strong. "Integrity means that data cannot be changed without permission, and confidentiality means that data cannot be read without permission." seL4 claims both. I think "unhackable" is a good enough summary.

andrewchambers 11y ago
Hacking includes guessing credentials. I don't think this protects against bad passwords etc.
amirmc 11y ago
I didn't mean to imply that the claims were not strong. Just that they're more careful/specific (which is a good thing for this kind of work). Also, saying a piece of software is "unhackable" is akin to saying a ship is "unsinkable".
- schoen 11y ago
  It seems like, in light of the mathematical proof, it may be reasonable to say "does not contain exploitable software vulnerabilities". Unfortunately, it's true that might not be enough to prevent attacks in some settings. For example, see Govindavajhala and Appel's "Using Memory Errors to Attack a Virtual Machine". https://www.cs.princeton.edu/~appel/papers/memerr.pdf https://www.cs.princeton.edu/~appel/papers/memerr.pdf In this case, they show that even given correct software safety guarantees, they can write a program which requires only one bit flip in any of a large number of RAM locations in order to achieve privilege escalation or violate the safety guarantees. They can then heat or irradiate the DRAM chips and make such a bit flip likely to occur. Since they can't control which bit will flip, it might sometimes crash the computer, but it's more likely to make their attack succeed. So, one thing to study with systems like this is whether hardware fault injection can compromise the security guarantees in a way that would allow an attack to succeed.
  - nickpsecurity 11y ago
    This is why you address system security holistically. There are countless projects that sprang from the Aegis processor that address the fact that RAM and devices aren't trustworthy. One had the start of an EAL7 argument for security of software from all those attacks via the hardware mechanism without modifying the processor's internal RTL. Another shows security of information flow of a design down to the gates. Others are about just synthesizing correct designs that arbitrary parties can produce for a fab and composing them into a trustworthy system. The problem, if not specific attack, has been known a long time. The Tandem NonStop architecture assumed that its memory, I/O, and key components could fail. So, they designed system to work correctly regardless plus linear scaling of resources. My proposal was to integrate above technologies with older, non-patented version of NonStop for high security and availability.

technion 11y ago

It looks like their website has been changed. I started writing a Pull Request to fix the README links for the FAQ and Contribution guidelines, but actually printing, signing and scanning a CLA put me off.