Comment by DebugDruid

5 days ago

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.

> 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.

  • 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.

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.

  • 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.