alt Hacker NewsSometimes 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.
Replies
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.
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)
However, worse is better on the market, and quality doesn't pay off, hence why such ideas take decades into mainstream.
Anything made by humans can be unmade by humans. Security is a perpetual arms race.
> 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.