Re:Ask HN: How would you design a Modern Operating System in...
by benlivengood on Monday September 12, 2022 @02:41PM
(#32814854)
Capability systems approach what an operating system should be able to provide.
Formally proven software can close the gap. It's hard work. SeL4 is a formally proven microkernel; there is a machine-checkable proof that the C code is correct. There's also now proofs that for arm and risc the binaries are translated correctly from C [0]. It took years and is a huge accomplishment.
Operating system support for formal verification of the remaining software is the next theoretical step to achieving the security and reliability goals that modern OSs struggle with.
In addition to the parent's list, I'd add:
* Network-aware or distributed capabilities. The Internet is a huge part of modern computing and the fact that same-origin and CORS and friends are the best network object security paradigm we have is a little silly. It should be possible to refer to and interact with remote objects securely and with native syntax/semantics and have the operating system mediate any network interactions required for that.
Formally proven software can close the gap. It's hard work. SeL4 is a formally proven microkernel; there is a machine-checkable proof that the C code is correct. There's also now proofs that for arm and risc the binaries are translated correctly from C [0]. It took years and is a huge accomplishment.
Operating system support for formal verification of the remaining software is the next theoretical step to achieving the security and reliability goals that modern OSs struggle with.
In addition to the parent's list, I'd add:
* Network-aware or distributed capabilities. The Internet is a huge part of modern computing and the fact that same-origin and CORS and friends are the best network object security paradigm we have is a little silly. It should be possible to refer to and interact with remote objects securely and with native syntax/semantics and have the operating system mediate any network interactions required for that.
[0] https://docs.sel4.systems/projects/sel4/frequently-asked-que...