> My claim is that doing this kind of computer security is possible.

But your evidence does not support that claim. SeL4 has proven that it is possible to design a secure microkernel and prove its security guarantees. It does not prove that you can build entire systems (filesystem+database+web server+browser) on top of that kernel while maintaining the same security guarantees.

I'm all for improving the state of computer security, and I'd love for capability systems like SeL4 to become more prevalent. But it's only a microkernel, and it's by no means certain that the PeopleSoft vulnerability exploited here required a kernel-level compromise.

I don’t expect every piece of software written to be proven correct like SeL4. But I don’t think we don’t need to do that to get big improvements in the security of a lot of systems. Honestly the biggest insight I take from sel4 is that we can get improvements in security by breaking up a large program into isolated pieces. Give each piece as few permissions as possible, so a compromise of one part doesn’t lead to a whole system compromise. And give them a way to talk. This has big benefits for reliability - since you can fail and restart individual processes. And it has benefits for security, since a system compromise should require an attack of multiple systems simultaneously. And it has benefits for debuggability, since you can add tracing at the comms layer or isolate modules for testing.

Wasm does this. Erlang does this. SeL4 does this. Chrome is built this way. The windows driver model is moving this way. And so on. You want a solid core to build around - which is what SeL4 and beam try to be. Then it’s up to us to use those primitives and build good software. Combine that with a memory safe language (rust, go, c#, etc) to protect against buffer overruns and use after frees. And a picture starts to form of how you can build software that is a lot more secure by default.

I don’t think perfect security is worth the cost for many companies. But so many security leaks happen because of amateur hour somewhere. Bugs happen - I get that. But a single bug in a C++ program shouldn’t immediately lead to RCE with system level privileges. This stuff isn’t rocket science.