8 ms·

Sometimes I dream about a 100% secure OS. Maybe formal verification is the key, or Rust, I don’t know. But I would love to know that I can't be hacked.

jeffbee 9mo ago
The problem is that for the overwhelming majority of use cases the isolation features that are violated by security bugs are not being used for real isolation, but for manageability and convenience. Virtualization, physical host segregation, etc are used to achieve greater isolation. People don't necessarily care about these flaws because they aren't actually exposed to the worst case preconditions. So the amount of contributor attention you could get behind a "100% secure OS" might not be as large as you are hoping. Anyway if you want to work on such things there are various OS development efforts floating around.
- nine_k 9mo ago
  Isolation is one thing, correctness is another. You may have architecturally perfect, hardware-assisted isolation, but triggering a bug would breach it. This is how a typical break out of a VM, or a container, or a privilege escalation, happens. There is a difference between a provably secure-by-design system, and a formally proven secure implementation, like Sel4.
- ameliaquining 9mo ago
  Obligatory https://xkcd.com/2044/ https://xkcd.com/2044/.
themafia 9mo ago
> But I would love to know that I can't be hacked. Cool. So social engineering it is. You are your own worst enemy anyways.
- staticassertion 9mo ago
  A world in which the only way to get hacked is to be tricked would be an insane improvement over today. There are a lot of ways to solve social engineering issue with tech solutions too - FIDO2 is one example, as would be app isolation, etc.
sydbarrett74 9mo ago
Anything made by humans can be unmade by humans. Security is a perpetual arms race.
fsflover 9mo ago
Here you go: https://qubes-os.org https://qubes-os.org
- deleted 9mo ago
  [deleted]
- JCattheATM 9mo ago
  That protects against much, but is far from a "100% secure OS". If the specific VM or 'qube' has a vulnerability, anything in that VM could be obtained/interacted with.
  - fsflover 9mo ago
    Your VM isn't protected from malware that you run in it. However your OS and other VMs containing sensitive data (in which you of course do not run anything untrusted at all) will stay safe, by design.
    - JCattheATM 9mo ago
      > Your VM isn't protected from malware that you run in it. Right, that was the point - so your suggestion that Qubes is a '100% secure OS' is false.
      - fsflover 9mo ago
        The OS is actually secure, isn't it? As well as all your valuable data. The VM gets compromised, after which you can reset it to its original state. See: https://doc.qubes-os.org/en/latest/user/how-to-guides/how-to-use-disposables.html https://doc.qubes-os.org/en/latest/user/how-to-guides/how-to...
        JCattheATM 9mo ago
        > The OS is actually secure, isn't it? Not 100% secure, as was your claim.
pjmlp 9mo ago
This has been done multiple times in research, see Verve OS from Microsoft, even Assembly is verified, that is where Dafny came from. https://en.wikipedia.org/wiki/Verve_(operating_system) https://en.wikipedia.org/wiki/Verve_(operating_system) However, worse is better on the market, and quality doesn't pay off, hence why such ideas take decades into mainstream.

jeffbee 9mo ago

The problem is that for the overwhelming majority of use cases the isolation features that are violated by security bugs are not being used for real isolation, but for manageability and convenience. Virtualization, physical host segregation, etc are used to achieve greater isolation. People don't necessarily care about these flaws because they aren't actually exposed to the worst case preconditions. So the amount of contributor attention you could get behind a "100% secure OS" might not be as large as you are hoping. Anyway if you want to work on such things there are various OS development efforts floating around.

nine_k 9mo ago
Isolation is one thing, correctness is another. You may have architecturally perfect, hardware-assisted isolation, but triggering a bug would breach it. This is how a typical break out of a VM, or a container, or a privilege escalation, happens. There is a difference between a provably secure-by-design system, and a formally proven secure implementation, like Sel4.
ameliaquining 9mo ago
Obligatory https://xkcd.com/2044/ https://xkcd.com/2044/.

themafia 9mo ago

> But I would love to know that I can't be hacked. Cool. So social engineering it is. You are your own worst enemy anyways.

staticassertion 9mo ago
A world in which the only way to get hacked is to be tricked would be an insane improvement over today. There are a lot of ways to solve social engineering issue with tech solutions too - FIDO2 is one example, as would be app isolation, etc.

sydbarrett74 9mo ago

Anything made by humans can be unmade by humans. Security is a perpetual arms race.

fsflover 9mo ago

Here you go: https://qubes-os.org https://qubes-os.org

deleted 9mo ago
[deleted]
JCattheATM 9mo ago
That protects against much, but is far from a "100% secure OS". If the specific VM or 'qube' has a vulnerability, anything in that VM could be obtained/interacted with.
- fsflover 9mo ago
  Your VM isn't protected from malware that you run in it. However your OS and other VMs containing sensitive data (in which you of course do not run anything untrusted at all) will stay safe, by design.
  - JCattheATM 9mo ago
    > Your VM isn't protected from malware that you run in it. Right, that was the point - so your suggestion that Qubes is a '100% secure OS' is false.
    - fsflover 9mo ago
      The OS is actually secure, isn't it? As well as all your valuable data. The VM gets compromised, after which you can reset it to its original state. See: https://doc.qubes-os.org/en/latest/user/how-to-guides/how-to-use-disposables.html https://doc.qubes-os.org/en/latest/user/how-to-guides/how-to...
      - JCattheATM 9mo ago
        > The OS is actually secure, isn't it? Not 100% secure, as was your claim.

pjmlp 9mo ago

This has been done multiple times in research, see Verve OS from Microsoft, even Assembly is verified, that is where Dafny came from. https://en.wikipedia.org/wiki/Verve_(operating_system) https://en.wikipedia.org/wiki/Verve_(operating_system) However, worse is better on the market, and quality doesn't pay off, hence why such ideas take decades into mainstream.