Re:The foundations of a provably secure operating system (PS...
by Joel_Mckay on Monday May 18, 2026 @07:48AM
(#48178352)
see other comment, the author describes some issues with current hardware virtualization. kvm is also pretty good, but not perfect... and completely irrelevant with GPU pass-through enabled. =3
[ Parent
| on HN ]
Re:The foundations of a provably secure operating system (PS...
by fsflover on Monday May 18, 2026 @07:54AM
(#48178425)
Which other approach to security do you consider reliable? Through correctness? Through obscurity?
https://blog.invisiblethings.org/2008/09/02/three-approaches...
Re:The foundations of a provably secure operating system (PS...
by Joel_Mckay on Monday May 18, 2026 @07:59AM
(#48178465)
Publicly documented encrypted mmu, as it is the only practical way to isolate contexts on parallel cores.
Or some exotic processor no one would ever sell successfully. =3
Re:The foundations of a provably secure operating system (PS...
by Rohansi on Monday May 18, 2026 @10:32AM
(#48180462)
What would an encrypted MMU do differently?
Re:The foundations of a provably secure operating system (PS...
by Joel_Mckay on Monday May 18, 2026 @10:58AM
(#48180804)
Mitigates undetectable bleeding/contamination of information between parallel processes, cores, and or rowhammer etc.
Thus, writing a robust and secure OS may actually be possible by competent programmers in most compiled languages. Best of luck =3
Re:The foundations of a provably secure operating system (PS...
by Rohansi on Monday May 18, 2026 @11:38AM
(#48181321)
But how does it accomplish that? And how can you guarantee it would solve those hardware issues?
Re:The foundations of a provably secure operating system (PS...
by Joel_Mckay on Monday May 18, 2026 @01:35PM
(#48182715)
The memory areas would appear as ciphertext to other processes/unprivileged-cores in most cases even when hardware has glitched up. If you are asking how they specifically implemented the mmu <-> unreachable key handling outside the OS, that information was never public if I recall.
I've often pondered how it was really implemented too. Best of luck. =3
"Why Multi-Threaded Code Can Sometimes Misbehave (Weak Memory Concurrency)" (Computerphile)